diff --git a/README.md b/README.md index bc5c4f6..83b1809 100644 --- a/README.md +++ b/README.md @@ -54,7 +54,7 @@ pip install . * [LeanDojo Website](https://leandojo.org/): The official website of LeanDojo. * [LeanDojo Benchmark](https://doi.org/10.5281/zenodo.8016385) [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.8016385.svg)](https://doi.org/10.5281/zenodo.8016385): The dataset used in our paper, consisting of 98,734 theorems and proofs extracted from [mathlib](https://github.com/leanprover-community/mathlib/commits/19c869efa56bbb8b500f2724c0b77261edbfa28c) by [generate-benchmark-lean3.ipynb](./scripts/generate-benchmark-lean3.ipynb). -* [LeanDojo Benchmark 4](https://doi.org/10.5281/zenodo.8040109) [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.8040109.svg)](https://doi.org/10.5281/zenodo.8040109): The Lean 4 version of LeanDojo Benchmark, consisting of 102,514 theorems and proofs extracted from [mathlib4](https://github.com/leanprover-community/mathlib4/commit/3ce43c18f614b76e161f911b75a3e1ef641620ff) by [generate-benchmark-lean4.ipynb](./scripts/generate-benchmark-lean4.ipynb). +* [LeanDojo Benchmark 4](https://doi.org/10.5281/zenodo.8040109) [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.8040109.svg)](https://doi.org/10.5281/zenodo.8040109): The Lean 4 version of LeanDojo Benchmark, consisting of 102,514 theorems and proofs extracted from [mathlib4](https://github.com/leanprover-community/mathlib4/commit/3c307701fa7e9acbdc0680d7f3b9c9fed9081740) by [generate-benchmark-lean4.ipynb](./scripts/generate-benchmark-lean4.ipynb). * [ReProver](https://github.com/lean-dojo/ReProver): The ReProver (Retrieval-Augmented Prover) model in our paper. * [LeanDojo ChatGPT Plugin](https://github.com/lean-dojo/LeanDojoChatGPT) * [Lean Copilot: Running language models as copilots for theorem proving in Lean](https://github.com/lean-dojo/LeanCopilot) diff --git a/docs/source/index.rst b/docs/source/index.rst index 6a456da..2825327 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -18,7 +18,7 @@ Related Links * `LeanDojo Website `_: The official website of LeanDojo. * `LeanDojo Benchmark `_: The Lean 3 dataset used in `our paper `_, consisting of 98,734 theorems and proofs extracted from `mathlib `_ by `generate-benchmark-lean3.ipynb `_. -* `LeanDojo Benchmark 4 `_: The Lean 4 version of LeanDojo Benchmark, consisting of 102,514 theorems and proofs extracted from `mathlib4 `_ by `generate-benchmark-lean4.ipynb `_. +* `LeanDojo Benchmark 4 `_: The Lean 4 version of LeanDojo Benchmark, consisting of 102,514 theorems and proofs extracted from `mathlib4 `_ by `generate-benchmark-lean4.ipynb `_. * `ReProver `_: The ReProver (Retrieval-Augmented Prover) model in our paper. * `LeanInfer `_: Native neural network inference for running ReProver directly in Lean 4. diff --git a/scripts/demo-lean4.ipynb b/scripts/demo-lean4.ipynb index 2c2167b..873cf80 100644 --- a/scripts/demo-lean4.ipynb +++ b/scripts/demo-lean4.ipynb @@ -38,7 +38,7 @@ { "data": { "text/plain": [ - "LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3ce43c18f614b76e161f911b75a3e1ef641620ff')" + "LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3c307701fa7e9acbdc0680d7f3b9c9fed9081740')" ] }, "execution_count": 2, @@ -49,7 +49,7 @@ "source": [ "repo = LeanGitRepo(\n", " \"https://github.com/leanprover-community/mathlib4\",\n", - " \"3ce43c18f614b76e161f911b75a3e1ef641620ff\",\n", + " \"3c307701fa7e9acbdc0680d7f3b9c9fed9081740\",\n", ")\n", "\n", "repo" @@ -75,7 +75,7 @@ { "data": { "text/plain": [ - "{'content': 'leanprover/lean4:v4.2.0-rc4\\n'}" + "{'content': 'leanprover/lean4:v4.6.0-rc1\\n'}" ] }, "execution_count": 4, @@ -97,10 +97,16 @@ "name": "stderr", "output_type": "stream", "text": [ - "\u001b[32m2023-12-13 22:27:39.003\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m182\u001b[0m - \u001b[1mLoading the traced repo from /Users/kaiyuy/.cache/lean_dojo/leanprover-community-mathlib4-3ce43c18f614b76e161f911b75a3e1ef641620ff/mathlib4\u001b[0m\n", - "2023-12-13 22:27:41,204\tINFO worker.py:1664 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n", - "100%|██████████| 4462/4462 [12:53<00:00, 5.77it/s] \n", - "Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356\n" + "\u001b[32m2024-03-07 20:11:09.981\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m116\u001b[0m - \u001b[1mLoading the traced repo from /Users/yangky/.cache/lean_dojo/leanprover-community-mathlib4-3c307701fa7e9acbdc0680d7f3b9c9fed9081740/mathlib4\u001b[0m\n", + "2024-03-07 20:11:12,625\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n", + "100%|██████████| 5042/5042 [32:30<00:00, 2.59it/s] \n", + "\u001b[32m2024-03-07 20:43:52.728\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='a751d21d4b68c999accb6fc5d960538af26ad5ec') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n", + "\u001b[32m2024-03-07 20:44:07.380\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n", + "\u001b[32m2024-03-07 20:44:16.575\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/xubaiw/CMark.lean', commit='0077cbbaa92abf855fc1c0413e158ffd8195ec77') relies on an unsupported Lean version: 8fc1af650ad6d31cf766d9bc84119149330e7d4e\u001b[0m\n", + "Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356\n", + "\u001b[32m2024-03-07 20:44:20.008\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/mhuisi/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa') relies on an unsupported Lean version: 216d2460e0adec8317fdeeb6f2543cb7442564fd\u001b[0m\n", + "\u001b[32m2024-03-07 20:44:26.382\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/fgdorais/lean4-unicode-basic', commit='280d75fdfe7be8eb337be7f1bf8479b4aac09f71') relies on an unsupported Lean version: 0d7051497ea09b2b4a4ef608e371b8f317487c3c\u001b[0m\n", + "\u001b[32m2024-03-07 20:44:30.682\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/hargonix/LeanInk', commit='2447df5cc6e48eb965c3c3fba87e46d353b5e9f1') relies on an unsupported Lean version: f6cd6c069587cfe62dd68cb6330f9ad794a56724\u001b[0m\n" ] } ], @@ -118,7 +124,7 @@ { "data": { "text/plain": [ - "" + "" ] }, "execution_count": 6, @@ -132,1620 +138,125 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 8, "id": "375023d4", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "4462" + "5042" ] }, - "execution_count": 7, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "traced_repo.num_traced_files" + "len(traced_repo.traced_files)" ] }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 15, "id": "1c725a11", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TracedFile(root_dir=PosixPath('/Users/kaiyuy/.cache/lean_dojo/leanprover-community-mathlib4-3ce43c18f614b76e161f911b75a3e1ef641620ff/mathlib4'), repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3ce43c18f614b76e161f911b75a3e1ef641620ff'), lean_file=LeanFile(path=PosixPath('Mathlib/LinearAlgebra/Basic.lean'), uses_lean4=True))" + "TracedFile(root_dir=PosixPath('/Users/yangky/.cache/lean_dojo/leanprover-community-mathlib4-3c307701fa7e9acbdc0680d7f3b9c9fed9081740/mathlib4'), repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3c307701fa7e9acbdc0680d7f3b9c9fed9081740'), lean_file=LeanFile(path=PosixPath('Mathlib/Algebra/BigOperators/Pi.lean')))" ] }, - "execution_count": 8, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "traced_file = traced_repo.get_traced_file(\"Mathlib/LinearAlgebra/Basic.lean\")\n", + "traced_file = traced_repo.get_traced_file(\"Mathlib/Algebra/BigOperators/Pi.lean\")\n", "\n", "traced_file" ] }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 16, "id": "153f37ce", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "[{'full_name': 'Finsupp.smul_sum',\n", - " 'code': 'theorem smul_sum {α : Type*} {β : Type*} {R : Type*} {M : Type*} [Zero β] [AddCommMonoid M]\\n [DistribSMul R M] {v : α →₀ β} {c : R} {h : α → β → M} :\\n c • v.sum h = v.sum fun a b => c • h a b',\n", - " 'start': [75, 1],\n", - " 'end': [78, 18],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"Finsupp.sum_smul_index_linearMap'\",\n", - " 'code': \"@[simp]\\ntheorem sum_smul_index_linearMap' {α : Type*} {R : Type*} {M : Type*} {M₂ : Type*} [Semiring R]\\n [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {v : α →₀ M} {c : R}\\n {h : α → M →ₗ[R] M₂} : ((c • v).sum fun a => h a) = c • v.sum fun a => h a\",\n", - " 'start': [81, 1],\n", - " 'end': [88, 25],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Finsupp.linearEquivFunOnFinite',\n", - " 'code': \"@[simps apply]\\nnoncomputable def linearEquivFunOnFinite : (α →₀ M) ≃ₗ[R] α → M :=\\n { equivFunOnFinite with\\n toFun := (⇑)\\n map_add' := fun _ _ => rfl\\n map_smul' := fun _ _ => rfl }\",\n", - " 'start': [95, 1],\n", - " 'end': [102, 34],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Finsupp.linearEquivFunOnFinite_single',\n", - " 'code': '@[simp]\\ntheorem linearEquivFunOnFinite_single [DecidableEq α] (x : α) (m : M) :\\n (linearEquivFunOnFinite R M α) (single x m) = Pi.single x m',\n", - " 'start': [105, 1],\n", - " 'end': [108, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Finsupp.linearEquivFunOnFinite_symm_single',\n", - " 'code': '@[simp]\\ntheorem linearEquivFunOnFinite_symm_single [DecidableEq α] (x : α) (m : M) :\\n (linearEquivFunOnFinite R M α).symm (Pi.single x m) = single x m',\n", - " 'start': [111, 1],\n", - " 'end': [114, 35],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Finsupp.linearEquivFunOnFinite_symm_coe',\n", - " 'code': '@[simp]\\ntheorem linearEquivFunOnFinite_symm_coe (f : α →₀ M) : (linearEquivFunOnFinite R M α).symm f = f',\n", - " 'start': [117, 1],\n", - " 'end': [119, 52],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Finsupp.LinearEquiv.finsuppUnique',\n", - " 'code': \"noncomputable def LinearEquiv.finsuppUnique (α : Type*) [Unique α] : (α →₀ M) ≃ₗ[R] M :=\\n { Finsupp.equivFunOnFinite.trans (Equiv.funUnique α M) with\\n map_add' := fun _ _ => rfl\\n map_smul' := fun _ _ => rfl }\",\n", - " 'start': [122, 1],\n", - " 'end': [127, 34],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Finsupp.LinearEquiv.finsuppUnique_apply',\n", - " 'code': '@[simp]\\ntheorem LinearEquiv.finsuppUnique_apply (α : Type*) [Unique α] (f : α →₀ M) :\\n LinearEquiv.finsuppUnique R M α f = f default',\n", - " 'start': [132, 1],\n", - " 'end': [135, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Finsupp.LinearEquiv.finsuppUnique_symm_apply',\n", - " 'code': '@[simp]\\ntheorem LinearEquiv.finsuppUnique_symm_apply {α : Type*} [Unique α] (m : M) :\\n (LinearEquiv.finsuppUnique R M α).symm m = Finsupp.single default m',\n", - " 'start': [138, 1],\n", - " 'end': [142, 39],\n", + "[{'full_name': 'Pi.list_prod_apply',\n", + " 'code': '@[to_additive]\\ntheorem list_prod_apply {α : Type*} {β : α → Type*} [∀ a, Monoid (β a)] (a : α)\\n (l : List (∀ a, β a)) : l.prod a = (l.map fun f : ∀ a, β a ↦ f a).prod',\n", + " 'start': [25, 1],\n", + " 'end': [28, 38],\n", + " 'kind': 'commanddeclaration'},\n", + " {'full_name': 'Pi.multiset_prod_apply',\n", + " 'code': '@[to_additive]\\ntheorem multiset_prod_apply {α : Type*} {β : α → Type*} [∀ a, CommMonoid (β a)] (a : α)\\n (s : Multiset (∀ a, β a)) : s.prod a = (s.map fun f : ∀ a, β a ↦ f a).prod',\n", + " 'start': [32, 1],\n", + " 'end': [35, 42],\n", + " 'kind': 'commanddeclaration'},\n", + " {'full_name': 'Finset.prod_apply',\n", + " 'code': '@[to_additive (attr := simp)]\\ntheorem Finset.prod_apply {α : Type*} {β : α → Type*} {γ} [∀ a, CommMonoid (β a)] (a : α)\\n (s : Finset γ) (g : γ → ∀ a, β a) : (∏ c in s, g c) a = ∏ c in s, g c a',\n", + " 'start': [41, 1],\n", + " 'end': [44, 38],\n", + " 'kind': 'commanddeclaration'},\n", + " {'full_name': 'Finset.prod_fn',\n", + " 'code': '@[to_additive \"An \\'unapplied\\' analogue of `Finset.sum_apply`.\"]\\ntheorem Finset.prod_fn {α : Type*} {β : α → Type*} {γ} [∀ a, CommMonoid (β a)] (s : Finset γ)\\n (g : γ → ∀ a, β a) : ∏ c in s, g c = fun a ↦ ∏ c in s, g c a',\n", + " 'start': [48, 1],\n", + " 'end': [52, 41],\n", + " 'kind': 'commanddeclaration'},\n", + " {'full_name': 'Fintype.prod_apply',\n", + " 'code': '@[to_additive]\\ntheorem Fintype.prod_apply {α : Type*} {β : α → Type*} {γ : Type*} [Fintype γ]\\n [∀ a, CommMonoid (β a)] (a : α) (g : γ → ∀ a, β a) : (∏ c, g c) a = ∏ c, g c a',\n", + " 'start': [56, 1],\n", + " 'end': [59, 36],\n", + " 'kind': 'commanddeclaration'},\n", + " {'full_name': 'prod_mk_prod',\n", + " 'code': '@[to_additive prod_mk_sum]\\ntheorem prod_mk_prod {α β γ : Type*} [CommMonoid α] [CommMonoid β] (s : Finset γ) (f : γ → α)\\n (g : γ → β) : (∏ x in s, f x, ∏ x in s, g x) = ∏ x in s, (f x, g x)',\n", + " 'start': [63, 1],\n", + " 'end': [67, 88],\n", " 'kind': 'commanddeclaration'},\n", " {'full_name': 'pi_eq_sum_univ',\n", " 'code': 'theorem pi_eq_sum_univ {ι : Type*} [Fintype ι] [DecidableEq ι] {R : Type*} [Semiring R]\\n (x : ι → R) : x = ∑ i, (x i) • fun j => if i = j then (1 : R) else 0',\n", - " 'start': [147, 1],\n", - " 'end': [151, 7],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.domRestrict',\n", - " 'code': 'def domRestrict (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) : p →ₛₗ[σ₁₂] M₂ :=\\n f.comp p.subtype',\n", - " 'start': [174, 1],\n", - " 'end': [177, 19],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.domRestrict_apply',\n", - " 'code': '@[simp]\\ntheorem domRestrict_apply (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) (x : p) :\\n f.domRestrict p x = f x',\n", - " 'start': [180, 1],\n", - " 'end': [183, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.codRestrict',\n", - " 'code': \"def codRestrict (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) (h : ∀ c, f c ∈ p) : M →ₛₗ[σ₁₂] p := by\\n refine' { toFun := fun c => ⟨f c, h c⟩.. } <;> intros <;> apply SetCoe.ext <;> simp\",\n", - " 'start': [186, 1],\n", - " 'end': [189, 86],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.codRestrict_apply',\n", - " 'code': '@[simp]\\ntheorem codRestrict_apply (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) {h} (x : M) :\\n (codRestrict p f h x : M₂) = f x',\n", - " 'start': [192, 1],\n", - " 'end': [195, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.comp_codRestrict',\n", - " 'code': '@[simp]\\ntheorem comp_codRestrict (p : Submodule R₃ M₃) (h : ∀ b, g b ∈ p) :\\n ((codRestrict p g h).comp f : M →ₛₗ[σ₁₃] p) = codRestrict p (g.comp f) fun _ => h _',\n", - " 'start': [198, 1],\n", - " 'end': [201, 19],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.subtype_comp_codRestrict',\n", - " 'code': '@[simp]\\ntheorem subtype_comp_codRestrict (p : Submodule R₂ M₂) (h : ∀ b, f b ∈ p) :\\n p.subtype.comp (codRestrict p f h) = f',\n", - " 'start': [204, 1],\n", - " 'end': [207, 19],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.restrict',\n", - " 'code': 'def restrict (f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) :\\n p →ₗ[R] q :=\\n (f.domRestrict p).codRestrict q <| SetLike.forall.2 hf',\n", - " 'start': [210, 1],\n", - " 'end': [213, 57],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.restrict_coe_apply',\n", - " 'code': '@[simp]\\ntheorem restrict_coe_apply (f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁}\\n (hf : ∀ x ∈ p, f x ∈ q) (x : p) : ↑(f.restrict hf x) = f x',\n", - " 'start': [216, 1],\n", - " 'end': [219, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.restrict_apply',\n", - " 'code': 'theorem restrict_apply {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁}\\n (hf : ∀ x ∈ p, f x ∈ q) (x : p) : f.restrict hf x = ⟨f x, hf x.1 x.2⟩',\n", - " 'start': [222, 1],\n", - " 'end': [224, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.subtype_comp_restrict',\n", - " 'code': 'theorem subtype_comp_restrict {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁}\\n (hf : ∀ x ∈ p, f x ∈ q) : q.subtype.comp (f.restrict hf) = f.domRestrict p',\n", - " 'start': [227, 1],\n", - " 'end': [229, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.restrict_eq_codRestrict_domRestrict',\n", - " 'code': 'theorem restrict_eq_codRestrict_domRestrict {f : M →ₗ[R] M₁} {p : Submodule R M}\\n {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) :\\n f.restrict hf = (f.domRestrict p).codRestrict q fun x => hf x.1 x.2',\n", - " 'start': [232, 1],\n", - " 'end': [235, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.restrict_eq_domRestrict_codRestrict',\n", - " 'code': 'theorem restrict_eq_domRestrict_codRestrict {f : M →ₗ[R] M₁} {p : Submodule R M}\\n {q : Submodule R M₁} (hf : ∀ x, f x ∈ q) :\\n (f.restrict fun x _ => hf x) = (f.codRestrict q hf).domRestrict p',\n", - " 'start': [238, 1],\n", - " 'end': [241, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.uniqueOfLeft',\n", - " 'code': 'instance uniqueOfLeft [Subsingleton M] : Unique (M →ₛₗ[σ₁₂] M₂) :=\\n { inferInstanceAs (Inhabited (M →ₛₗ[σ₁₂] M₂)) with\\n uniq := fun f => ext fun x => by rw [Subsingleton.elim x 0, map_zero, map_zero] }',\n", - " 'start': [244, 1],\n", - " 'end': [246, 86],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.uniqueOfRight',\n", - " 'code': 'instance uniqueOfRight [Subsingleton M₂] : Unique (M →ₛₗ[σ₁₂] M₂) :=\\n coe_injective.unique',\n", - " 'start': [249, 1],\n", - " 'end': [250, 23],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.evalAddMonoidHom',\n", - " 'code': \"def evalAddMonoidHom (a : M) : (M →ₛₗ[σ₁₂] M₂) →+ M₂ where\\n toFun f := f a\\n map_add' f g := LinearMap.add_apply f g a\\n map_zero' := rfl\",\n", - " 'start': [253, 1],\n", - " 'end': [257, 19],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearMap.toAddMonoidHom'\",\n", - " 'code': \"def toAddMonoidHom' : (M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂ where\\n toFun := toAddMonoidHom\\n map_zero' := by ext; rfl\\n map_add' := by intros; ext; rfl\",\n", - " 'start': [260, 1],\n", - " 'end': [264, 34],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.sum_apply',\n", - " 'code': 'theorem sum_apply (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) (b : M) :\\n (∑ d in t, f d) b = ∑ d in t, f d b',\n", - " 'start': [267, 1],\n", - " 'end': [269, 66],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.smulRight',\n", - " 'code': \"def smulRight (f : M₁ →ₗ[R] S) (x : M) : M₁ →ₗ[R] M where\\n toFun b := f b • x\\n map_add' x y := by dsimp only; rw [f.map_add, add_smul]\\n map_smul' b y := by dsimp; rw [map_smul, smul_assoc]\",\n", - " 'start': [276, 1],\n", - " 'end': [281, 55],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.coe_smulRight',\n", - " 'code': '@[simp]\\ntheorem coe_smulRight (f : M₁ →ₗ[R] S) (x : M) : (smulRight f x : M₁ → M) = fun c => f c • x',\n", - " 'start': [284, 1],\n", - " 'end': [286, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.smulRight_apply',\n", - " 'code': 'theorem smulRight_apply (f : M₁ →ₗ[R] S) (x : M) (c : M₁) : smulRight f x c = f c • x',\n", - " 'start': [289, 1],\n", - " 'end': [290, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.coeFn_sum',\n", - " 'code': '@[simp, norm_cast]\\ntheorem coeFn_sum {ι : Type*} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) :\\n ⇑(∑ i in t, f i) = ∑ i in t, (f i : M → M₂)',\n", - " 'start': [299, 1],\n", - " 'end': [306, 47],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.submodule_pow_eq_zero_of_pow_eq_zero',\n", - " 'code': 'theorem submodule_pow_eq_zero_of_pow_eq_zero {N : Submodule R M} {g : Module.End R N}\\n {G : Module.End R M} (h : G.comp N.subtype = N.subtype.comp g) {k : ℕ} (hG : G ^ k = 0) :\\n g ^ k = 0',\n", - " 'start': [309, 1],\n", - " 'end': [315, 17],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.pow_apply_mem_of_forall_mem',\n", - " 'code': \"theorem pow_apply_mem_of_forall_mem {p : Submodule R M} (n : ℕ) (h : ∀ x ∈ p, f' x ∈ p) (x : M)\\n (hx : x ∈ p) : (f' ^ n) x ∈ p\",\n", - " 'start': [322, 1],\n", - " 'end': [326, 97],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.pow_restrict',\n", - " 'code': \"theorem pow_restrict {p : Submodule R M} (n : ℕ) (h : ∀ x ∈ p, f' x ∈ p)\\n (h' := pow_apply_mem_of_forall_mem n h) :\\n (f'.restrict h) ^ n = (HPow.hPow f' n).restrict h'\",\n", - " 'start': [329, 1],\n", - " 'end': [334, 41],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.pi_apply_eq_sum_univ',\n", - " 'code': 'theorem pi_apply_eq_sum_univ [Fintype ι] [DecidableEq ι] (f : (ι → R) →ₗ[R] M) (x : ι → R) :\\n f x = ∑ i, x i • f fun j => if i = j then 1 else 0',\n", - " 'start': [339, 1],\n", - " 'end': [345, 16],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearMap.applyₗ'\",\n", - " 'code': \"@[simps]\\ndef applyₗ' : M →+ (M →ₗ[R] M₂) →ₗ[S] M₂ where\\n toFun v :=\\n { toFun := fun f => f v\\n map_add' := fun f g => f.add_apply g v\\n map_smul' := fun x f => f.smul_apply x v }\\n map_zero' := LinearMap.ext fun f => f.map_zero\\n map_add' _ _ := LinearMap.ext fun f => f.map_add _ _\",\n", - " 'start': [358, 1],\n", - " 'end': [368, 55],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ringLmapEquivSelf',\n", - " 'code': \"@[simps]\\ndef ringLmapEquivSelf [Module S M] [SMulCommClass R S M] : (R →ₗ[R] M) ≃ₗ[S] M :=\\n { applyₗ' S (1 : R) with\\n toFun := fun f => f 1\\n invFun := smulRight (1 : R →ₗ[R] R)\\n left_inv := fun f => by\\n ext\\n simp only [coe_smulRight, one_apply, smul_eq_mul, ← map_smul f, mul_one]\\n right_inv := fun x => by simp }\",\n", - " 'start': [375, 1],\n", - " 'end': [391, 36],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.compRight',\n", - " 'code': \"def compRight (f : M₂ →ₗ[R] M₃) : (M →ₗ[R] M₂) →ₗ[R] M →ₗ[R] M₃ where\\n toFun := f.comp\\n map_add' _ _ := LinearMap.ext fun _ => map_add f _ _\\n map_smul' _ _ := LinearMap.ext fun _ => map_smul f _ _\",\n", - " 'start': [406, 1],\n", - " 'end': [411, 57],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.compRight_apply',\n", - " 'code': '@[simp]\\ntheorem compRight_apply (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) : compRight f g = f.comp g',\n", - " 'start': [414, 1],\n", - " 'end': [416, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.applyₗ',\n", - " 'code': \"@[simps]\\ndef applyₗ : M →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] M₂ :=\\n { applyₗ' R with\\n toFun := fun v => { applyₗ' R v with toFun := fun f => f v }\\n map_smul' := fun _ _ => LinearMap.ext fun f => map_smul f _ _ }\",\n", - " 'start': [419, 1],\n", - " 'end': [427, 68],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearMap.domRestrict'\",\n", - " 'code': \"def domRestrict' (p : Submodule R M) : (M →ₗ[R] M₂) →ₗ[R] p →ₗ[R] M₂ where\\n toFun φ := φ.domRestrict p\\n map_add' := by simp [LinearMap.ext_iff]\\n map_smul' := by simp [LinearMap.ext_iff]\",\n", - " 'start': [430, 1],\n", - " 'end': [434, 43],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearMap.domRestrict'_apply\",\n", - " 'code': \"@[simp]\\ntheorem domRestrict'_apply (f : M →ₗ[R] M₂) (p : Submodule R M) (x : p) :\\n domRestrict' p f x = f x\",\n", - " 'start': [437, 1],\n", - " 'end': [440, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.smulRightₗ',\n", - " 'code': \"def smulRightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M where\\n toFun f :=\\n { toFun := LinearMap.smulRight f\\n map_add' := fun m m' => by\\n ext\\n apply smul_add\\n map_smul' := fun c m => by\\n ext\\n apply smul_comm }\\n map_add' f f' := by\\n ext\\n apply add_smul\\n map_smul' c f := by\\n ext\\n apply mul_smul\",\n", - " 'start': [443, 1],\n", - " 'end': [460, 19],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.smulRightₗ_apply',\n", - " 'code': '@[simp]\\ntheorem smulRightₗ_apply (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :\\n (smulRightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M) f x c = f c • x',\n", - " 'start': [463, 1],\n", - " 'end': [466, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'addMonoidHomLequivNat',\n", - " 'code': \"@[simps]\\ndef addMonoidHomLequivNat {A B : Type*} (R : Type*) [Semiring R] [AddCommMonoid A]\\n [AddCommMonoid B] [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℕ] B\\n where\\n toFun := AddMonoidHom.toNatLinearMap\\n invFun := LinearMap.toAddMonoidHom\\n map_add' := by intros; ext; rfl\\n map_smul' := by intros; ext; rfl\\n left_inv := by intro f; ext; rfl\\n right_inv := by intro f; ext; rfl\",\n", - " 'start': [473, 1],\n", - " 'end': [485, 36],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'addMonoidHomLequivInt',\n", - " 'code': \"@[simps]\\ndef addMonoidHomLequivInt {A B : Type*} (R : Type*) [Semiring R] [AddCommGroup A] [AddCommGroup B]\\n [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℤ] B\\n where\\n toFun := AddMonoidHom.toIntLinearMap\\n invFun := LinearMap.toAddMonoidHom\\n map_add' := by intros; ext; rfl\\n map_smul' := by intros; ext; rfl\\n left_inv := by intro f; ext; rfl\\n right_inv := by intro f; ext; rfl\",\n", - " 'start': [488, 1],\n", - " 'end': [500, 36],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.ofLe',\n", - " 'code': \"def ofLe (h : p ≤ p') : p →ₗ[R] p' :=\\n p.subtype.codRestrict p' fun ⟨_, hx⟩ => h hx\",\n", - " 'start': [525, 1],\n", - " 'end': [528, 47],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.coe_ofLe',\n", - " 'code': \"@[simp]\\ntheorem coe_ofLe (h : p ≤ p') (x : p) : (ofLe h x : M) = x\",\n", - " 'start': [531, 1],\n", - " 'end': [533, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.ofLe_apply',\n", - " 'code': \"theorem ofLe_apply (h : p ≤ p') (x : p) : ofLe h x = ⟨x, h x.2⟩\",\n", - " 'start': [536, 1],\n", - " 'end': [537, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.ofLe_injective',\n", - " 'code': \"theorem ofLe_injective (h : p ≤ p') : Function.Injective (ofLe h)\",\n", - " 'start': [540, 1],\n", - " 'end': [541, 43],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.subtype_comp_ofLe',\n", - " 'code': 'theorem subtype_comp_ofLe (p q : Submodule R M) (h : p ≤ q) :\\n q.subtype.comp (ofLe h) = p.subtype',\n", - " 'start': [546, 1],\n", - " 'end': [549, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map',\n", - " 'code': \"def map (f : F) (p : Submodule R M) : Submodule R₂ M₂ :=\\n { p.toAddSubmonoid.map f with\\n carrier := f '' p\\n smul_mem' := by\\n rintro c x ⟨y, hy, rfl⟩\\n obtain ⟨a, rfl⟩ := σ₁₂.surjective c\\n exact ⟨_, p.smul_mem a hy, map_smulₛₗ f _ _⟩ }\",\n", - " 'start': [556, 1],\n", - " 'end': [563, 53],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_coe',\n", - " 'code': \"@[simp]\\ntheorem map_coe (f : F) (p : Submodule R M) : (map f p : Set M₂) = f '' p\",\n", - " 'start': [566, 1],\n", - " 'end': [568, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_toAddSubmonoid',\n", - " 'code': 'theorem map_toAddSubmonoid (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) :\\n (p.map f).toAddSubmonoid = p.toAddSubmonoid.map (f : M →+ M₂)',\n", - " 'start': [571, 1],\n", - " 'end': [573, 28],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"Submodule.map_toAddSubmonoid'\",\n", - " 'code': \"theorem map_toAddSubmonoid' (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) :\\n (p.map f).toAddSubmonoid = p.toAddSubmonoid.map f\",\n", - " 'start': [576, 1],\n", - " 'end': [578, 28],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'AddMonoidHom.coe_toIntLinearMap_map',\n", - " 'code': '@[simp]\\ntheorem _root_.AddMonoidHom.coe_toIntLinearMap_map {A A₂ : Type*} [AddCommGroup A] [AddCommGroup A₂]\\n (f : A →+ A₂) (s : AddSubgroup A) :\\n (AddSubgroup.toIntSubmodule s).map f.toIntLinearMap =\\n AddSubgroup.toIntSubmodule (s.map f)',\n", - " 'start': [581, 1],\n", - " 'end': [585, 50],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'MonoidHom.coe_toAdditive_map',\n", - " 'code': '@[simp]\\ntheorem _root_.MonoidHom.coe_toAdditive_map {G G₂ : Type*} [Group G] [Group G₂] (f : G →* G₂)\\n (s : Subgroup G) :\\n s.toAddSubgroup.map (MonoidHom.toAdditive f) = Subgroup.toAddSubgroup (s.map f)',\n", - " 'start': [587, 1],\n", - " 'end': [590, 91],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'AddMonoidHom.coe_toMultiplicative_map',\n", - " 'code': '@[simp]\\ntheorem _root_.AddMonoidHom.coe_toMultiplicative_map {G G₂ : Type*} [AddGroup G] [AddGroup G₂]\\n (f : G →+ G₂) (s : AddSubgroup G) :\\n s.toSubgroup.map (AddMonoidHom.toMultiplicative f) = AddSubgroup.toSubgroup (s.map f)',\n", - " 'start': [592, 1],\n", - " 'end': [595, 97],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.mem_map',\n", - " 'code': '@[simp]\\ntheorem mem_map {f : F} {p : Submodule R M} {x : M₂} : x ∈ map f p ↔ ∃ y, y ∈ p ∧ f y = x',\n", - " 'start': [597, 1],\n", - " 'end': [599, 10],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.mem_map_of_mem',\n", - " 'code': 'theorem mem_map_of_mem {f : F} {p : Submodule R M} {r} (h : r ∈ p) : f r ∈ map f p',\n", - " 'start': [602, 1],\n", - " 'end': [603, 27],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.apply_coe_mem_map',\n", - " 'code': 'theorem apply_coe_mem_map (f : F) {p : Submodule R M} (r : p) : f r ∈ map f p',\n", - " 'start': [606, 1],\n", - " 'end': [607, 24],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_id',\n", - " 'code': '@[simp]\\ntheorem map_id : map (LinearMap.id : M →ₗ[R] M) p = p',\n", - " 'start': [610, 1],\n", - " 'end': [612, 33],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_comp',\n", - " 'code': 'theorem map_comp [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] (f : M →ₛₗ[σ₁₂] M₂)\\n (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R M) : map (g.comp f : M →ₛₗ[σ₁₃] M₃) p = map g (map f p)',\n", - " 'start': [615, 1],\n", - " 'end': [617, 96],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_mono',\n", - " 'code': \"theorem map_mono {f : F} {p p' : Submodule R M} : p ≤ p' → map f p ≤ map f p'\",\n", - " 'start': [620, 1],\n", - " 'end': [621, 17],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_zero',\n", - " 'code': '@[simp]\\ntheorem map_zero : map (0 : M →ₛₗ[σ₁₂] M₂) p = ⊥',\n", - " 'start': [624, 1],\n", - " 'end': [627, 33],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_add_le',\n", - " 'code': 'theorem map_add_le (f g : M →ₛₗ[σ₁₂] M₂) : map (f + g) p ≤ map f p ⊔ map g p',\n", - " 'start': [630, 1],\n", - " 'end': [632, 60],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_inf_le',\n", - " 'code': 'theorem map_inf_le (f : F) {p q : Submodule R M} :\\n (p ⊓ q).map f ≤ p.map f ⊓ q.map f',\n", - " 'start': [635, 1],\n", - " 'end': [637, 27],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_inf',\n", - " 'code': 'theorem map_inf (f : F) {p q : Submodule R M} (hf : Injective f) :\\n (p ⊓ q).map f = p.map f ⊓ q.map f',\n", - " 'start': [639, 1],\n", - " 'end': [641, 46],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.range_map_nonempty',\n", - " 'code': 'theorem range_map_nonempty (N : Submodule R M) :\\n (Set.range (fun ϕ => Submodule.map ϕ N : (M →ₛₗ[σ₁₂] M₂) → Submodule R₂ M₂)).Nonempty',\n", - " 'start': [643, 1],\n", - " 'end': [645, 34],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.equivMapOfInjective',\n", - " 'code': \"noncomputable def equivMapOfInjective (f : F) (i : Injective f) (p : Submodule R M) :\\n p ≃ₛₗ[σ₁₂] p.map f :=\\n { Equiv.Set.image f p i with\\n map_add' := by\\n intros\\n simp only [coe_add, map_add, Equiv.toFun_as_coe, Equiv.Set.image_apply]\\n rfl\\n map_smul' := by\\n intros\\n simp only [coe_smul_of_tower, map_smulₛₗ, Equiv.toFun_as_coe, Equiv.Set.image_apply]\\n rfl }\",\n", - " 'start': [654, 1],\n", - " 'end': [667, 12],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.coe_equivMapOfInjective_apply',\n", - " 'code': '@[simp]\\ntheorem coe_equivMapOfInjective_apply (f : F) (i : Injective f) (p : Submodule R M) (x : p) :\\n (equivMapOfInjective f i p x : M₂) = f x',\n", - " 'start': [670, 1],\n", - " 'end': [673, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap',\n", - " 'code': \"def comap (f : F) (p : Submodule R₂ M₂) : Submodule R M :=\\n { p.toAddSubmonoid.comap f with\\n carrier := f ⁻¹' p\\n smul_mem' := fun a x h => by simp [p.smul_mem (σ₁₂ a) h] }\",\n", - " 'start': [676, 1],\n", - " 'end': [680, 63],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_coe',\n", - " 'code': \"@[simp]\\ntheorem comap_coe (f : F) (p : Submodule R₂ M₂) : (comap f p : Set M) = f ⁻¹' p\",\n", - " 'start': [683, 1],\n", - " 'end': [685, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.AddMonoidHom.coe_toIntLinearMap_comap',\n", - " 'code': '@[simp]\\ntheorem AddMonoidHom.coe_toIntLinearMap_comap {A A₂ : Type*} [AddCommGroup A] [AddCommGroup A₂]\\n (f : A →+ A₂) (s : AddSubgroup A₂) :\\n (AddSubgroup.toIntSubmodule s).comap f.toIntLinearMap =\\n AddSubgroup.toIntSubmodule (s.comap f)',\n", - " 'start': [688, 1],\n", - " 'end': [692, 52],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.mem_comap',\n", - " 'code': '@[simp]\\ntheorem mem_comap {f : F} {p : Submodule R₂ M₂} : x ∈ comap f p ↔ f x ∈ p',\n", - " 'start': [694, 1],\n", - " 'end': [696, 10],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_id',\n", - " 'code': '@[simp]\\ntheorem comap_id : comap (LinearMap.id : M →ₗ[R] M) p = p',\n", - " 'start': [699, 1],\n", - " 'end': [701, 28],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_comp',\n", - " 'code': 'theorem comap_comp (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R₃ M₃) :\\n comap (g.comp f : M →ₛₗ[σ₁₃] M₃) p = comap f (comap g p)',\n", - " 'start': [704, 1],\n", - " 'end': [706, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_mono',\n", - " 'code': \"theorem comap_mono {f : F} {q q' : Submodule R₂ M₂} : q ≤ q' → comap f q ≤ comap f q'\",\n", - " 'start': [709, 1],\n", - " 'end': [710, 16],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.le_comap_pow_of_le_comap',\n", - " 'code': 'theorem le_comap_pow_of_le_comap (p : Submodule R M) {f : M →ₗ[R] M} (h : p ≤ p.comap f) (k : ℕ) :\\n p ≤ p.comap (f ^ k)',\n", - " 'start': [713, 1],\n", - " 'end': [717, 71],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_le_iff_le_comap',\n", - " 'code': 'theorem map_le_iff_le_comap {f : F} {p : Submodule R M} {q : Submodule R₂ M₂} :\\n map f p ≤ q ↔ p ≤ comap f q',\n", - " 'start': [724, 1],\n", - " 'end': [726, 19],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.gc_map_comap',\n", - " 'code': 'theorem gc_map_comap (f : F) : GaloisConnection (map f) (comap f)',\n", - " 'start': [729, 1],\n", - " 'end': [730, 32],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_bot',\n", - " 'code': '@[simp]\\ntheorem map_bot (f : F) : map f ⊥ = ⊥',\n", - " 'start': [733, 1],\n", - " 'end': [735, 25],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_sup',\n", - " 'code': \"@[simp]\\ntheorem map_sup (f : F) : map f (p ⊔ p') = map f p ⊔ map f p'\",\n", - " 'start': [738, 1],\n", - " 'end': [740, 62],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_iSup',\n", - " 'code': '@[simp]\\ntheorem map_iSup {ι : Sort*} (f : F) (p : ι → Submodule R M) :\\n map f (⨆ i, p i) = ⨆ i, map f (p i)',\n", - " 'start': [743, 1],\n", - " 'end': [746, 63],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_top',\n", - " 'code': '@[simp]\\ntheorem comap_top (f : F) : comap f ⊤ = ⊤',\n", - " 'start': [751, 1],\n", - " 'end': [753, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_inf',\n", - " 'code': \"@[simp]\\ntheorem comap_inf (f : F) : comap f (q ⊓ q') = comap f q ⊓ comap f q'\",\n", - " 'start': [756, 1],\n", - " 'end': [758, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_iInf',\n", - " 'code': '@[simp]\\ntheorem comap_iInf [RingHomSurjective σ₁₂] {ι : Sort*} (f : F) (p : ι → Submodule R₂ M₂) :\\n comap f (⨅ i, p i) = ⨅ i, comap f (p i)',\n", - " 'start': [761, 1],\n", - " 'end': [764, 63],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_zero',\n", - " 'code': '@[simp]\\ntheorem comap_zero : comap (0 : M →ₛₗ[σ₁₂] M₂) q = ⊤',\n", - " 'start': [767, 1],\n", - " 'end': [769, 17],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_comap_le',\n", - " 'code': 'theorem map_comap_le [RingHomSurjective σ₁₂] (f : F) (q : Submodule R₂ M₂) :\\n map f (comap f q) ≤ q',\n", - " 'start': [772, 1],\n", - " 'end': [774, 28],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.le_comap_map',\n", - " 'code': 'theorem le_comap_map [RingHomSurjective σ₁₂] (f : F) (p : Submodule R M) : p ≤ comap f (map f p)',\n", - " 'start': [777, 1],\n", - " 'end': [778, 28],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.giMapComap',\n", - " 'code': 'def giMapComap : GaloisInsertion (map f) (comap f) :=\\n (gc_map_comap f).toGaloisInsertion fun S x hx => by\\n rcases hf x with ⟨y, rfl⟩\\n simp only [mem_map, mem_comap]\\n exact ⟨y, hx, rfl⟩',\n", - " 'start': [787, 1],\n", - " 'end': [792, 23],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_comap_eq_of_surjective',\n", - " 'code': 'theorem map_comap_eq_of_surjective (p : Submodule R₂ M₂) : (p.comap f).map f = p',\n", - " 'start': [795, 1],\n", - " 'end': [796, 27],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_surjective_of_surjective',\n", - " 'code': 'theorem map_surjective_of_surjective : Function.Surjective (map f)',\n", - " 'start': [799, 1],\n", - " 'end': [800, 31],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_injective_of_surjective',\n", - " 'code': 'theorem comap_injective_of_surjective : Function.Injective (comap f)',\n", - " 'start': [803, 1],\n", - " 'end': [804, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_sup_comap_of_surjective',\n", - " 'code': 'theorem map_sup_comap_of_surjective (p q : Submodule R₂ M₂) :\\n (p.comap f ⊔ q.comap f).map f = p ⊔ q',\n", - " 'start': [807, 1],\n", - " 'end': [809, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_iSup_comap_of_sujective',\n", - " 'code': 'theorem map_iSup_comap_of_sujective {ι : Sort*} (S : ι → Submodule R₂ M₂) :\\n (⨆ i, (S i).comap f).map f = iSup S',\n", - " 'start': [812, 1],\n", - " 'end': [814, 29],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_inf_comap_of_surjective',\n", - " 'code': 'theorem map_inf_comap_of_surjective (p q : Submodule R₂ M₂) :\\n (p.comap f ⊓ q.comap f).map f = p ⊓ q',\n", - " 'start': [817, 1],\n", - " 'end': [819, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_iInf_comap_of_surjective',\n", - " 'code': 'theorem map_iInf_comap_of_surjective {ι : Sort*} (S : ι → Submodule R₂ M₂) :\\n (⨅ i, (S i).comap f).map f = iInf S',\n", - " 'start': [822, 1],\n", - " 'end': [824, 29],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_le_comap_iff_of_surjective',\n", - " 'code': 'theorem comap_le_comap_iff_of_surjective (p q : Submodule R₂ M₂) : p.comap f ≤ q.comap f ↔ p ≤ q',\n", - " 'start': [827, 1],\n", - " 'end': [828, 29],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_strictMono_of_surjective',\n", - " 'code': 'theorem comap_strictMono_of_surjective : StrictMono (comap f)',\n", - " 'start': [831, 1],\n", - " 'end': [832, 31],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.gciMapComap',\n", - " 'code': 'def gciMapComap : GaloisCoinsertion (map f) (comap f) :=\\n (gc_map_comap f).toGaloisCoinsertion fun S x => by\\n simp [mem_comap, mem_map, forall_exists_index, and_imp]\\n intro y hy hxy\\n rw [hf.eq_iff] at hxy\\n rwa [← hxy]',\n", - " 'start': [841, 1],\n", - " 'end': [847, 16],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_map_eq_of_injective',\n", - " 'code': 'theorem comap_map_eq_of_injective (p : Submodule R M) : (p.map f).comap f = p',\n", - " 'start': [850, 1],\n", - " 'end': [851, 28],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_surjective_of_injective',\n", - " 'code': 'theorem comap_surjective_of_injective : Function.Surjective (comap f)',\n", - " 'start': [854, 1],\n", - " 'end': [855, 32],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_injective_of_injective',\n", - " 'code': 'theorem map_injective_of_injective : Function.Injective (map f)',\n", - " 'start': [858, 1],\n", - " 'end': [859, 31],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_inf_map_of_injective',\n", - " 'code': 'theorem comap_inf_map_of_injective (p q : Submodule R M) : (p.map f ⊓ q.map f).comap f = p ⊓ q',\n", - " 'start': [862, 1],\n", - " 'end': [863, 31],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_iInf_map_of_injective',\n", - " 'code': 'theorem comap_iInf_map_of_injective {ι : Sort*} (S : ι → Submodule R M) :\\n (⨅ i, (S i).map f).comap f = iInf S',\n", - " 'start': [866, 1],\n", - " 'end': [868, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_sup_map_of_injective',\n", - " 'code': 'theorem comap_sup_map_of_injective (p q : Submodule R M) : (p.map f ⊔ q.map f).comap f = p ⊔ q',\n", - " 'start': [871, 1],\n", - " 'end': [872, 31],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_iSup_map_of_injective',\n", - " 'code': 'theorem comap_iSup_map_of_injective {ι : Sort*} (S : ι → Submodule R M) :\\n (⨆ i, (S i).map f).comap f = iSup S',\n", - " 'start': [875, 1],\n", - " 'end': [877, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_le_map_iff_of_injective',\n", - " 'code': 'theorem map_le_map_iff_of_injective (p q : Submodule R M) : p.map f ≤ q.map f ↔ p ≤ q',\n", - " 'start': [880, 1],\n", - " 'end': [881, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_strictMono_of_injective',\n", - " 'code': 'theorem map_strictMono_of_injective : StrictMono (map f)',\n", - " 'start': [884, 1],\n", - " 'end': [885, 32],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.orderIsoMapComap',\n", - " 'code': \"@[simps symm_apply apply]\\ndef orderIsoMapComap (f : F) : Submodule R M ≃o Submodule R₂ M₂ where\\n toFun := map f\\n invFun := comap f\\n left_inv := comap_map_eq_of_injective (EquivLike.injective f)\\n right_inv := map_comap_eq_of_surjective (EquivLike.surjective f)\\n map_rel_iff' := map_le_map_iff_of_injective (EquivLike.injective f) _ _\",\n", - " 'start': [896, 1],\n", - " 'end': [903, 74],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_inf_eq_map_inf_comap',\n", - " 'code': \"theorem map_inf_eq_map_inf_comap [RingHomSurjective σ₁₂] {f : F} {p : Submodule R M}\\n {p' : Submodule R₂ M₂} : map f p ⊓ p' = map f (p ⊓ comap f p')\",\n", - " 'start': [911, 1],\n", - " 'end': [914, 73],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_comap_subtype',\n", - " 'code': \"theorem map_comap_subtype : map p.subtype (comap p.subtype p') = p ⊓ p'\",\n", - " 'start': [917, 1],\n", - " 'end': [918, 98],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.eq_zero_of_bot_submodule',\n", - " 'code': 'theorem eq_zero_of_bot_submodule : ∀ b : (⊥ : Submodule R M), b = 0',\n", - " 'start': [921, 1],\n", - " 'end': [922, 64],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.iInf_invariant',\n", - " 'code': 'theorem _root_.LinearMap.iInf_invariant {σ : R →+* R} [RingHomSurjective σ] {ι : Sort*}\\n (f : M →ₛₗ[σ] M) {p : ι → Submodule R M} (hf : ∀ i, ∀ v ∈ p i, f v ∈ p i) :\\n ∀ v ∈ iInf p, f v ∈ iInf p',\n", - " 'start': [925, 1],\n", - " 'end': [934, 75],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.neg_coe',\n", - " 'code': 'theorem neg_coe : -(p : Set M) = p',\n", - " 'start': [945, 1],\n", - " 'end': [946, 33],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_neg',\n", - " 'code': '@[simp]\\nprotected theorem map_neg (f : M →ₗ[R] M₂) : map (-f) p = map f p',\n", - " 'start': [949, 1],\n", - " 'end': [953, 86],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_smul',\n", - " 'code': 'theorem comap_smul (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K) (h : a ≠ 0) :\\n p.comap (a • f) = p.comap f',\n", - " 'start': [966, 1],\n", - " 'end': [968, 81],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_smul',\n", - " 'code': 'protected theorem map_smul (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K) (h : a ≠ 0) :\\n p.map (a • f) = p.map f',\n", - " 'start': [971, 1],\n", - " 'end': [974, 79],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"Submodule.comap_smul'\",\n", - " 'code': \"theorem comap_smul' (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K) :\\n p.comap (a • f) = ⨅ _ : a ≠ 0, p.comap f\",\n", - " 'start': [977, 1],\n", - " 'end': [979, 56],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"Submodule.map_smul'\",\n", - " 'code': \"theorem map_smul' (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K) :\\n p.map (a • f) = ⨆ _ : a ≠ 0, map f p\",\n", - " 'start': [982, 1],\n", - " 'end': [984, 64],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.coe_finsupp_sum',\n", - " 'code': 'theorem coe_finsupp_sum (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) :\\n ⇑(t.sum g) = t.sum fun i d => g i d',\n", - " 'start': [1010, 1],\n", - " 'end': [1011, 47],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.finsupp_sum_apply',\n", - " 'code': '@[simp]\\ntheorem finsupp_sum_apply (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) (b : M) :\\n (t.sum g) b = t.sum fun i d => g i d b',\n", - " 'start': [1014, 1],\n", - " 'end': [1017, 18],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.coe_dfinsupp_sum',\n", - " 'code': 'theorem coe_dfinsupp_sum (t : Π₀ i, γ i) (g : ∀ i, γ i → M →ₛₗ[σ₁₂] M₂) :\\n ⇑(t.sum g) = t.sum fun i d => g i d',\n", - " 'start': [1034, 1],\n", - " 'end': [1035, 47],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.dfinsupp_sum_apply',\n", - " 'code': '@[simp]\\ntheorem dfinsupp_sum_apply (t : Π₀ i, γ i) (g : ∀ i, γ i → M →ₛₗ[σ₁₂] M₂) (b : M) :\\n (t.sum g) b = t.sum fun i d => g i d b',\n", - " 'start': [1038, 1],\n", - " 'end': [1041, 18],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.map_dfinsupp_sumAddHom',\n", - " 'code': '@[simp]\\ntheorem map_dfinsupp_sumAddHom (f : M →ₛₗ[σ₁₂] M₂) {t : Π₀ i, γ i} {g : ∀ i, γ i →+ M} :\\n f (sumAddHom g t) = sumAddHom (fun i => f.toAddMonoidHom.comp (g i)) t',\n", - " 'start': [1050, 1],\n", - " 'end': [1053, 46],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.map_codRestrict',\n", - " 'code': \"theorem map_codRestrict [RingHomSurjective σ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (h p') :\\n Submodule.map (codRestrict p f h) p' = comap p.subtype (p'.map f)\",\n", - " 'start': [1064, 1],\n", - " 'end': [1066, 61],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.comap_codRestrict',\n", - " 'code': \"theorem comap_codRestrict (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (hf p') :\\n Submodule.comap (codRestrict p f hf) p' = Submodule.comap f (map p.subtype p')\",\n", - " 'start': [1069, 1],\n", - " 'end': [1071, 92],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range',\n", - " 'code': 'def range [RingHomSurjective τ₁₂] (f : F) : Submodule R₂ M₂ :=\\n (map f ⊤).copy (Set.range f) Set.image_univ.symm',\n", - " 'start': [1078, 1],\n", - " 'end': [1081, 51],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_coe',\n", - " 'code': 'theorem range_coe [RingHomSurjective τ₁₂] (f : F) : (range f : Set M₂) = Set.range f',\n", - " 'start': [1084, 1],\n", - " 'end': [1085, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_toAddSubmonoid',\n", - " 'code': 'theorem range_toAddSubmonoid [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :\\n f.range.toAddSubmonoid = AddMonoidHom.mrange f',\n", - " 'start': [1088, 1],\n", - " 'end': [1090, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.mem_range',\n", - " 'code': '@[simp]\\ntheorem mem_range [RingHomSurjective τ₁₂] {f : F} {x} : x ∈ range f ↔ ∃ y, f y = x',\n", - " 'start': [1093, 1],\n", - " 'end': [1095, 10],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_eq_map',\n", - " 'code': 'theorem range_eq_map [RingHomSurjective τ₁₂] (f : F) : range f = map f ⊤',\n", - " 'start': [1098, 1],\n", - " 'end': [1100, 7],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.mem_range_self',\n", - " 'code': 'theorem mem_range_self [RingHomSurjective τ₁₂] (f : F) (x : M) : f x ∈ range f',\n", - " 'start': [1103, 1],\n", - " 'end': [1104, 11],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_id',\n", - " 'code': '@[simp]\\ntheorem range_id : range (LinearMap.id : M →ₗ[R] M) = ⊤',\n", - " 'start': [1107, 1],\n", - " 'end': [1109, 37],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_comp',\n", - " 'code': 'theorem range_comp [RingHomSurjective τ₁₂] [RingHomSurjective τ₂₃] [RingHomSurjective τ₁₃]\\n (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : range (g.comp f : M →ₛₗ[τ₁₃] M₃) = map g (range f)',\n", - " 'start': [1112, 1],\n", - " 'end': [1114, 45],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_comp_le_range',\n", - " 'code': 'theorem range_comp_le_range [RingHomSurjective τ₂₃] [RingHomSurjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂)\\n (g : M₂ →ₛₗ[τ₂₃] M₃) : range (g.comp f : M →ₛₗ[τ₁₃] M₃) ≤ range g',\n", - " 'start': [1117, 1],\n", - " 'end': [1119, 53],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_eq_top',\n", - " 'code': 'theorem range_eq_top [RingHomSurjective τ₁₂] {f : F} : range f = ⊤ ↔ Surjective f',\n", - " 'start': [1122, 1],\n", - " 'end': [1123, 70],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_le_iff_comap',\n", - " 'code': 'theorem range_le_iff_comap [RingHomSurjective τ₁₂] {f : F} {p : Submodule R₂ M₂} :\\n range f ≤ p ↔ comap f p = ⊤',\n", - " 'start': [1126, 1],\n", - " 'end': [1127, 89],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.map_le_range',\n", - " 'code': 'theorem map_le_range [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} : map f p ≤ range f',\n", - " 'start': [1130, 1],\n", - " 'end': [1131, 48],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_neg',\n", - " 'code': '@[simp]\\ntheorem range_neg {R : Type*} {R₂ : Type*} {M : Type*} {M₂ : Type*} [Semiring R] [Ring R₂]\\n [AddCommMonoid M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂}\\n [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : LinearMap.range (-f) = LinearMap.range f',\n", - " 'start': [1134, 1],\n", - " 'end': [1139, 55],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_domRestrict_le_range',\n", - " 'code': 'lemma range_domRestrict_le_range [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (S : Submodule R M) :\\n LinearMap.range (f.domRestrict S) ≤ LinearMap.range f := by\\n rintro x ⟨⟨y, hy⟩, rfl⟩\\n exact LinearMap.mem_range_self f y',\n", - " 'start': [1142, 1],\n", - " 'end': [1145, 37],\n", - " 'kind': 'mathlibtacticlemma'},\n", - " {'full_name': 'AddMonoidHom.coe_toIntLinearMap_range',\n", - " 'code': '@[simp]\\ntheorem _root_.AddMonoidHom.coe_toIntLinearMap_range {M M₂ : Type*} [AddCommGroup M]\\n [AddCommGroup M₂] (f : M →+ M₂) :\\n LinearMap.range f.toIntLinearMap = AddSubgroup.toIntSubmodule f.range',\n", - " 'start': [1147, 1],\n", - " 'end': [1150, 81],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.eqLocus',\n", - " 'code': \"def eqLocus (f g : F) : Submodule R M :=\\n { (f : M →+ M₂).eqLocusM g with\\n carrier := { x | f x = g x }\\n smul_mem' := fun {r} {x} (hx : _ = _) => show _ = _ by\\n simpa only [map_smulₛₗ] using congr_arg ((· • ·) (τ₁₂ r)) hx }\",\n", - " 'start': [1152, 1],\n", - " 'end': [1157, 69],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.mem_eqLocus',\n", - " 'code': '@[simp]\\ntheorem mem_eqLocus {x : M} {f g : F} : x ∈ eqLocus f g ↔ f x = g x',\n", - " 'start': [1160, 1],\n", - " 'end': [1162, 10],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.eqLocus_toAddSubmonoid',\n", - " 'code': 'theorem eqLocus_toAddSubmonoid (f g : F) :\\n (eqLocus f g).toAddSubmonoid = (f : M →+ M₂).eqLocusM g',\n", - " 'start': [1165, 1],\n", - " 'end': [1167, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.eqLocus_eq_top',\n", - " 'code': '@[simp]\\ntheorem eqLocus_eq_top {f g : F} : eqLocus f g = ⊤ ↔ f = g',\n", - " 'start': [1170, 1],\n", - " 'end': [1172, 42],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.eqLocus_same',\n", - " 'code': '@[simp]\\ntheorem eqLocus_same (f : F) : eqLocus f f = ⊤',\n", - " 'start': [1174, 1],\n", - " 'end': [1175, 71],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.le_eqLocus',\n", - " 'code': 'theorem le_eqLocus {f g : F} {S : Submodule R M} : S ≤ eqLocus f g ↔ Set.EqOn f g S',\n", - " 'start': [1178, 1],\n", - " 'end': [1178, 95],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.eqOn_sup',\n", - " 'code': 'theorem eqOn_sup {f g : F} {S T : Submodule R M} (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) :\\n Set.EqOn f g ↑(S ⊔ T)',\n", - " 'start': [1180, 1],\n", - " 'end': [1183, 21],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ext_on_codisjoint',\n", - " 'code': 'theorem ext_on_codisjoint {f g : F} {S T : Submodule R M} (hST : Codisjoint S T)\\n (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) : f = g',\n", - " 'start': [1185, 1],\n", - " 'end': [1187, 70],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.iterateRange',\n", - " 'code': \"@[simps]\\ndef iterateRange (f : M →ₗ[R] M) : ℕ →o (Submodule R M)ᵒᵈ where\\n toFun n := LinearMap.range (f ^ n)\\n monotone' n m w x h := by\\n obtain ⟨c, rfl⟩ := le_iff_exists_add.mp w\\n rw [LinearMap.mem_range] at h\\n obtain ⟨m, rfl⟩ := h\\n rw [LinearMap.mem_range]\\n use (f ^ c) m\\n rw [pow_add, LinearMap.mul_apply]\",\n", - " 'start': [1191, 1],\n", - " 'end': [1202, 38],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.rangeRestrict',\n", - " 'code': '@[reducible]\\ndef rangeRestrict [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : M →ₛₗ[τ₁₂] LinearMap.range f :=\\n f.codRestrict (LinearMap.range f) (LinearMap.mem_range_self f)',\n", - " 'start': [1205, 1],\n", - " 'end': [1210, 65],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.fintypeRange',\n", - " 'code': 'instance fintypeRange [Fintype M] [DecidableEq M₂] [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :\\n Fintype (range f) :=\\n Set.fintypeRange f',\n", - " 'start': [1213, 1],\n", - " 'end': [1218, 21],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker',\n", - " 'code': 'def ker (f : F) : Submodule R M :=\\n comap f ⊥',\n", - " 'start': [1223, 1],\n", - " 'end': [1226, 12],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.mem_ker',\n", - " 'code': '@[simp]\\ntheorem mem_ker {f : F} {y} : y ∈ ker f ↔ f y = 0',\n", - " 'start': [1229, 1],\n", - " 'end': [1231, 13],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_id',\n", - " 'code': '@[simp]\\ntheorem ker_id : ker (LinearMap.id : M →ₗ[R] M) = ⊥',\n", - " 'start': [1234, 1],\n", - " 'end': [1236, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.map_coe_ker',\n", - " 'code': '@[simp]\\ntheorem map_coe_ker (f : F) (x : ker f) : f x = 0',\n", - " 'start': [1239, 1],\n", - " 'end': [1241, 16],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_toAddSubmonoid',\n", - " 'code': 'theorem ker_toAddSubmonoid (f : M →ₛₗ[τ₁₂] M₂) : f.ker.toAddSubmonoid = (AddMonoidHom.mker f)',\n", - " 'start': [1244, 1],\n", - " 'end': [1245, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.comp_ker_subtype',\n", - " 'code': 'theorem comp_ker_subtype (f : M →ₛₗ[τ₁₂] M₂) : f.comp f.ker.subtype = 0',\n", - " 'start': [1248, 1],\n", - " 'end': [1249, 39],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_comp',\n", - " 'code': 'theorem ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :\\n ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = comap f (ker g)',\n", - " 'start': [1252, 1],\n", - " 'end': [1254, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_le_ker_comp',\n", - " 'code': 'theorem ker_le_ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :\\n ker f ≤ ker (g.comp f : M →ₛₗ[τ₁₃] M₃)',\n", - " 'start': [1257, 1],\n", - " 'end': [1258, 88],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.disjoint_ker',\n", - " 'code': 'theorem disjoint_ker {f : F} {p : Submodule R M} : Disjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0',\n", - " 'start': [1261, 1],\n", - " 'end': [1262, 25],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearMap.ker_eq_bot'\",\n", - " 'code': \"theorem ker_eq_bot' {f : F} : ker f = ⊥ ↔ ∀ m, f m = 0 → m = 0\",\n", - " 'start': [1265, 1],\n", - " 'end': [1266, 80],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_eq_bot_of_inverse',\n", - " 'code': 'theorem ker_eq_bot_of_inverse {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂}\\n {g : M₂ →ₛₗ[τ₂₁] M} (h : (g.comp f : M →ₗ[R] M) = id) : ker f = ⊥',\n", - " 'start': [1269, 1],\n", - " 'end': [1271, 91],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.le_ker_iff_map',\n", - " 'code': 'theorem le_ker_iff_map [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} :\\n p ≤ ker f ↔ map f p = ⊥',\n", - " 'start': [1274, 1],\n", - " 'end': [1275, 76],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_codRestrict',\n", - " 'code': 'theorem ker_codRestrict {τ₂₁ : R₂ →+* R} (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf) :\\n ker (codRestrict p f hf) = ker f',\n", - " 'start': [1278, 1],\n", - " 'end': [1279, 95],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_codRestrict',\n", - " 'code': 'theorem range_codRestrict {τ₂₁ : R₂ →+* R} [RingHomSurjective τ₂₁] (p : Submodule R M)\\n (f : M₂ →ₛₗ[τ₂₁] M) (hf) :\\n range (codRestrict p f hf) = comap p.subtype (LinearMap.range f)',\n", - " 'start': [1282, 1],\n", - " 'end': [1285, 58],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_restrict',\n", - " 'code': 'theorem ker_restrict [AddCommMonoid M₁] [Module R M₁] {p : Submodule R M} {q : Submodule R M₁}\\n {f : M →ₗ[R] M₁} (hf : ∀ x : M, x ∈ p → f x ∈ q) :\\n ker (f.restrict hf) = LinearMap.ker (f.domRestrict p)',\n", - " 'start': [1288, 1],\n", - " 'end': [1291, 60],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_comap_eq',\n", - " 'code': 'theorem _root_.Submodule.map_comap_eq [RingHomSurjective τ₁₂] (f : F) (q : Submodule R₂ M₂) :\\n map f (comap f q) = range f ⊓ q',\n", - " 'start': [1294, 1],\n", - " 'end': [1297, 51],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_comap_eq_self',\n", - " 'code': 'theorem _root_.Submodule.map_comap_eq_self [RingHomSurjective τ₁₂] {f : F} {q : Submodule R₂ M₂}\\n (h : q ≤ range f) : map f (comap f q) = q',\n", - " 'start': [1300, 1],\n", - " 'end': [1301, 95],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_zero',\n", - " 'code': '@[simp]\\ntheorem ker_zero : ker (0 : M →ₛₗ[τ₁₂] M₂) = ⊤',\n", - " 'start': [1304, 1],\n", - " 'end': [1306, 33],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_zero',\n", - " 'code': '@[simp]\\ntheorem range_zero [RingHomSurjective τ₁₂] : range (0 : M →ₛₗ[τ₁₂] M₂) = ⊥',\n", - " 'start': [1309, 1],\n", - " 'end': [1311, 55],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_eq_top',\n", - " 'code': 'theorem ker_eq_top {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊤ ↔ f = 0',\n", - " 'start': [1314, 1],\n", - " 'end': [1315, 84],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'AddMonoidHom.coe_toIntLinearMap_ker',\n", - " 'code': '@[simp]\\ntheorem _root_.AddMonoidHom.coe_toIntLinearMap_ker {M M₂ : Type*} [AddCommGroup M] [AddCommGroup M₂]\\n (f : M →+ M₂) : LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker',\n", - " 'start': [1318, 1],\n", - " 'end': [1320, 93],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_le_bot_iff',\n", - " 'code': 'theorem range_le_bot_iff (f : M →ₛₗ[τ₁₂] M₂) : range f ≤ ⊥ ↔ f = 0',\n", - " 'start': [1326, 1],\n", - " 'end': [1327, 44],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_eq_bot',\n", - " 'code': 'theorem range_eq_bot {f : M →ₛₗ[τ₁₂] M₂} : range f = ⊥ ↔ f = 0',\n", - " 'start': [1330, 1],\n", - " 'end': [1331, 38],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_le_ker_iff',\n", - " 'code': 'theorem range_le_ker_iff {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} :\\n range f ≤ ker g ↔ (g.comp f : M →ₛₗ[τ₁₃] M₃) = 0',\n", - " 'start': [1334, 1],\n", - " 'end': [1337, 87],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.comap_le_comap_iff',\n", - " 'code': \"theorem comap_le_comap_iff {f : F} (hf : range f = ⊤) {p p'} : comap f p ≤ comap f p' ↔ p ≤ p'\",\n", - " 'start': [1340, 1],\n", - " 'end': [1341, 90],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.comap_injective',\n", - " 'code': 'theorem comap_injective {f : F} (hf : range f = ⊤) : Injective (comap f)',\n", - " 'start': [1344, 1],\n", - " 'end': [1345, 96],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_eq_bot_of_injective',\n", - " 'code': 'theorem ker_eq_bot_of_injective {f : F} (hf : Injective f) : ker f = ⊥',\n", - " 'start': [1350, 1],\n", - " 'end': [1357, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.iterateKer',\n", - " 'code': \"@[simps]\\ndef iterateKer (f : M →ₗ[R] M) : ℕ →o Submodule R M where\\n toFun n := ker (f ^ n)\\n monotone' n m w x h := by\\n obtain ⟨c, rfl⟩ := le_iff_exists_add.mp w\\n rw [LinearMap.mem_ker] at h\\n rw [LinearMap.mem_ker, add_comm, pow_add, LinearMap.mul_apply, h, LinearMap.map_zero]\",\n", - " 'start': [1360, 1],\n", - " 'end': [1368, 90],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_toAddSubgroup',\n", - " 'code': 'theorem range_toAddSubgroup [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :\\n (range f).toAddSubgroup = f.toAddMonoidHom.range',\n", - " 'start': [1385, 1],\n", - " 'end': [1387, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_toAddSubgroup',\n", - " 'code': 'theorem ker_toAddSubgroup (f : M →ₛₗ[τ₁₂] M₂) : (ker f).toAddSubgroup = f.toAddMonoidHom.ker',\n", - " 'start': [1390, 1],\n", - " 'end': [1391, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.eqLocus_eq_ker_sub',\n", - " 'code': 'theorem eqLocus_eq_ker_sub (f g : M →ₛₗ[τ₁₂] M₂) : eqLocus f g = ker (f - g)',\n", - " 'start': [1394, 1],\n", - " 'end': [1395, 40],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.sub_mem_ker_iff',\n", - " 'code': 'theorem sub_mem_ker_iff {x y} : x - y ∈ ker f ↔ f x = f y',\n", - " 'start': [1398, 1],\n", - " 'end': [1398, 99],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearMap.disjoint_ker'\",\n", - " 'code': \"theorem disjoint_ker' {p : Submodule R M} :\\n Disjoint p (ker f) ↔ ∀ x ∈ p, ∀ y ∈ p, f x = f y → x = y\",\n", - " 'start': [1401, 1],\n", - " 'end': [1405, 65],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.injOn_of_disjoint_ker',\n", - " 'code': 'theorem injOn_of_disjoint_ker {p : Submodule R M} {s : Set M} (h : s ⊆ p)\\n (hd : Disjoint p (ker f)) : Set.InjOn f s',\n", - " 'start': [1408, 1],\n", - " 'end': [1410, 39],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMapClass.ker_eq_bot',\n", - " 'code': 'theorem _root_.LinearMapClass.ker_eq_bot : ker f = ⊥ ↔ Injective f',\n", - " 'start': [1415, 1],\n", - " 'end': [1416, 81],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_eq_bot',\n", - " 'code': 'theorem ker_eq_bot {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊥ ↔ Injective f',\n", - " 'start': [1421, 1],\n", - " 'end': [1422, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_le_iff',\n", - " 'code': \"theorem ker_le_iff [RingHomSurjective τ₁₂] {p : Submodule R M} :\\n ker f ≤ p ↔ ∃ y ∈ range f, f ⁻¹' {y} ⊆ p\",\n", - " 'start': [1425, 1],\n", - " 'end': [1443, 28],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.injective_domRestrict_iff',\n", - " 'code': \"@[simp] lemma injective_domRestrict_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :\\n Injective (f.domRestrict S) ↔ S ⊓ LinearMap.ker f = ⊥ := by\\n rw [← LinearMap.ker_eq_bot]\\n refine ⟨fun h ↦ le_bot_iff.1 ?_, fun h ↦ le_bot_iff.1 ?_⟩\\n · intro x ⟨hx, h'x⟩\\n have : ⟨x, hx⟩ ∈ LinearMap.ker (LinearMap.domRestrict f S) := by simpa using h'x\\n rw [h] at this\\n simpa using this\\n · rintro ⟨x, hx⟩ h'x\\n have : x ∈ S ⊓ LinearMap.ker f := ⟨hx, h'x⟩\\n rw [h] at this\\n simpa using this\",\n", - " 'start': [1446, 1],\n", - " 'end': [1457, 21],\n", - " 'kind': 'mathlibtacticlemma'},\n", - " {'full_name': 'LinearMap.ker_smul',\n", - " 'code': 'theorem ker_smul (f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) : ker (a • f) = ker f',\n", - " 'start': [1467, 1],\n", - " 'end': [1468, 31],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearMap.ker_smul'\",\n", - " 'code': \"theorem ker_smul' (f : V →ₗ[K] V₂) (a : K) : ker (a • f) = ⨅ _ : a ≠ 0, ker f\",\n", - " 'start': [1471, 1],\n", - " 'end': [1472, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_smul',\n", - " 'code': 'theorem range_smul (f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) : range (a • f) = range f',\n", - " 'start': [1475, 1],\n", - " 'end': [1476, 61],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearMap.range_smul'\",\n", - " 'code': \"theorem range_smul' (f : V →ₗ[K] V₂) (a : K) :\\n range (a • f) = ⨆ _ : a ≠ 0, range f\",\n", - " 'start': [1479, 1],\n", - " 'end': [1481, 60],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'IsLinearMap.isLinearMap_add',\n", - " 'code': 'theorem isLinearMap_add [Semiring R] [AddCommMonoid M] [Module R M] :\\n IsLinearMap R fun x : M × M => x.1 + x.2',\n", - " 'start': [1490, 1],\n", - " 'end': [1497, 20],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'IsLinearMap.isLinearMap_sub',\n", - " 'code': 'theorem isLinearMap_sub {R M : Type*} [Semiring R] [AddCommGroup M] [Module R M] :\\n IsLinearMap R fun x : M × M => x.1 - x.2',\n", - " 'start': [1500, 1],\n", - " 'end': [1508, 20],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_top',\n", - " 'code': '@[simp]\\ntheorem map_top [RingHomSurjective τ₁₂] (f : F) : map f ⊤ = range f',\n", - " 'start': [1529, 1],\n", - " 'end': [1531, 24],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_bot',\n", - " 'code': '@[simp]\\ntheorem comap_bot (f : F) : comap f ⊥ = ker f',\n", - " 'start': [1534, 1],\n", - " 'end': [1536, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.ker_subtype',\n", - " 'code': '@[simp]\\ntheorem ker_subtype : ker p.subtype = ⊥',\n", - " 'start': [1539, 1],\n", - " 'end': [1541, 53],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.range_subtype',\n", - " 'code': '@[simp]\\ntheorem range_subtype : range p.subtype = p',\n", - " 'start': [1544, 1],\n", - " 'end': [1545, 84],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_subtype_le',\n", - " 'code': \"theorem map_subtype_le (p' : Submodule R p) : map p.subtype p' ≤ p\",\n", - " 'start': [1548, 1],\n", - " 'end': [1549, 66],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_subtype_top',\n", - " 'code': 'theorem map_subtype_top : map p.subtype (⊤ : Submodule R p) = p',\n", - " 'start': [1552, 1],\n", - " 'end': [1555, 75],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_subtype_eq_top',\n", - " 'code': \"@[simp]\\ntheorem comap_subtype_eq_top {p p' : Submodule R M} : comap p.subtype p' = ⊤ ↔ p ≤ p'\",\n", - " 'start': [1558, 1],\n", - " 'end': [1560, 80],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_subtype_self',\n", - " 'code': '@[simp]\\ntheorem comap_subtype_self : comap p.subtype p = ⊤',\n", - " 'start': [1563, 1],\n", - " 'end': [1565, 32],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.ker_ofLe',\n", - " 'code': \"@[simp]\\ntheorem ker_ofLe (p p' : Submodule R M) (h : p ≤ p') : ker (ofLe h) = ⊥\",\n", - " 'start': [1568, 1],\n", - " 'end': [1570, 42],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.range_ofLe',\n", - " 'code': 'theorem range_ofLe (p q : Submodule R M) (h : p ≤ q) : range (ofLe h) = comap q.subtype p',\n", - " 'start': [1573, 1],\n", - " 'end': [1574, 74],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_subtype_range_ofLe',\n", - " 'code': \"@[simp]\\ntheorem map_subtype_range_ofLe {p p' : Submodule R M} (h : p ≤ p') :\\n map p'.subtype (range $ ofLe h) = p\",\n", - " 'start': [1577, 1],\n", - " 'end': [1579, 81],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.disjoint_iff_comap_eq_bot',\n", - " 'code': 'theorem disjoint_iff_comap_eq_bot {p q : Submodule R M} : Disjoint p q ↔ comap p.subtype q = ⊥',\n", - " 'start': [1582, 1],\n", - " 'end': [1584, 46],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.MapSubtype.relIso',\n", - " 'code': \"def MapSubtype.relIso : Submodule R p ≃o { p' : Submodule R M // p' ≤ p } where\\n toFun p' := ⟨map p.subtype p', map_subtype_le p _⟩\\n invFun q := comap p.subtype q\\n left_inv p' := comap_map_eq_of_injective (by exact Subtype.val_injective) p'\\n right_inv := fun ⟨q, hq⟩ => Subtype.ext_val <| by simp [map_comap_subtype p, inf_of_le_right hq]\\n map_rel_iff' {p₁ p₂} := Subtype.coe_le_coe.symm.trans $ by\\n dsimp\\n rw [map_le_iff_le_comap,\\n comap_map_eq_of_injective (show Injective p.subtype from Subtype.coe_injective) p₂]\",\n", - " 'start': [1587, 1],\n", - " 'end': [1596, 90],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.MapSubtype.orderEmbedding',\n", - " 'code': \"def MapSubtype.orderEmbedding : Submodule R p ↪o Submodule R M :=\\n (RelIso.toRelEmbedding <| MapSubtype.relIso p).trans $\\n Subtype.relEmbedding (X := Submodule R M) (fun p p' ↦ p ≤ p') _\",\n", - " 'start': [1599, 1],\n", - " 'end': [1603, 68],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_subtype_embedding_eq',\n", - " 'code': \"@[simp]\\ntheorem map_subtype_embedding_eq (p' : Submodule R p) :\\n MapSubtype.orderEmbedding p p' = map p.subtype p'\",\n", - " 'start': [1606, 1],\n", - " 'end': [1609, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_eq_bot_of_cancel',\n", - " 'code': 'theorem ker_eq_bot_of_cancel {f : M →ₛₗ[τ₁₂] M₂}\\n (h : ∀ u v : ker f →ₗ[R] M, f.comp u = f.comp v → u = v) : ker f = ⊥',\n", - " 'start': [1630, 1],\n", - " 'end': [1636, 19],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_comp_of_range_eq_top',\n", - " 'code': 'theorem range_comp_of_range_eq_top [RingHomSurjective τ₁₂] [RingHomSurjective τ₂₃]\\n [RingHomSurjective τ₁₃] {f : M →ₛₗ[τ₁₂] M₂} (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : range f = ⊤) :\\n range (g.comp f : M →ₛₗ[τ₁₃] M₃) = range g',\n", - " 'start': [1639, 1],\n", - " 'end': [1641, 92],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_comp_of_ker_eq_bot',\n", - " 'code': 'theorem ker_comp_of_ker_eq_bot (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : ker g = ⊥) :\\n ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = ker f',\n", - " 'start': [1644, 1],\n", - " 'end': [1645, 88],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.submoduleImage',\n", - " 'code': \"def submoduleImage {M' : Type*} [AddCommMonoid M'] [Module R M'] {O : Submodule R M}\\n (ϕ : O →ₗ[R] M') (N : Submodule R M) : Submodule R M' :=\\n (N.comap O.subtype).map ϕ\",\n", - " 'start': [1650, 1],\n", - " 'end': [1654, 28],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.mem_submoduleImage',\n", - " 'code': \"@[simp]\\ntheorem mem_submoduleImage {M' : Type*} [AddCommMonoid M'] [Module R M'] {O : Submodule R M}\\n {ϕ : O →ₗ[R] M'} {N : Submodule R M} {x : M'} :\\n x ∈ ϕ.submoduleImage N ↔ ∃ (y : _) (yO : y ∈ O) (_ : y ∈ N), ϕ ⟨y, yO⟩ = x\",\n", - " 'start': [1657, 1],\n", - " 'end': [1665, 27],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.mem_submoduleImage_of_le',\n", - " 'code': \"theorem mem_submoduleImage_of_le {M' : Type*} [AddCommMonoid M'] [Module R M'] {O : Submodule R M}\\n {ϕ : O →ₗ[R] M'} {N : Submodule R M} (hNO : N ≤ O) {x : M'} :\\n x ∈ ϕ.submoduleImage N ↔ ∃ (y : _) (yN : y ∈ N), ϕ ⟨y, hNO yN⟩ = x\",\n", - " 'start': [1668, 1],\n", - " 'end': [1675, 29],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.submoduleImage_apply_ofLe',\n", - " 'code': \"theorem submoduleImage_apply_ofLe {M' : Type*} [AddCommGroup M'] [Module R M'] {O : Submodule R M}\\n (ϕ : O →ₗ[R] M') (N : Submodule R M) (hNO : N ≤ O) :\\n ϕ.submoduleImage N = range (ϕ.comp (Submodule.ofLe hNO))\",\n", - " 'start': [1678, 1],\n", - " 'end': [1681, 56],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.range_rangeRestrict',\n", - " 'code': '@[simp]\\ntheorem LinearMap.range_rangeRestrict [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M]\\n [Module R M₂] (f : M →ₗ[R] M₂) : range f.rangeRestrict = ⊤',\n", - " 'start': [1690, 1],\n", - " 'end': [1692, 98],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.ker_rangeRestrict',\n", - " 'code': '@[simp]\\ntheorem LinearMap.ker_rangeRestrict [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M]\\n [Module R M₂] (f : M →ₗ[R] M₂) : ker f.rangeRestrict = ker f',\n", - " 'start': [1695, 1],\n", - " 'end': [1698, 34],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.zero_symm',\n", - " 'code': '@[simp]\\ntheorem zero_symm : (0 : M ≃ₛₗ[σ₁₂] M₂).symm = 0',\n", - " 'start': [1734, 1],\n", - " 'end': [1736, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.coe_zero',\n", - " 'code': '@[simp]\\ntheorem coe_zero : ⇑(0 : M ≃ₛₗ[σ₁₂] M₂) = 0',\n", - " 'start': [1739, 1],\n", - " 'end': [1741, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.zero_apply',\n", - " 'code': 'theorem zero_apply (x : M) : (0 : M ≃ₛₗ[σ₁₂] M₂) x = 0',\n", - " 'start': [1744, 1],\n", - " 'end': [1745, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.uniqueOfSubsingleton',\n", - " 'code': 'instance uniqueOfSubsingleton [Subsingleton R] [Subsingleton R₂] : Unique (M ≃ₛₗ[σ₁₂] M₂) := by\\n haveI := Module.subsingleton R M\\n haveI := Module.subsingleton R₂ M₂\\n infer_instance',\n", - " 'start': [1756, 1],\n", - " 'end': [1759, 17],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.map_eq_comap',\n", - " 'code': 'theorem map_eq_comap {p : Submodule R M} :\\n (p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂) = p.comap (e.symm : M₂ →ₛₗ[σ₂₁] M)',\n", - " 'start': [1780, 1],\n", - " 'end': [1782, 57],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.submoduleMap',\n", - " 'code': \"def submoduleMap (p : Submodule R M) : p ≃ₛₗ[σ₁₂] ↥(p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂) :=\\n { ((e : M →ₛₗ[σ₁₂] M₂).domRestrict p).codRestrict (p.map (e : M →ₛₗ[σ₁₂] M₂)) fun x =>\\n ⟨x, by\\n simp only [LinearMap.domRestrict_apply, eq_self_iff_true, and_true_iff, SetLike.coe_mem,\\n SetLike.mem_coe]⟩ with\\n invFun := fun y =>\\n ⟨(e.symm : M₂ →ₛₗ[σ₂₁] M) y, by\\n rcases y with ⟨y', hy⟩\\n rw [Submodule.mem_map] at hy\\n rcases hy with ⟨x, hx, hxy⟩\\n subst hxy\\n simp only [symm_apply_apply, Submodule.coe_mk, coe_coe, hx]⟩\\n left_inv := fun x => by\\n simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe,\\n LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, SetLike.eta]\\n right_inv := fun y => by\\n apply SetCoe.ext\\n simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe,\\n LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply] }\",\n", - " 'start': [1785, 1],\n", - " 'end': [1809, 61],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.submoduleMap_apply',\n", - " 'code': '@[simp]\\ntheorem submoduleMap_apply (p : Submodule R M) (x : p) : ↑(e.submoduleMap p x) = e x',\n", - " 'start': [1813, 1],\n", - " 'end': [1815, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.submoduleMap_symm_apply',\n", - " 'code': '@[simp]\\ntheorem submoduleMap_symm_apply (p : Submodule R M)\\n (x : (p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂)) : ↑((e.submoduleMap p).symm x) = e.symm x',\n", - " 'start': [1818, 1],\n", - " 'end': [1821, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.map_dfinsupp_sumAddHom',\n", - " 'code': '@[simp]\\ntheorem map_dfinsupp_sumAddHom [∀ i, AddZeroClass (γ i)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ i, γ i)\\n (g : ∀ i, γ i →+ M) :\\n f (sumAddHom g t) = sumAddHom (fun i => f.toAddEquiv.toAddMonoidHom.comp (g i)) t',\n", - " 'start': [1852, 1],\n", - " 'end': [1856, 42],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.curry',\n", - " 'code': \"protected def curry : (V × V₂ → R) ≃ₗ[R] V → V₂ → R :=\\n { Equiv.curry _ _ _ with\\n map_add' := fun _ _ => by\\n ext\\n rfl\\n map_smul' := fun _ _ => by\\n ext\\n rfl }\",\n", - " 'start': [1869, 1],\n", - " 'end': [1878, 12],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.coe_curry',\n", - " 'code': '@[simp]\\ntheorem coe_curry : ⇑(LinearEquiv.curry R V V₂) = curry',\n", - " 'start': [1881, 1],\n", - " 'end': [1883, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.coe_curry_symm',\n", - " 'code': '@[simp]\\ntheorem coe_curry_symm : ⇑(LinearEquiv.curry R V V₂).symm = uncurry',\n", - " 'start': [1886, 1],\n", - " 'end': [1888, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofEq',\n", - " 'code': \"def ofEq (h : p = q) : p ≃ₗ[R] q :=\\n { Equiv.Set.ofEq (congr_arg _ h) with\\n map_smul' := fun _ _ => rfl\\n map_add' := fun _ _ => rfl }\",\n", - " 'start': [1917, 1],\n", - " 'end': [1921, 33],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.coe_ofEq_apply',\n", - " 'code': '@[simp]\\ntheorem coe_ofEq_apply (h : p = q) (x : p) : (ofEq p q h x : M) = x',\n", - " 'start': [1926, 1],\n", - " 'end': [1928, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofEq_symm',\n", - " 'code': '@[simp]\\ntheorem ofEq_symm (h : p = q) : (ofEq p q h).symm = ofEq q p h.symm',\n", - " 'start': [1931, 1],\n", - " 'end': [1933, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofEq_rfl',\n", - " 'code': '@[simp]\\ntheorem ofEq_rfl : ofEq p p rfl = LinearEquiv.refl R p',\n", - " 'start': [1936, 1],\n", - " 'end': [1937, 70],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofSubmodules',\n", - " 'code': 'def ofSubmodules (p : Submodule R M) (q : Submodule R₂ M₂) (h : p.map (e : M →ₛₗ[σ₁₂] M₂) = q) :\\n p ≃ₛₗ[σ₁₂] q :=\\n (e.submoduleMap p).trans (LinearEquiv.ofEq _ _ h)',\n", - " 'start': [1940, 1],\n", - " 'end': [1944, 52],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofSubmodules_apply',\n", - " 'code': '@[simp]\\ntheorem ofSubmodules_apply {p : Submodule R M} {q : Submodule R₂ M₂} (h : p.map ↑e = q) (x : p) :\\n ↑(e.ofSubmodules p q h x) = e x',\n", - " 'start': [1947, 1],\n", - " 'end': [1950, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofSubmodules_symm_apply',\n", - " 'code': '@[simp]\\ntheorem ofSubmodules_symm_apply {p : Submodule R M} {q : Submodule R₂ M₂} (h : p.map ↑e = q)\\n (x : q) : ↑((e.ofSubmodules p q h).symm x) = e.symm x',\n", - " 'start': [1953, 1],\n", - " 'end': [1956, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearEquiv.ofSubmodule'\",\n", - " 'code': \"def ofSubmodule' [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) :\\n U.comap (f : M →ₛₗ[σ₁₂] M₂) ≃ₛₗ[σ₁₂] U :=\\n (f.symm.ofSubmodules _ _ f.symm.map_eq_comap).symm\",\n", - " 'start': [1959, 1],\n", - " 'end': [1965, 53],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearEquiv.ofSubmodule'_toLinearMap\",\n", - " 'code': \"theorem ofSubmodule'_toLinearMap [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂)\\n (U : Submodule R₂ M₂) :\\n (f.ofSubmodule' U).toLinearMap = (f.toLinearMap.domRestrict _).codRestrict _ Subtype.prop\",\n", - " 'start': [1968, 1],\n", - " 'end': [1972, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearEquiv.ofSubmodule'_apply\",\n", - " 'code': \"@[simp]\\ntheorem ofSubmodule'_apply [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂)\\n (x : U.comap (f : M →ₛₗ[σ₁₂] M₂)) : (f.ofSubmodule' U x : M₂) = f (x : M)\",\n", - " 'start': [1975, 1],\n", - " 'end': [1978, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"LinearEquiv.ofSubmodule'_symm_apply\",\n", - " 'code': \"@[simp]\\ntheorem ofSubmodule'_symm_apply [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂)\\n (U : Submodule R₂ M₂) (x : U) : ((f.ofSubmodule' U).symm x : M) = f.symm (x : M₂)\",\n", - " 'start': [1981, 1],\n", - " 'end': [1984, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofTop',\n", - " 'code': 'def ofTop (h : p = ⊤) : p ≃ₗ[R] M :=\\n { p.subtype with\\n invFun := fun x => ⟨x, h.symm ▸ trivial⟩\\n left_inv := fun _ => rfl\\n right_inv := fun _ => rfl }',\n", - " 'start': [1989, 1],\n", - " 'end': [1994, 32],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofTop_apply',\n", - " 'code': '@[simp]\\ntheorem ofTop_apply {h} (x : p) : ofTop p h x = x',\n", - " 'start': [1997, 1],\n", - " 'end': [1999, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.coe_ofTop_symm_apply',\n", - " 'code': '@[simp]\\ntheorem coe_ofTop_symm_apply {h} (x : M) : ((ofTop p h).symm x : M) = x',\n", - " 'start': [2002, 1],\n", - " 'end': [2004, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofTop_symm_apply',\n", - " 'code': 'theorem ofTop_symm_apply {h} (x : M) : (ofTop p h).symm x = ⟨x, h.symm ▸ trivial⟩',\n", - " 'start': [2007, 1],\n", - " 'end': [2008, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofLinear',\n", - " 'code': 'def ofLinear (h₁ : f.comp g = LinearMap.id) (h₂ : g.comp f = LinearMap.id) : M ≃ₛₗ[σ₁₂] M₂ :=\\n { f with\\n invFun := g\\n left_inv := LinearMap.ext_iff.1 h₂\\n right_inv := LinearMap.ext_iff.1 h₁ }',\n", - " 'start': [2011, 1],\n", - " 'end': [2016, 42],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofLinear_apply',\n", - " 'code': '@[simp]\\ntheorem ofLinear_apply {h₁ h₂} (x : M) : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) x = f x',\n", - " 'start': [2019, 1],\n", - " 'end': [2021, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofLinear_symm_apply',\n", - " 'code': '@[simp]\\ntheorem ofLinear_symm_apply {h₁ h₂} (x : M₂) : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm x = g x',\n", - " 'start': [2024, 1],\n", - " 'end': [2026, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.range',\n", - " 'code': '@[simp]\\nprotected theorem range : LinearMap.range (e : M →ₛₗ[σ₁₂] M₂) = ⊤',\n", - " 'start': [2029, 1],\n", - " 'end': [2031, 48],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquivClass.range',\n", - " 'code': '@[simp]\\nprotected theorem _root_.LinearEquivClass.range [Module R M] [Module R₂ M₂] {F : Type*}\\n [SemilinearEquivClass F σ₁₂ M M₂] (e : F) : LinearMap.range e = ⊤',\n", - " 'start': [2034, 1],\n", - " 'end': [2037, 52],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.eq_bot_of_equiv',\n", - " 'code': 'theorem eq_bot_of_equiv [Module R₂ M₂] (e : p ≃ₛₗ[σ₁₂] (⊥ : Submodule R₂ M₂)) : p = ⊥',\n", - " 'start': [2040, 1],\n", - " 'end': [2043, 43],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ker',\n", - " 'code': '@[simp]\\nprotected theorem ker : LinearMap.ker (e : M →ₛₗ[σ₁₂] M₂) = ⊥',\n", - " 'start': [2046, 1],\n", - " 'end': [2048, 56],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.range_comp',\n", - " 'code': '@[simp]\\ntheorem range_comp [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] :\\n LinearMap.range (h.comp (e : M →ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₃] M₃) = LinearMap.range h',\n", - " 'start': [2052, 1],\n", - " 'end': [2055, 49],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ker_comp',\n", - " 'code': \"@[simp]\\ntheorem ker_comp (l : M →ₛₗ[σ₁₂] M₂) :\\n LinearMap.ker (((e'' : M₂ →ₛₗ[σ₂₃] M₃).comp l : M →ₛₗ[σ₁₃] M₃) : M →ₛₗ[σ₁₃] M₃) =\\n LinearMap.ker l\",\n", - " 'start': [2058, 1],\n", - " 'end': [2062, 45],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofLeftInverse',\n", - " 'code': \"def ofLeftInverse [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {g : M₂ → M}\\n (h : Function.LeftInverse g f) : M ≃ₛₗ[σ₁₂] (LinearMap.range f) :=\\n { LinearMap.rangeRestrict f with\\n toFun := LinearMap.rangeRestrict f\\n invFun := g ∘ (LinearMap.range f).subtype\\n left_inv := h\\n right_inv := fun x =>\\n Subtype.ext <|\\n let ⟨x', hx'⟩ := LinearMap.mem_range.mp x.prop\\n show f (g x) = x by rw [← hx', h x'] }\",\n", - " 'start': [2067, 1],\n", - " 'end': [2081, 47],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofLeftInverse_apply',\n", - " 'code': '@[simp]\\ntheorem ofLeftInverse_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]\\n (h : Function.LeftInverse g f) (x : M) : ↑(ofLeftInverse h x) = f x',\n", - " 'start': [2084, 1],\n", - " 'end': [2087, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofLeftInverse_symm_apply',\n", - " 'code': '@[simp]\\ntheorem ofLeftInverse_symm_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]\\n (h : Function.LeftInverse g f) (x : LinearMap.range f) : (ofLeftInverse h).symm x = g x',\n", - " 'start': [2090, 1],\n", - " 'end': [2093, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofInjective',\n", - " 'code': 'noncomputable def ofInjective [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Injective f) :\\n M ≃ₛₗ[σ₁₂] LinearMap.range f :=\\n ofLeftInverse <| Classical.choose_spec h.hasLeftInverse',\n", - " 'start': [2098, 1],\n", - " 'end': [2102, 58],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofInjective_apply',\n", - " 'code': '@[simp]\\ntheorem ofInjective_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Injective f}\\n (x : M) : ↑(ofInjective f h x) = f x',\n", - " 'start': [2105, 1],\n", - " 'end': [2108, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofBijective',\n", - " 'code': 'noncomputable def ofBijective [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (hf : Bijective f) :\\n M ≃ₛₗ[σ₁₂] M₂ :=\\n (ofInjective f hf.injective).trans (ofTop _ <| LinearMap.range_eq_top.2 hf.surjective)',\n", - " 'start': [2111, 1],\n", - " 'end': [2114, 89],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.ofBijective_apply',\n", - " 'code': '@[simp]\\ntheorem ofBijective_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {hf} (x : M) :\\n ofBijective f hf x = f x',\n", - " 'start': [2117, 1],\n", - " 'end': [2120, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.map_neg',\n", - " 'code': 'theorem map_neg (a : M) : e (-a) = -e a',\n", - " 'start': [2148, 1],\n", - " 'end': [2149, 26],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.map_sub',\n", - " 'code': 'theorem map_sub (a b : M) : e (a - b) = e a - e b',\n", - " 'start': [2153, 1],\n", - " 'end': [2154, 28],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.neg',\n", - " 'code': 'def neg : M ≃ₗ[R] M :=\\n { Equiv.neg M, (-LinearMap.id : M →ₗ[R] M) with }',\n", - " 'start': [2163, 1],\n", - " 'end': [2165, 52],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.coe_neg',\n", - " 'code': '@[simp]\\ntheorem coe_neg : ⇑(neg R : M ≃ₗ[R] M) = -id',\n", - " 'start': [2170, 1],\n", - " 'end': [2172, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.neg_apply',\n", - " 'code': 'theorem neg_apply (x : M) : neg R x = -x',\n", - " 'start': [2175, 1],\n", - " 'end': [2175, 52],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.symm_neg',\n", - " 'code': '@[simp]\\ntheorem symm_neg : (neg R : M ≃ₗ[R] M).symm = neg R',\n", - " 'start': [2178, 1],\n", - " 'end': [2180, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.smulOfUnit',\n", - " 'code': 'def smulOfUnit (a : Rˣ) : M ≃ₗ[R] M :=\\n DistribMulAction.toLinearEquiv R M a',\n", - " 'start': [2193, 1],\n", - " 'end': [2195, 39],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.arrowCongr',\n", - " 'code': \"def arrowCongr {R M₁ M₂ M₂₁ M₂₂ : Sort _} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂]\\n [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁]\\n [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) : (M₁ →ₗ[R] M₂₁) ≃ₗ[R] M₂ →ₗ[R] M₂₂\\n where\\n toFun := fun f : M₁ →ₗ[R] M₂₁ => (e₂ : M₂₁ →ₗ[R] M₂₂).comp <| f.comp (e₁.symm : M₂ →ₗ[R] M₁)\\n invFun f := (e₂.symm : M₂₂ →ₗ[R] M₂₁).comp <| f.comp (e₁ : M₁ →ₗ[R] M₂)\\n left_inv f := by\\n ext x\\n simp only [symm_apply_apply, Function.comp_apply, coe_comp, coe_coe]\\n right_inv f := by\\n ext x\\n simp only [Function.comp_apply, apply_symm_apply, coe_comp, coe_coe]\\n map_add' f g := by\\n ext x\\n simp only [map_add, add_apply, Function.comp_apply, coe_comp, coe_coe]\\n map_smul' c f := by\\n ext x\\n simp only [smul_apply, Function.comp_apply, coe_comp, map_smulₛₗ e₂, coe_coe]\",\n", - " 'start': [2198, 1],\n", - " 'end': [2217, 82],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.arrowCongr_apply',\n", - " 'code': '@[simp]\\ntheorem arrowCongr_apply {R M₁ M₂ M₂₁ M₂₂ : Sort _} [CommSemiring R] [AddCommMonoid M₁]\\n [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂]\\n [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₁ →ₗ[R] M₂₁)\\n (x : M₂) : arrowCongr e₁ e₂ f x = e₂ (f (e₁.symm x))',\n", - " 'start': [2220, 1],\n", - " 'end': [2225, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.arrowCongr_symm_apply',\n", - " 'code': '@[simp]\\ntheorem arrowCongr_symm_apply {R M₁ M₂ M₂₁ M₂₂ : Sort _} [CommSemiring R] [AddCommMonoid M₁]\\n [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂]\\n [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₂ →ₗ[R] M₂₂)\\n (x : M₁) : (arrowCongr e₁ e₂).symm f x = e₂.symm (f (e₁ x))',\n", - " 'start': [2228, 1],\n", - " 'end': [2233, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.arrowCongr_comp',\n", - " 'code': 'theorem arrowCongr_comp {N N₂ N₃ : Sort _} [AddCommMonoid N] [AddCommMonoid N₂] [AddCommMonoid N₃]\\n [Module R N] [Module R N₂] [Module R N₃] (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃)\\n (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :\\n arrowCongr e₁ e₃ (g.comp f) = (arrowCongr e₂ e₃ g).comp (arrowCongr e₁ e₂ f)',\n", - " 'start': [2236, 1],\n", - " 'end': [2241, 71],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.arrowCongr_trans',\n", - " 'code': 'theorem arrowCongr_trans {M₁ M₂ M₃ N₁ N₂ N₃ : Sort _} [AddCommMonoid M₁] [Module R M₁]\\n [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid N₁]\\n [Module R N₁] [AddCommMonoid N₂] [Module R N₂] [AddCommMonoid N₃] [Module R N₃]\\n (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) :\\n (arrowCongr e₁ e₂).trans (arrowCongr e₃ e₄) = arrowCongr (e₁.trans e₃) (e₂.trans e₄)',\n", - " 'start': [2244, 1],\n", - " 'end': [2249, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.congrRight',\n", - " 'code': 'def congrRight (f : M₂ ≃ₗ[R] M₃) : (M →ₗ[R] M₂) ≃ₗ[R] M →ₗ[R] M₃ :=\\n arrowCongr (LinearEquiv.refl R M) f',\n", - " 'start': [2252, 1],\n", - " 'end': [2255, 38],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.conj',\n", - " 'code': 'def conj (e : M ≃ₗ[R] M₂) : Module.End R M ≃ₗ[R] Module.End R M₂ :=\\n arrowCongr e e',\n", - " 'start': [2258, 1],\n", - " 'end': [2261, 17],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.conj_apply',\n", - " 'code': 'theorem conj_apply (e : M ≃ₗ[R] M₂) (f : Module.End R M) :\\n e.conj f = ((↑e : M →ₗ[R] M₂).comp f).comp (e.symm : M₂ →ₗ[R] M)',\n", - " 'start': [2264, 1],\n", - " 'end': [2266, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.conj_apply_apply',\n", - " 'code': 'theorem conj_apply_apply (e : M ≃ₗ[R] M₂) (f : Module.End R M) (x : M₂) :\\n e.conj f x = e (f (e.symm x))',\n", - " 'start': [2269, 1],\n", - " 'end': [2271, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.symm_conj_apply',\n", - " 'code': 'theorem symm_conj_apply (e : M ≃ₗ[R] M₂) (f : Module.End R M₂) :\\n e.symm.conj f = ((↑e.symm : M₂ →ₗ[R] M).comp f).comp (e : M →ₗ[R] M₂)',\n", - " 'start': [2274, 1],\n", - " 'end': [2276, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.conj_comp',\n", - " 'code': 'theorem conj_comp (e : M ≃ₗ[R] M₂) (f g : Module.End R M) :\\n e.conj (g.comp f) = (e.conj g).comp (e.conj f)',\n", - " 'start': [2279, 1],\n", - " 'end': [2281, 28],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.conj_trans',\n", - " 'code': 'theorem conj_trans (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) :\\n e₁.conj.trans e₂.conj = (e₁.trans e₂).conj',\n", - " 'start': [2284, 1],\n", - " 'end': [2287, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.conj_id',\n", - " 'code': '@[simp]\\ntheorem conj_id (e : M ≃ₗ[R] M₂) : e.conj LinearMap.id = LinearMap.id',\n", - " 'start': [2290, 1],\n", - " 'end': [2293, 20],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.smulOfNeZero',\n", - " 'code': '@[simps!]\\ndef smulOfNeZero (a : K) (ha : a ≠ 0) : M ≃ₗ[K] M :=\\n smulOfUnit <| Units.mk0 a ha',\n", - " 'start': [2308, 1],\n", - " 'end': [2311, 31],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.equivSubtypeMap',\n", - " 'code': \"def equivSubtypeMap (p : Submodule R M) (q : Submodule R p) : q ≃ₗ[R] q.map p.subtype :=\\n { (p.subtype.domRestrict q).codRestrict _ (by rintro ⟨x, hx⟩; exact ⟨x, hx, rfl⟩) with\\n invFun := by\\n rintro ⟨x, hx⟩\\n refine' ⟨⟨x, _⟩, _⟩ <;> rcases hx with ⟨⟨_, h⟩, _, rfl⟩ <;> assumption\\n left_inv := fun ⟨⟨_, _⟩, _⟩ => rfl\\n right_inv := fun ⟨x, ⟨_, h⟩, _, rfl⟩ => by ext; rfl }\",\n", - " 'start': [2324, 1],\n", - " 'end': [2332, 58],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.equivSubtypeMap_apply',\n", - " 'code': '@[simp]\\ntheorem equivSubtypeMap_apply {p : Submodule R M} {q : Submodule R p} (x : q) :\\n (p.equivSubtypeMap q x : M) = p.subtype.domRestrict q x',\n", - " 'start': [2335, 1],\n", - " 'end': [2338, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.equivSubtypeMap_symm_apply',\n", - " 'code': '@[simp]\\ntheorem equivSubtypeMap_symm_apply {p : Submodule R M} {q : Submodule R p} (x : q.map p.subtype) :\\n ((p.equivSubtypeMap q).symm x : M) = x',\n", - " 'start': [2341, 1],\n", - " 'end': [2345, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comapSubtypeEquivOfLe',\n", - " 'code': \"@[simps symm_apply]\\ndef comapSubtypeEquivOfLe {p q : Submodule R M} (hpq : p ≤ q) : comap q.subtype p ≃ₗ[R] p where\\n toFun x := ⟨x, x.2⟩\\n invFun x := ⟨⟨x, hpq x.2⟩, x.2⟩\\n left_inv x := by simp only [coe_mk, SetLike.eta, LinearEquiv.coe_coe]\\n right_inv x := by simp only [Subtype.coe_mk, SetLike.eta, LinearEquiv.coe_coe]\\n map_add' x y := rfl\\n map_smul' c x := rfl\",\n", - " 'start': [2348, 1],\n", - " 'end': [2357, 23],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comapSubtypeEquivOfLe_apply_coe',\n", - " 'code': '@[simp]\\ntheorem comapSubtypeEquivOfLe_apply_coe {p q : Submodule R M} (hpq : p ≤ q)\\n (x : comap q.subtype p) :\\n (comapSubtypeEquivOfLe hpq x : M) = (x : M)',\n", - " 'start': [2363, 1],\n", - " 'end': [2367, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.mem_map_equiv',\n", - " 'code': '@[simp high]\\ntheorem mem_map_equiv {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} :\\n x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔ e.symm x ∈ p',\n", - " 'start': [2391, 1],\n", - " 'end': [2398, 36],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_equiv_eq_comap_symm',\n", - " 'code': 'theorem map_equiv_eq_comap_symm (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R M) :\\n K.map (e : M →ₛₗ[τ₁₂] M₂) = K.comap (e.symm : M₂ →ₛₗ[τ₂₁] M)',\n", - " 'start': [2401, 1],\n", - " 'end': [2403, 79],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_equiv_eq_map_symm',\n", - " 'code': 'theorem comap_equiv_eq_map_symm (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R₂ M₂) :\\n K.comap (e : M →ₛₗ[τ₁₂] M₂) = K.map (e.symm : M₂ →ₛₗ[τ₂₁] M)',\n", - " 'start': [2406, 1],\n", - " 'end': [2408, 42],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.map_symm_eq_iff',\n", - " 'code': 'theorem map_symm_eq_iff (e : M ≃ₛₗ[τ₁₂] M₂) {K : Submodule R₂ M₂} :\\n K.map e.symm = p ↔ p.map e = K',\n", - " 'start': [2413, 1],\n", - " 'end': [2421, 55],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"Submodule.orderIsoMapComap_apply'\",\n", - " 'code': \"theorem orderIsoMapComap_apply' (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R M) :\\n orderIsoMapComap e p = comap e.symm p\",\n", - " 'start': [2424, 1],\n", - " 'end': [2426, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': \"Submodule.orderIsoMapComap_symm_apply'\",\n", - " 'code': \"theorem orderIsoMapComap_symm_apply' (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R₂ M₂) :\\n (orderIsoMapComap e).symm p = map e.symm p\",\n", - " 'start': [2429, 1],\n", - " 'end': [2431, 30],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.inf_comap_le_comap_add',\n", - " 'code': 'theorem inf_comap_le_comap_add (f₁ f₂ : M →ₛₗ[τ₁₂] M₂) :\\n comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q',\n", - " 'start': [2434, 1],\n", - " 'end': [2440, 26],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.comap_le_comap_smul',\n", - " 'code': 'theorem comap_le_comap_smul (fₗ : N →ₗ[R] N₂) (c : R) : comap fₗ qₗ ≤ comap (c • fₗ) qₗ',\n", - " 'start': [2461, 1],\n", - " 'end': [2466, 24],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Submodule.compatibleMaps',\n", - " 'code': \"def compatibleMaps : Submodule R (N →ₗ[R] N₂) where\\n carrier := { fₗ | pₗ ≤ comap fₗ qₗ }\\n zero_mem' := by\\n change pₗ ≤ comap (0 : N →ₗ[R] N₂) qₗ\\n rw [comap_zero]\\n refine' le_top\\n add_mem' {f₁ f₂} h₁ h₂ := by\\n apply le_trans _ (inf_comap_le_comap_add qₗ f₁ f₂)\\n rw [le_inf_iff]\\n exact ⟨h₁, h₂⟩\\n smul_mem' c fₗ h := by\\n dsimp at h\\n exact le_trans h (comap_le_comap_smul qₗ fₗ c)\",\n", - " 'start': [2469, 1],\n", - " 'end': [2483, 51],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'Equiv.toLinearEquiv',\n", - " 'code': \"def toLinearEquiv (e : M ≃ M₂) (h : IsLinearMap R (e : M → M₂)) : M ≃ₗ[R] M₂ :=\\n { e, h.mk' e with }\",\n", - " 'start': [2492, 1],\n", - " 'end': [2494, 22],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.funLeft',\n", - " 'code': \"def funLeft (f : m → n) : (n → M) →ₗ[R] m → M where\\n toFun := (· ∘ f)\\n map_add' _ _ := rfl\\n map_smul' _ _ := rfl\",\n", - " 'start': [2507, 1],\n", - " 'end': [2512, 23],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.funLeft_apply',\n", - " 'code': '@[simp]\\ntheorem funLeft_apply (f : m → n) (g : n → M) (i : m) : funLeft R M f g i = g (f i)',\n", - " 'start': [2515, 1],\n", - " 'end': [2517, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.funLeft_id',\n", - " 'code': '@[simp]\\ntheorem funLeft_id (g : n → M) : funLeft R M _root_.id g = g',\n", - " 'start': [2520, 1],\n", - " 'end': [2522, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.funLeft_comp',\n", - " 'code': 'theorem funLeft_comp (f₁ : n → p) (f₂ : m → n) :\\n funLeft R M (f₁ ∘ f₂) = (funLeft R M f₂).comp (funLeft R M f₁)',\n", - " 'start': [2525, 1],\n", - " 'end': [2527, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.funLeft_surjective_of_injective',\n", - " 'code': 'theorem funLeft_surjective_of_injective (f : m → n) (hf : Injective f) :\\n Surjective (funLeft R M f)',\n", - " 'start': [2530, 1],\n", - " 'end': [2540, 57],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearMap.funLeft_injective_of_surjective',\n", - " 'code': 'theorem funLeft_injective_of_surjective (f : m → n) (hf : Surjective f) :\\n Injective (funLeft R M f)',\n", - " 'start': [2543, 1],\n", - " 'end': [2548, 65],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.funCongrLeft',\n", - " 'code': 'def funCongrLeft (e : m ≃ n) : (n → M) ≃ₗ[R] m → M :=\\n LinearEquiv.ofLinear (funLeft R M e) (funLeft R M e.symm)\\n (LinearMap.ext fun x =>\\n funext fun i => by rw [id_apply, ← funLeft_comp, Equiv.symm_comp_self, LinearMap.funLeft_id])\\n (LinearMap.ext fun x =>\\n funext fun i => by rw [id_apply, ← funLeft_comp, Equiv.self_comp_symm, LinearMap.funLeft_id])',\n", - " 'start': [2557, 1],\n", - " 'end': [2564, 100],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.funCongrLeft_apply',\n", - " 'code': '@[simp]\\ntheorem funCongrLeft_apply (e : m ≃ n) (x : n → M) : funCongrLeft R M e x = funLeft R M e x',\n", - " 'start': [2567, 1],\n", - " 'end': [2569, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.funCongrLeft_id',\n", - " 'code': '@[simp]\\ntheorem funCongrLeft_id : funCongrLeft R M (Equiv.refl n) = LinearEquiv.refl R (n → M)',\n", - " 'start': [2572, 1],\n", - " 'end': [2574, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.funCongrLeft_comp',\n", - " 'code': '@[simp]\\ntheorem funCongrLeft_comp (e₁ : m ≃ n) (e₂ : n ≃ p) :\\n funCongrLeft R M (Equiv.trans e₁ e₂) =\\n LinearEquiv.trans (funCongrLeft R M e₂) (funCongrLeft R M e₁)',\n", - " 'start': [2577, 1],\n", - " 'end': [2581, 6],\n", - " 'kind': 'commanddeclaration'},\n", - " {'full_name': 'LinearEquiv.funCongrLeft_symm',\n", - " 'code': '@[simp]\\ntheorem funCongrLeft_symm (e : m ≃ n) : (funCongrLeft R M e).symm = funCongrLeft R M e.symm',\n", - " 'start': [2584, 1],\n", - " 'end': [2586, 6],\n", + " 'start': [71, 1],\n", + " 'end': [75, 7],\n", + " 'kind': 'commanddeclaration'},\n", + " {'full_name': 'Finset.univ_prod_mulSingle',\n", + " 'code': '@[to_additive]\\ntheorem Finset.univ_prod_mulSingle [Fintype I] (f : ∀ i, Z i) :\\n (∏ i, Pi.mulSingle i (f i)) = f',\n", + " 'start': [84, 1],\n", + " 'end': [88, 7],\n", + " 'kind': 'commanddeclaration'},\n", + " {'full_name': 'MonoidHom.functions_ext',\n", + " 'code': '@[to_additive]\\ntheorem MonoidHom.functions_ext [Finite I] (G : Type*) [CommMonoid G] (g h : (∀ i, Z i) →* G)\\n (H : ∀ i x, g (Pi.mulSingle i x) = h (Pi.mulSingle i x)) : g = h',\n", + " 'start': [92, 1],\n", + " 'end': [98, 16],\n", + " 'kind': 'commanddeclaration'},\n", + " {'full_name': \"MonoidHom.functions_ext'\",\n", + " 'code': '@[to_additive (attr := ext)\\n \"\\\\nThis is used as the ext lemma instead of `AddMonoidHom.functions_ext` for reasons\\n explained in note [partially-applied ext lemmas].\"]\\ntheorem MonoidHom.functions_ext\\' [Finite I] (M : Type*) [CommMonoid M] (g h : (∀ i, Z i) →* M)\\n (H : ∀ i, g.comp (MonoidHom.single Z i) = h.comp (MonoidHom.single Z i)) : g = h',\n", + " 'start': [102, 1],\n", + " 'end': [109, 56],\n", + " 'kind': 'commanddeclaration'},\n", + " {'full_name': 'RingHom.functions_ext',\n", + " 'code': '@[ext]\\ntheorem RingHom.functions_ext [Finite I] (G : Type*) [NonAssocSemiring G] (g h : (∀ i, f i) →+* G)\\n (H : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h',\n", + " 'start': [123, 1],\n", + " 'end': [127, 72],\n", + " 'kind': 'commanddeclaration'},\n", + " {'full_name': 'Prod.fst_prod',\n", + " 'code': '@[to_additive]\\ntheorem fst_prod : (∏ c in s, f c).1 = ∏ c in s, (f c).1',\n", + " 'start': [136, 1],\n", + " 'end': [138, 35],\n", + " 'kind': 'commanddeclaration'},\n", + " {'full_name': 'Prod.snd_prod',\n", + " 'code': '@[to_additive]\\ntheorem snd_prod : (∏ c in s, f c).2 = ∏ c in s, (f c).2',\n", + " 'start': [142, 1],\n", + " 'end': [144, 35],\n", " 'kind': 'commanddeclaration'}]" ] }, - "execution_count": 9, + "execution_count": 16, "metadata": {}, "output_type": "execute_result" } @@ -1756,17 +267,17 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 17, "id": "77e58935", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "252" + "13" ] }, - "execution_count": 10, + "execution_count": 17, "metadata": {}, "output_type": "execute_result" } @@ -1779,17 +290,17 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 18, "id": "00042165", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TracedTheorem(theorem=Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3ce43c18f614b76e161f911b75a3e1ef641620ff'), file_path=PosixPath('Mathlib/LinearAlgebra/Basic.lean'), full_name='pi_eq_sum_univ'))" + "TracedTheorem(theorem=Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3c307701fa7e9acbdc0680d7f3b9c9fed9081740'), file_path=PosixPath('Mathlib/Algebra/BigOperators/Pi.lean'), full_name='pi_eq_sum_univ'))" ] }, - "execution_count": 11, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } @@ -1802,7 +313,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 19, "id": "4d9ed905", "metadata": {}, "outputs": [], @@ -1813,17 +324,17 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 20, "id": "eafb6369", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3ce43c18f614b76e161f911b75a3e1ef641620ff'), file_path=PosixPath('Mathlib/LinearAlgebra/Basic.lean'), full_name='pi_eq_sum_univ')" + "Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3c307701fa7e9acbdc0680d7f3b9c9fed9081740'), file_path=PosixPath('Mathlib/Algebra/BigOperators/Pi.lean'), full_name='pi_eq_sum_univ')" ] }, - "execution_count": 13, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } @@ -1834,17 +345,17 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 21, "id": "5e00cba9", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "((148, 1), (151, 7))" + "((72, 1), (75, 7))" ] }, - "execution_count": 14, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" } @@ -1855,7 +366,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 22, "id": "14c611f4", "metadata": {}, "outputs": [ @@ -1865,7 +376,7 @@ "True" ] }, - "execution_count": 15, + "execution_count": 22, "metadata": {}, "output_type": "execute_result" } @@ -1876,7 +387,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 23, "id": "24bc67e9", "metadata": {}, "outputs": [ @@ -1886,7 +397,7 @@ "2" ] }, - "execution_count": 16, + "execution_count": 23, "metadata": {}, "output_type": "execute_result" } @@ -1897,7 +408,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 24, "id": "3fa19ef3", "metadata": {}, "outputs": [ @@ -1919,97 +430,40 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 25, "id": "1fae1876", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "[TracedTactic(tactic=ext, state_before=R✝ : Type u_1\n", - " R₁ : Type u_2\n", - " R₂ : Type u_3\n", - " R₃ : Type u_4\n", - " R₄ : Type u_5\n", - " S : Type u_6\n", - " K : Type u_7\n", - " K₂ : Type u_8\n", - " M : Type u_9\n", - " M' : Type u_10\n", - " M₁ : Type u_11\n", - " M₂ : Type u_12\n", - " M₃ : Type u_13\n", - " M₄ : Type u_14\n", - " N : Type u_15\n", - " N₂ : Type u_16\n", - " ι✝ : Type u_17\n", - " V : Type u_18\n", - " V₂ : Type u_19\n", - " ι : Type u_20\n", + "[TracedTactic(tactic=ext, state_before=ι : Type u_1\n", " inst✝² : Fintype ι\n", " inst✝¹ : DecidableEq ι\n", - " R : Type u_21\n", + " R : Type u_2\n", " inst✝ : Semiring R\n", " x : ι → R\n", " ⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0, state_after=case h\n", - " R✝ : Type u_1\n", - " R₁ : Type u_2\n", - " R₂ : Type u_3\n", - " R₃ : Type u_4\n", - " R₄ : Type u_5\n", - " S : Type u_6\n", - " K : Type u_7\n", - " K₂ : Type u_8\n", - " M : Type u_9\n", - " M' : Type u_10\n", - " M₁ : Type u_11\n", - " M₂ : Type u_12\n", - " M₃ : Type u_13\n", - " M₄ : Type u_14\n", - " N : Type u_15\n", - " N₂ : Type u_16\n", - " ι✝ : Type u_17\n", - " V : Type u_18\n", - " V₂ : Type u_19\n", - " ι : Type u_20\n", + " ι : Type u_1\n", " inst✝² : Fintype ι\n", " inst✝¹ : DecidableEq ι\n", - " R : Type u_21\n", + " R : Type u_2\n", " inst✝ : Semiring R\n", " x : ι → R\n", " x✝ : ι\n", " ⊢ x x✝ = Finset.sum Finset.univ (fun i => x i • fun j => if i = j then 1 else 0) x✝),\n", " TracedTactic(tactic=simp, state_before=case h\n", - " R✝ : Type u_1\n", - " R₁ : Type u_2\n", - " R₂ : Type u_3\n", - " R₃ : Type u_4\n", - " R₄ : Type u_5\n", - " S : Type u_6\n", - " K : Type u_7\n", - " K₂ : Type u_8\n", - " M : Type u_9\n", - " M' : Type u_10\n", - " M₁ : Type u_11\n", - " M₂ : Type u_12\n", - " M₃ : Type u_13\n", - " M₄ : Type u_14\n", - " N : Type u_15\n", - " N₂ : Type u_16\n", - " ι✝ : Type u_17\n", - " V : Type u_18\n", - " V₂ : Type u_19\n", - " ι : Type u_20\n", + " ι : Type u_1\n", " inst✝² : Fintype ι\n", " inst✝¹ : DecidableEq ι\n", - " R : Type u_21\n", + " R : Type u_2\n", " inst✝ : Semiring R\n", " x : ι → R\n", " x✝ : ι\n", " ⊢ x x✝ = Finset.sum Finset.univ (fun i => x i • fun j => if i = j then 1 else 0) x✝, state_after=no goals)]" ] }, - "execution_count": 18, + "execution_count": 25, "metadata": {}, "output_type": "execute_result" } @@ -2022,7 +476,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 26, "id": "39fbe993", "metadata": {}, "outputs": [ @@ -2030,36 +484,17 @@ "data": { "text/plain": [ "TracedTactic(tactic=simp, state_before=case h\n", - "R✝ : Type u_1\n", - "R₁ : Type u_2\n", - "R₂ : Type u_3\n", - "R₃ : Type u_4\n", - "R₄ : Type u_5\n", - "S : Type u_6\n", - "K : Type u_7\n", - "K₂ : Type u_8\n", - "M : Type u_9\n", - "M' : Type u_10\n", - "M₁ : Type u_11\n", - "M₂ : Type u_12\n", - "M₃ : Type u_13\n", - "M₄ : Type u_14\n", - "N : Type u_15\n", - "N₂ : Type u_16\n", - "ι✝ : Type u_17\n", - "V : Type u_18\n", - "V₂ : Type u_19\n", - "ι : Type u_20\n", + "ι : Type u_1\n", "inst✝² : Fintype ι\n", "inst✝¹ : DecidableEq ι\n", - "R : Type u_21\n", + "R : Type u_2\n", "inst✝ : Semiring R\n", "x : ι → R\n", "x✝ : ι\n", "⊢ x x✝ = Finset.sum Finset.univ (fun i => x i • fun j => if i = j then 1 else 0) x✝, state_after=no goals)" ] }, - "execution_count": 19, + "execution_count": 26, "metadata": {}, "output_type": "execute_result" } @@ -2080,17 +515,17 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 27, "id": "f3d3f736", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3ce43c18f614b76e161f911b75a3e1ef641620ff')" + "LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3c307701fa7e9acbdc0680d7f3b9c9fed9081740')" ] }, - "execution_count": 20, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } @@ -2109,7 +544,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 29, "id": "10364e0f", "metadata": {}, "outputs": [ @@ -2117,12 +552,12 @@ "name": "stderr", "output_type": "stream", "text": [ - "\u001b[32m2023-12-13 22:41:54.656\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.interaction.dojo\u001b[0m:\u001b[36m__init__\u001b[0m:\u001b[36m172\u001b[0m - \u001b[33m\u001b[1mUsing Lean 4 without a hard timeout may hang indefinitely.\u001b[0m\n" + "\u001b[32m2024-03-07 21:02:23.933\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.interaction.dojo\u001b[0m:\u001b[36m__init__\u001b[0m:\u001b[36m162\u001b[0m - \u001b[33m\u001b[1mUsing Lean 4 without a hard timeout may hang indefinitely.\u001b[0m\n" ] } ], "source": [ - "theorem = Theorem(repo, \"Mathlib/LinearAlgebra/Basic.lean\", \"pi_eq_sum_univ\")\n", + "theorem = Theorem(repo, \"Mathlib/Algebra/BigOperators/Pi.lean\", \"pi_eq_sum_univ\")\n", "\n", "# For some theorems, it might take a few minutes.\n", "dojo, state_0 = Dojo(theorem).__enter__()" @@ -2130,17 +565,17 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 30, "id": "a7d4ad9a", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "TacticState(pp=\"R✝ : Type u_1\\nR₁ : Type u_2\\nR₂ : Type u_3\\nR₃ : Type u_4\\nR₄ : Type u_5\\nS : Type u_6\\nK : Type u_7\\nK₂ : Type u_8\\nM : Type u_9\\nM' : Type u_10\\nM₁ : Type u_11\\nM₂ : Type u_12\\nM₃ : Type u_13\\nM₄ : Type u_14\\nN : Type u_15\\nN₂ : Type u_16\\nι✝ : Type u_17\\nV : Type u_18\\nV₂ : Type u_19\\nι : Type u_20\\ninst✝² : Fintype ι\\ninst✝¹ : DecidableEq ι\\nR : Type u_21\\ninst✝ : Semiring R\\nx : ι → R\\n⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0\", id=0, message=None)" + "TacticState(pp='ι : Type u_1\\ninst✝² : Fintype ι\\ninst✝¹ : DecidableEq ι\\nR : Type u_2\\ninst✝ : Semiring R\\nx : ι → R\\n⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0', id=0, message=None)" ] }, - "execution_count": 22, + "execution_count": 30, "metadata": {}, "output_type": "execute_result" } @@ -2151,7 +586,7 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 31, "id": "af88893b", "metadata": {}, "outputs": [ @@ -2159,29 +594,10 @@ "name": "stdout", "output_type": "stream", "text": [ - "R✝ : Type u_1\n", - "R₁ : Type u_2\n", - "R₂ : Type u_3\n", - "R₃ : Type u_4\n", - "R₄ : Type u_5\n", - "S : Type u_6\n", - "K : Type u_7\n", - "K₂ : Type u_8\n", - "M : Type u_9\n", - "M' : Type u_10\n", - "M₁ : Type u_11\n", - "M₂ : Type u_12\n", - "M₃ : Type u_13\n", - "M₄ : Type u_14\n", - "N : Type u_15\n", - "N₂ : Type u_16\n", - "ι✝ : Type u_17\n", - "V : Type u_18\n", - "V₂ : Type u_19\n", - "ι : Type u_20\n", + "ι : Type u_1\n", "inst✝² : Fintype ι\n", "inst✝¹ : DecidableEq ι\n", - "R : Type u_21\n", + "R : Type u_2\n", "inst✝ : Semiring R\n", "x : ι → R\n", "⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0\n" @@ -2194,7 +610,7 @@ }, { "cell_type": "code", - "execution_count": 24, + "execution_count": 32, "id": "4ca2dca9", "metadata": {}, "outputs": [ @@ -2202,29 +618,10 @@ "name": "stdout", "output_type": "stream", "text": [ - "R✝ : Type u_1\n", - "R₁ : Type u_2\n", - "R₂ : Type u_3\n", - "R₃ : Type u_4\n", - "R₄ : Type u_5\n", - "S : Type u_6\n", - "K : Type u_7\n", - "K₂ : Type u_8\n", - "M : Type u_9\n", - "M' : Type u_10\n", - "M₁ : Type u_11\n", - "M₂ : Type u_12\n", - "M₃ : Type u_13\n", - "M₄ : Type u_14\n", - "N : Type u_15\n", - "N₂ : Type u_16\n", - "ι✝ : Type u_17\n", - "V : Type u_18\n", - "V₂ : Type u_19\n", - "ι : Type u_20\n", + "ι : Type u_1\n", "inst✝² : Fintype ι\n", "inst✝¹ : DecidableEq ι\n", - "R : Type u_21\n", + "R : Type u_2\n", "inst✝ : Semiring R\n", "⊢ ∀ (x : ι → R), x = ∑ i : ι, x i • fun j => if i = j then 1 else 0\n" ] @@ -2238,7 +635,7 @@ }, { "cell_type": "code", - "execution_count": 25, + "execution_count": 33, "id": "89a62c89", "metadata": {}, "outputs": [ @@ -2248,7 +645,7 @@ "LeanError(error=':1:1: unknown tactic')" ] }, - "execution_count": 25, + "execution_count": 33, "metadata": {}, "output_type": "execute_result" } @@ -2261,7 +658,7 @@ }, { "cell_type": "code", - "execution_count": 26, + "execution_count": 34, "id": "10b5f013", "metadata": {}, "outputs": [ @@ -2272,8 +669,8 @@ "traceback": [ "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", "\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)", - "Cell \u001b[0;32mIn[26], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[43mdojo\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mrun_tac\u001b[49m\u001b[43m(\u001b[49m\u001b[43mstate_2\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[38;5;124;43mskip\u001b[39;49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[43m)\u001b[49m\n", - "File \u001b[0;32m~/Desktop/dev/LeanDojo/src/lean_dojo/interaction/dojo.py:481\u001b[0m, in \u001b[0;36mDojo.run_tac\u001b[0;34m(self, state, tactic)\u001b[0m\n\u001b[1;32m 479\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mrun_tac\u001b[39m(\u001b[38;5;28mself\u001b[39m, state: TacticState, tactic: \u001b[38;5;28mstr\u001b[39m) \u001b[38;5;241m-\u001b[39m\u001b[38;5;241m>\u001b[39m TacticResult:\n\u001b[1;32m 480\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;129;01mnot\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(state, TacticState):\n\u001b[0;32m--> 481\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mRuntimeError\u001b[39;00m(\n\u001b[1;32m 482\u001b[0m \u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mAttempting to run a tactic on an invalid state \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mstate\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m.\u001b[39m\u001b[38;5;124m\"\u001b[39m\n\u001b[1;32m 483\u001b[0m )\n\u001b[1;32m 484\u001b[0m \u001b[38;5;28;01massert\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(tactic, \u001b[38;5;28mstr\u001b[39m), \u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mInvalid tactic \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mtactic\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m\n\u001b[1;32m 486\u001b[0m tsid \u001b[38;5;241m=\u001b[39m state\u001b[38;5;241m.\u001b[39mid\n", + "Cell \u001b[0;32mIn[34], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[43mdojo\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mrun_tac\u001b[49m\u001b[43m(\u001b[49m\u001b[43mstate_2\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[38;5;124;43mskip\u001b[39;49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[43m)\u001b[49m\n", + "File \u001b[0;32m~/Desktop/dev/LeanDojo/src/lean_dojo/interaction/dojo.py:427\u001b[0m, in \u001b[0;36mDojo.run_tac\u001b[0;34m(self, state, tactic)\u001b[0m\n\u001b[1;32m 425\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mrun_tac\u001b[39m(\u001b[38;5;28mself\u001b[39m, state: TacticState, tactic: \u001b[38;5;28mstr\u001b[39m) \u001b[38;5;241m-\u001b[39m\u001b[38;5;241m>\u001b[39m TacticResult:\n\u001b[1;32m 426\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;129;01mnot\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(state, TacticState):\n\u001b[0;32m--> 427\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mRuntimeError\u001b[39;00m(\n\u001b[1;32m 428\u001b[0m \u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mAttempting to run a tactic on an invalid state \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mstate\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m.\u001b[39m\u001b[38;5;124m\"\u001b[39m\n\u001b[1;32m 429\u001b[0m )\n\u001b[1;32m 430\u001b[0m \u001b[38;5;28;01massert\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(tactic, \u001b[38;5;28mstr\u001b[39m), \u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mInvalid tactic \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mtactic\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m\n\u001b[1;32m 432\u001b[0m tsid \u001b[38;5;241m=\u001b[39m state\u001b[38;5;241m.\u001b[39mid\n", "\u001b[0;31mRuntimeError\u001b[0m: Attempting to run a tactic on an invalid state LeanError(error=':1:1: unknown tactic')." ] } @@ -2284,7 +681,7 @@ }, { "cell_type": "code", - "execution_count": 27, + "execution_count": 35, "id": "65bae6ea", "metadata": {}, "outputs": [ @@ -2294,7 +691,7 @@ "ProofGivenUp()" ] }, - "execution_count": 27, + "execution_count": 35, "metadata": {}, "output_type": "execute_result" } @@ -2305,7 +702,7 @@ }, { "cell_type": "code", - "execution_count": 28, + "execution_count": 36, "id": "c373865a", "metadata": {}, "outputs": [ @@ -2313,29 +710,10 @@ "name": "stdout", "output_type": "stream", "text": [ - "R✝ : Type u_1\n", - "R₁ : Type u_2\n", - "R₂ : Type u_3\n", - "R₃ : Type u_4\n", - "R₄ : Type u_5\n", - "S : Type u_6\n", - "K : Type u_7\n", - "K₂ : Type u_8\n", - "M : Type u_9\n", - "M' : Type u_10\n", - "M₁ : Type u_11\n", - "M₂ : Type u_12\n", - "M₃ : Type u_13\n", - "M₄ : Type u_14\n", - "N : Type u_15\n", - "N₂ : Type u_16\n", - "ι✝ : Type u_17\n", - "V : Type u_18\n", - "V₂ : Type u_19\n", - "ι : Type u_20\n", + "ι : Type u_1\n", "inst✝² : Fintype ι\n", "inst✝¹ : DecidableEq ι\n", - "R : Type u_21\n", + "R : Type u_2\n", "inst✝ : Semiring R\n", "x : ι → R\n", "⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0\n" @@ -2348,7 +726,7 @@ }, { "cell_type": "code", - "execution_count": 29, + "execution_count": 37, "id": "a5d0156f", "metadata": {}, "outputs": [ @@ -2357,29 +735,10 @@ "output_type": "stream", "text": [ "case h\n", - "R✝ : Type u_1\n", - "R₁ : Type u_2\n", - "R₂ : Type u_3\n", - "R₃ : Type u_4\n", - "R₄ : Type u_5\n", - "S : Type u_6\n", - "K : Type u_7\n", - "K₂ : Type u_8\n", - "M : Type u_9\n", - "M' : Type u_10\n", - "M₁ : Type u_11\n", - "M₂ : Type u_12\n", - "M₃ : Type u_13\n", - "M₄ : Type u_14\n", - "N : Type u_15\n", - "N₂ : Type u_16\n", - "ι✝ : Type u_17\n", - "V : Type u_18\n", - "V₂ : Type u_19\n", - "ι : Type u_20\n", + "ι : Type u_1\n", "inst✝² : Fintype ι\n", "inst✝¹ : DecidableEq ι\n", - "R : Type u_21\n", + "R : Type u_2\n", "inst✝ : Semiring R\n", "x : ι → R\n", "x✝ : ι\n", @@ -2395,7 +754,7 @@ }, { "cell_type": "code", - "execution_count": 30, + "execution_count": 38, "id": "71ab5854", "metadata": {}, "outputs": [ @@ -2415,7 +774,7 @@ }, { "cell_type": "code", - "execution_count": 31, + "execution_count": 39, "id": "fdb44496", "metadata": {}, "outputs": [ @@ -2425,7 +784,7 @@ "True" ] }, - "execution_count": 31, + "execution_count": 39, "metadata": {}, "output_type": "execute_result" } @@ -2444,7 +803,7 @@ }, { "cell_type": "code", - "execution_count": 32, + "execution_count": 40, "id": "243ea43c", "metadata": {}, "outputs": [ @@ -2452,18 +811,18 @@ "name": "stderr", "output_type": "stream", "text": [ - "\u001b[32m2023-12-13 23:21:00.847\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.interaction.dojo\u001b[0m:\u001b[36m__init__\u001b[0m:\u001b[36m172\u001b[0m - \u001b[33m\u001b[1mUsing Lean 4 without a hard timeout may hang indefinitely.\u001b[0m\n" + "\u001b[32m2024-03-07 21:05:20.377\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.interaction.dojo\u001b[0m:\u001b[36m__init__\u001b[0m:\u001b[36m162\u001b[0m - \u001b[33m\u001b[1mUsing Lean 4 without a hard timeout may hang indefinitely.\u001b[0m\n" ] } ], "source": [ - "entry = (repo, \"Mathlib/LinearAlgebra/Basic.lean\", 83) # (repo, file_path, line_nb)\n", + "entry = (repo, \"Mathlib/LinearAlgebra/Basic.lean\", 90) # (repo, file_path, line_nb)\n", "dojo, state_0 = Dojo(entry).__enter__()" ] }, { "cell_type": "code", - "execution_count": 33, + "execution_count": 41, "id": "5ebd615c", "metadata": {}, "outputs": [ @@ -2473,7 +832,7 @@ "CommandState(id=0, message=None)" ] }, - "execution_count": 33, + "execution_count": 41, "metadata": {}, "output_type": "execute_result" } @@ -2484,7 +843,7 @@ }, { "cell_type": "code", - "execution_count": 34, + "execution_count": 42, "id": "b1e079fa", "metadata": {}, "outputs": [ @@ -2494,7 +853,7 @@ "CommandState(id=1, message='1')" ] }, - "execution_count": 34, + "execution_count": 42, "metadata": {}, "output_type": "execute_result" } @@ -2505,7 +864,7 @@ }, { "cell_type": "code", - "execution_count": 35, + "execution_count": 43, "id": "31c9bada", "metadata": {}, "outputs": [ @@ -2515,7 +874,7 @@ "LeanError(error=\"unknown identifier 'x'\")" ] }, - "execution_count": 35, + "execution_count": 43, "metadata": {}, "output_type": "execute_result" } @@ -2526,7 +885,7 @@ }, { "cell_type": "code", - "execution_count": 36, + "execution_count": 44, "id": "b638bfbf", "metadata": {}, "outputs": [ @@ -2536,7 +895,7 @@ "CommandState(id=3, message='')" ] }, - "execution_count": 36, + "execution_count": 44, "metadata": {}, "output_type": "execute_result" } @@ -2549,7 +908,7 @@ }, { "cell_type": "code", - "execution_count": 37, + "execution_count": 45, "id": "bdc4f14d", "metadata": {}, "outputs": [ @@ -2559,7 +918,7 @@ "CommandState(id=4, message='1')" ] }, - "execution_count": 37, + "execution_count": 45, "metadata": {}, "output_type": "execute_result" } @@ -2570,44 +929,44 @@ }, { "cell_type": "code", - "execution_count": 38, + "execution_count": 46, "id": "ef47afb8", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "CommandState(id=5, message='Finsupp.smul_sum.{u_23, u_22, u_21, u_20} {α : Type u_20} {β : Type u_21} {R : Type u_22} {M : Type u_23}\\n[inst✝ : Zero β] [inst✝¹ : AddCommMonoid M] [inst✝² : DistribSMul R M] {v : α →₀ β} {c : R} {h : α → β → M} :\\nc • sum v h = sum v fun a b => c • h a b')" + "CommandState(id=5, message='addMonoidHomLequivNat.{u_22, u_21, u_20} {A : Type u_20} {B : Type u_21} (R : Type u_22) [inst✝ : Semiring R]\\n[inst✝¹ : AddCommMonoid A] [inst✝² : AddCommMonoid B] [inst✝³ : Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℕ] B')" ] }, - "execution_count": 38, + "execution_count": 46, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "dojo.run_cmd(state_0, \"#check smul_sum\")" + "dojo.run_cmd(state_0, \"#check addMonoidHomLequivNat\")" ] }, { "cell_type": "code", - "execution_count": 39, + "execution_count": 47, "id": "c6b8b9a5", "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "LeanError(error=\"unknown identifier 'linearEquivFunOnFinite'\")" + "LeanError(error=\"unknown identifier 'addMonoidEndRingEquivInt'\")" ] }, - "execution_count": 39, + "execution_count": 47, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "dojo.run_cmd(state_0, \"#check linearEquivFunOnFinite\")" + "dojo.run_cmd(state_0, \"#check addMonoidEndRingEquivInt\")" ] }, { @@ -2635,7 +994,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.10.13" + "version": "3.9.18" } }, "nbformat": 4, diff --git a/scripts/generate-benchmark-lean4.ipynb b/scripts/generate-benchmark-lean4.ipynb index 3e45221..e85c3a4 100644 --- a/scripts/generate-benchmark-lean4.ipynb +++ b/scripts/generate-benchmark-lean4.ipynb @@ -14,7 +14,7 @@ "NeurIPS 2023 (Datasets and Benchmarks Track) \n", "[Kaiyu Yang](https://yangky11.github.io/), [Aidan Swope](https://aidanswope.com/about), [Alex Gu](https://minimario.github.io/), [Rahul Chalamala](https://rchalamala.github.io/), [Peiyang Song](https://peiyang-song.github.io/), [Shixing Yu](https://billysx.github.io/), [Saad Godil](https://www.linkedin.com/in/saad-godil-9728353/), [Ryan Prenger](https://www.linkedin.com/in/ryan-prenger-18797ba1/), [Anima Anandkumar](http://tensorlab.cms.caltech.edu/users/anima/)\n", "\n", - "The dataset is constructed from [mathlib4](https://github.com/leanprover-community/mathlib4/tree/3ce43c18f614b76e161f911b75a3e1ef641620ff) (`3ce43c18f614b76e161f911b75a3e1ef641620ff`) and will be saved to `../leandojo_benchmark_4`. It includes 2000 theorems for validation, 2000 theorems for testing, and the rest for training. Please refer to our paper for details. For most use cases, you shouldn't need to generate the data and can directly use our official LeanDojo Benchmark 4 downloadable [here](https://zenodo.org/doi/10.5281/zenodo.8040109).\n", + "The dataset is constructed from [mathlib4](https://github.com/leanprover-community/mathlib4/tree/3c307701fa7e9acbdc0680d7f3b9c9fed9081740) (`3c307701fa7e9acbdc0680d7f3b9c9fed9081740`) and will be saved to `../leandojo_benchmark_4`. It includes 2000 theorems for validation, 2000 theorems for testing, and the rest for training. Please refer to our paper for details. For most use cases, you shouldn't need to generate the data and can directly use our official LeanDojo Benchmark 4 downloadable [here](https://zenodo.org/doi/10.5281/zenodo.8040109).\n", "\n", "This script is for Lean 4. We also have a [version for Lean 3](https://github.com/lean-dojo/LeanDojo/blob/main/scripts/generate-benchmark-lean3.ipynb).\n" ] @@ -43,7 +43,7 @@ "random.seed(3407) # https://arxiv.org/abs/2109.08203\n", "\n", "URL = \"https://github.com/leanprover-community/mathlib4\"\n", - "COMMIT = \"3ce43c18f614b76e161f911b75a3e1ef641620ff\"\n", + "COMMIT = \"3c307701fa7e9acbdc0680d7f3b9c9fed9081740\"\n", "DST_DIR = Path(\"../leandojo_benchmark_4\")\n", "NUM_VAL = NUM_TEST = 2000" ] @@ -207,7 +207,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 6, "id": "06e6fe8d", "metadata": {}, "outputs": [], @@ -336,7 +336,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 7, "id": "bc50220e", "metadata": { "scrolled": true @@ -346,19 +346,29 @@ "name": "stderr", "output_type": "stream", "text": [ - "\u001b[32m2024-01-18 14:28:18.667\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m193\u001b[0m - \u001b[1mLoading the traced repo from /home/kaiyu/.cache/lean_dojo/leanprover-community-mathlib4-3ce43c18f614b76e161f911b75a3e1ef641620ff/mathlib4\u001b[0m\n", - "2024-01-18 14:28:27,148\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n", - "100%|██████████| 4462/4462 [23:45<00:00, 3.13it/s] \n", - "\u001b[32m2024-01-18 14:53:12.008\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_data\u001b[0m:\u001b[36m6\u001b[0m - \u001b[1m106248 theorems in total\u001b[0m\n", - "\u001b[32m2024-01-18 14:53:12.010\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_randomly\u001b[0m:\u001b[36m18\u001b[0m - \u001b[1mSplitting the theorems randomly\u001b[0m\n", - "\u001b[32m2024-01-18 14:53:12.058\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_by_premise\u001b[0m:\u001b[36m8\u001b[0m - \u001b[1mSplitting the theorems by premises\u001b[0m\n", - "\u001b[32m2024-01-18 14:57:45.598\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m102248 theorems and 212584 tactics saved to ../leandojo_benchmark_4/random/train.json\u001b[0m\n", - "\u001b[32m2024-01-18 14:57:46.455\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 4340 tactics saved to ../leandojo_benchmark_4/random/val.json\u001b[0m\n", - "\u001b[32m2024-01-18 14:57:47.126\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 3628 tactics saved to ../leandojo_benchmark_4/random/test.json\u001b[0m\n", - "\u001b[32m2024-01-18 14:58:12.494\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m102248 theorems and 202196 tactics saved to ../leandojo_benchmark_4/novel_premises/train.json\u001b[0m\n", - "\u001b[32m2024-01-18 14:58:13.907\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 9334 tactics saved to ../leandojo_benchmark_4/novel_premises/val.json\u001b[0m\n", - "\u001b[32m2024-01-18 14:58:14.971\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m37\u001b[0m - \u001b[1m2000 theorems and 9022 tactics saved to ../leandojo_benchmark_4/novel_premises/test.json\u001b[0m\n", - "\u001b[32m2024-01-18 14:58:47.950\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m61\u001b[0m - \u001b[1m152695 theorems/definitions from 4462 files saved to ../leandojo_benchmark_4/corpus.jsonl\u001b[0m\n" + "\u001b[32m2024-03-08 22:02:09.712\u001b[0m | \u001b[1mINFO \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m116\u001b[0m - \u001b[1mLoading the traced repo from /Users/yangky/.cache/lean_dojo/leanprover-community-mathlib4-3c307701fa7e9acbdc0680d7f3b9c9fed9081740/mathlib4\u001b[0m\n", + "2024-03-08 22:02:12,872\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n", + "100%|██████████| 5042/5042 [2:00:08<00:00, 1.43s/it] \n", + "\u001b[32m2024-03-09 00:02:34.525\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='a751d21d4b68c999accb6fc5d960538af26ad5ec') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n", + "\u001b[32m2024-03-09 00:03:01.450\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n", + "\u001b[32m2024-03-09 00:03:12.592\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/xubaiw/CMark.lean', commit='0077cbbaa92abf855fc1c0413e158ffd8195ec77') relies on an unsupported Lean version: 8fc1af650ad6d31cf766d9bc84119149330e7d4e\u001b[0m\n", + "Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356\n", + "\u001b[32m2024-03-09 00:03:16.757\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/mhuisi/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa') relies on an unsupported Lean version: 216d2460e0adec8317fdeeb6f2543cb7442564fd\u001b[0m\n", + "\u001b[32m2024-03-09 00:03:24.256\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/fgdorais/lean4-unicode-basic', commit='280d75fdfe7be8eb337be7f1bf8479b4aac09f71') relies on an unsupported Lean version: 0d7051497ea09b2b4a4ef608e371b8f317487c3c\u001b[0m\n", + "\u001b[32m2024-03-09 00:03:28.948\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/hargonix/LeanInk', commit='2447df5cc6e48eb965c3c3fba87e46d353b5e9f1') relies on an unsupported Lean version: f6cd6c069587cfe62dd68cb6330f9ad794a56724\u001b[0m\n" + ] + }, + { + "ename": "AttributeError", + "evalue": "'LeanGitRepo' object has no attribute 'is_lean4'", + "output_type": "error", + "traceback": [ + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mAttributeError\u001b[0m Traceback (most recent call last)", + "Cell \u001b[0;32mIn[7], line 3\u001b[0m\n\u001b[1;32m 1\u001b[0m repo \u001b[38;5;241m=\u001b[39m LeanGitRepo(URL, COMMIT)\n\u001b[1;32m 2\u001b[0m traced_repo \u001b[38;5;241m=\u001b[39m trace(repo)\n\u001b[0;32m----> 3\u001b[0m splits \u001b[38;5;241m=\u001b[39m \u001b[43msplit_data\u001b[49m\u001b[43m(\u001b[49m\u001b[43mtraced_repo\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 4\u001b[0m export_data(traced_repo, splits, DST_DIR, dataset_name\u001b[38;5;241m=\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mLeanDojo Benchmark 4\u001b[39m\u001b[38;5;124m\"\u001b[39m)\n", + "Cell \u001b[0;32mIn[5], line 3\u001b[0m, in \u001b[0;36msplit_data\u001b[0;34m(traced_repo)\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21msplit_data\u001b[39m(traced_repo: TracedRepo) \u001b[38;5;241m-\u001b[39m\u001b[38;5;241m>\u001b[39m Dict[SPLIT_STRATEGY, SPLIT]:\n\u001b[1;32m 2\u001b[0m \u001b[38;5;66;03m# Skip theorems in the Lean 4 repo itself.\u001b[39;00m\n\u001b[0;32m----> 3\u001b[0m traced_theorems \u001b[38;5;241m=\u001b[39m [\n\u001b[1;32m 4\u001b[0m thm \u001b[38;5;28;01mfor\u001b[39;00m thm \u001b[38;5;129;01min\u001b[39;00m traced_repo\u001b[38;5;241m.\u001b[39mget_traced_theorems() \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;129;01mnot\u001b[39;00m thm\u001b[38;5;241m.\u001b[39mrepo\u001b[38;5;241m.\u001b[39mis_lean4\n\u001b[1;32m 5\u001b[0m ]\n\u001b[1;32m 6\u001b[0m logger\u001b[38;5;241m.\u001b[39minfo(\u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;132;01m{\u001b[39;00m\u001b[38;5;28mlen\u001b[39m(traced_theorems)\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m theorems in total\u001b[39m\u001b[38;5;124m\"\u001b[39m)\n\u001b[1;32m 8\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m {\n\u001b[1;32m 9\u001b[0m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mrandom\u001b[39m\u001b[38;5;124m\"\u001b[39m: split_randomly(traced_theorems),\n\u001b[1;32m 10\u001b[0m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mnovel_premises\u001b[39m\u001b[38;5;124m\"\u001b[39m: split_by_premise(traced_theorems),\n\u001b[1;32m 11\u001b[0m }\n", + "Cell \u001b[0;32mIn[5], line 4\u001b[0m, in \u001b[0;36m\u001b[0;34m(.0)\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21msplit_data\u001b[39m(traced_repo: TracedRepo) \u001b[38;5;241m-\u001b[39m\u001b[38;5;241m>\u001b[39m Dict[SPLIT_STRATEGY, SPLIT]:\n\u001b[1;32m 2\u001b[0m \u001b[38;5;66;03m# Skip theorems in the Lean 4 repo itself.\u001b[39;00m\n\u001b[1;32m 3\u001b[0m traced_theorems \u001b[38;5;241m=\u001b[39m [\n\u001b[0;32m----> 4\u001b[0m thm \u001b[38;5;28;01mfor\u001b[39;00m thm \u001b[38;5;129;01min\u001b[39;00m traced_repo\u001b[38;5;241m.\u001b[39mget_traced_theorems() \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;129;01mnot\u001b[39;00m \u001b[43mthm\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mrepo\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mis_lean4\u001b[49m\n\u001b[1;32m 5\u001b[0m ]\n\u001b[1;32m 6\u001b[0m logger\u001b[38;5;241m.\u001b[39minfo(\u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;132;01m{\u001b[39;00m\u001b[38;5;28mlen\u001b[39m(traced_theorems)\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m theorems in total\u001b[39m\u001b[38;5;124m\"\u001b[39m)\n\u001b[1;32m 8\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m {\n\u001b[1;32m 9\u001b[0m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mrandom\u001b[39m\u001b[38;5;124m\"\u001b[39m: split_randomly(traced_theorems),\n\u001b[1;32m 10\u001b[0m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mnovel_premises\u001b[39m\u001b[38;5;124m\"\u001b[39m: split_by_premise(traced_theorems),\n\u001b[1;32m 11\u001b[0m }\n", + "\u001b[0;31mAttributeError\u001b[0m: 'LeanGitRepo' object has no attribute 'is_lean4'" ] } ], @@ -408,18 +418,10 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": null, "id": "7427982d", "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "4462\n" - ] - } - ], + "outputs": [], "source": [ "!cat ../leandojo_benchmark_4/corpus.jsonl | wc -l" ] @@ -434,21 +436,10 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": null, "id": "cbca21c9", "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "dict_keys(['path', 'imports', 'premises'])" - ] - }, - "execution_count": 11, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "corpus_path = DST_DIR / \"corpus.jsonl\"\n", "lines = list(corpus_path.open())\n", @@ -466,46 +457,20 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": null, "id": "f5c1920a", "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "('Mathlib/Data/Polynomial/FieldDivision.lean',\n", - " ['Mathlib/RingTheory/EuclideanDomain.lean',\n", - " 'lake-packages/lean4/src/lean/Init.lean',\n", - " 'Mathlib/Data/Polynomial/Derivative.lean',\n", - " 'Mathlib/Data/Polynomial/RingDivision.lean'])" - ] - }, - "execution_count": 12, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "file_in_corpus[\"path\"], file_in_corpus[\"imports\"]" ] }, { "cell_type": "code", - "execution_count": 13, + "execution_count": null, "id": "d801a0ae", "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "67" - ] - }, - "execution_count": 13, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "len(file_in_corpus[\"premises\"])" ] @@ -520,25 +485,10 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": null, "id": "b533d342", "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "{'full_name': 'Polynomial.derivative_rootMultiplicity_of_root',\n", - " 'code': 'theorem derivative_rootMultiplicity_of_root [CharZero R] {p : R[X]} {t : R} (hpt : p.IsRoot t) :\\n p.derivative.rootMultiplicity t = p.rootMultiplicity t - 1',\n", - " 'start': [34, 1],\n", - " 'end': [57, 20],\n", - " 'kind': 'commanddeclaration'}" - ] - }, - "execution_count": 14, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "file_in_corpus[\"premises\"][0]" ] @@ -558,21 +508,10 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": null, "id": "4fb19aa3", "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "102248" - ] - }, - "execution_count": 15, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "train_path = DST_DIR / \"random/train.json\"\n", "proofs_train = json.load(train_path.open())\n", @@ -589,21 +528,10 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": null, "id": "3cc47f7e", "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "dict_keys(['url', 'commit', 'file_path', 'full_name', 'start', 'end', 'traced_tactics'])" - ] - }, - "execution_count": 21, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "for proof in proofs_train[::-1]:\n", " if proof[\"traced_tactics\"] != []:\n", @@ -613,24 +541,10 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": null, "id": "3c2c36a7", "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "('https://github.com/leanprover-community/mathlib4',\n", - " '3ce43c18f614b76e161f911b75a3e1ef641620ff',\n", - " 'Mathlib/Order/Filter/Bases.lean',\n", - " \"Filter.countable_biInf_eq_iInf_seq'\")" - ] - }, - "execution_count": 22, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "proof[\"url\"], proof[\"commit\"], proof[\"file_path\"], proof[\"full_name\"]" ] @@ -645,21 +559,10 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": null, "id": "c29987ff", "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "5" - ] - }, - "execution_count": 23, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "len(proof[\"traced_tactics\"])" ] @@ -674,28 +577,10 @@ }, { "cell_type": "code", - "execution_count": 25, + "execution_count": null, "id": "a734d788", "metadata": {}, - "outputs": [ - { - "data": { - "text/plain": [ - "{'tactic': 'rw [hB, iInf_emptyset]',\n", - " 'annotated_tactic': ['rw [hB, iInf_emptyset]',\n", - " [{'full_name': 'iInf_emptyset',\n", - " 'def_path': 'Mathlib/Order/CompleteLattice.lean',\n", - " 'def_pos': [1466, 9],\n", - " 'def_end_pos': [1466, 22]}]],\n", - " 'state_before': \"case inl\\nα : Type u_1\\nβ : Type u_2\\nγ : Type u_3\\nι : Type u_4\\nι' : Sort u_5\\ninst✝ : CompleteLattice α\\nB : Set ι\\nBcbl : Set.Countable B\\nf : ι → α\\ni₀ : ι\\nh : f i₀ = ⊤\\nhB : B = ∅\\n⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)\",\n", - " 'state_after': \"case inl\\nα : Type u_1\\nβ : Type u_2\\nγ : Type u_3\\nι : Type u_4\\nι' : Sort u_5\\ninst✝ : CompleteLattice α\\nB : Set ι\\nBcbl : Set.Countable B\\nf : ι → α\\ni₀ : ι\\nh : f i₀ = ⊤\\nhB : B = ∅\\n⊢ ∃ x, ⊤ = ⨅ i, f (x i)\"}" - ] - }, - "execution_count": 25, - "metadata": {}, - "output_type": "execute_result" - } - ], + "outputs": [], "source": [ "proof[\"traced_tactics\"][1]" ] @@ -733,7 +618,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.10.13" + "version": "3.9.18" } }, "nbformat": 4, diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py index 7cd2d4f..1679d59 100644 --- a/src/lean_dojo/data_extraction/lean.py +++ b/src/lean_dojo/data_extraction/lean.py @@ -439,7 +439,7 @@ def __post_init__(self) -> None: # Determine the required Lean version. if (self.url, self.commit) in info_cache.lean_version: lean_version = info_cache.lean_version[(self.url, self.commit)] - elif self.url == LEAN4_URL: + elif self.is_lean4: lean_version = self.commit else: config = self.get_config("lean-toolchain") @@ -462,6 +462,10 @@ def from_path(cls, path: Path) -> "LeanGitRepo": def name(self) -> str: return self.repo.name + @property + def is_lean4(self) -> bool: + return self.url == LEAN4_URL + @property def commit_url(self) -> str: return os.path.join(self.url, f"tree/{self.commit}") diff --git a/src/lean_dojo/data_extraction/trace.py b/src/lean_dojo/data_extraction/trace.py index d9b0624..d406c9e 100644 --- a/src/lean_dojo/data_extraction/trace.py +++ b/src/lean_dojo/data_extraction/trace.py @@ -11,7 +11,7 @@ from .cache import cache from .lean import LeanGitRepo -from ..constants import NUM_PROCS, LEAN4_URL +from ..constants import NUM_PROCS from .traced_data import TracedRepo from ..utils import working_directory from ..container import create_mounts, get_container, NativeContainer @@ -27,7 +27,7 @@ def _trace(repo: LeanGitRepo, build_deps: bool) -> None: ), f"The {repo} does not exist. Please check the URL `{repo.commit_url}`." # Trace `repo` in the current working directory. - assert repo.url != LEAN4_URL, "Cannot trace Lean 4 itself." + assert not repo.is_lean4, "Cannot trace Lean 4 itself." repo.clone_and_checkout() logger.debug(f"Tracing {repo}")