ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<GOAL>Free R M
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<GOAL>Free R M
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<GOAL>Free R M
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<GOAL>Free R M
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝ : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this : Finite R ↥(LinearMap.ker i)<GOAL>Free R M
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝ : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this : Finite R ↥(LinearMap.ker i)<GOAL>Function.Injective ⇑i
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝ : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this : Finite R ↥(LinearMap.ker i)<GOAL>∀ (y : k ⊗[R] ↥(LinearMap.ker i)), y = 0
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝¹ : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this✝ : Finite R ↥(LinearMap.ker i)<VAR>this : Surjective ⇑(LinearMap.baseChange k i)<GOAL>∀ (y : k ⊗[R] ↥(LinearMap.ker i)), y = 0
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝¹ : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this✝ : Finite R ↥(LinearMap.ker i)<VAR>this : Surjective ⇑(LinearMap.baseChange k i)<VAR>hi' : Function.Bijective ⇑(LinearMap.baseChange k i)<GOAL>∀ (y : k ⊗[R] ↥(LinearMap.ker i)), y = 0
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝² : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this✝¹ : Finite R ↥(LinearMap.ker i)<VAR>this✝ : Surjective ⇑(LinearMap.baseChange k i)<VAR>hi' : Function.Bijective ⇑(LinearMap.baseChange k i)<VAR>this : ∀ {g₁ : ↥(LinearMap.ker i) →ₗ[R] I →₀ R} {g₂ : (I →₀ R) →ₗ[R] M}, Exact ⇑(Submodule.subtype 𝔪) ⇑(Submodule.mkQ 𝔪) → Surjective ⇑(Submodule.mkQ 𝔪) → Exact ⇑g₁ ⇑g₂ → Surjective ⇑g₂ → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) → Function.Injective ⇑(LinearMap.lTensor R g₁) → Function.Injective ⇑(LinearMap.lTensor (R ⧸ 𝔪) g₁)<GOAL>∀ (y : k ⊗[R] ↥(LinearMap.ker i)), y = 0
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝² : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this✝¹ : Finite R ↥(LinearMap.ker i)<VAR>this✝ : Surjective ⇑(LinearMap.baseChange k i)<VAR>hi' : Function.Bijective ⇑(LinearMap.baseChange k i)<VAR>this : ∀ {g₁ : ↥(LinearMap.ker i) →ₗ[R] I →₀ R} {g₂ : (I →₀ R) →ₗ[R] M}, Exact ⇑(Submodule.subtype 𝔪) ⇑(Submodule.mkQ 𝔪) → Surjective ⇑(Submodule.mkQ 𝔪) → Exact ⇑g₁ ⇑g₂ → Surjective ⇑g₂ → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) → Function.Injective ⇑(LinearMap.lTensor R g₁) → Function.Injective ⇑(LinearMap.lTensor (R ⧸ 𝔪) g₁)<VAR>x : k ⊗[R] ↥(LinearMap.ker i)<GOAL>x = 0
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝² : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this✝¹ : Finite R ↥(LinearMap.ker i)<VAR>this✝ : Surjective ⇑(LinearMap.baseChange k i)<VAR>hi' : Function.Bijective ⇑(LinearMap.baseChange k i)<VAR>this : ∀ {g₁ : ↥(LinearMap.ker i) →ₗ[R] I →₀ R} {g₂ : (I →₀ R) →ₗ[R] M}, Exact ⇑(Submodule.subtype 𝔪) ⇑(Submodule.mkQ 𝔪) → Surjective ⇑(Submodule.mkQ 𝔪) → Exact ⇑g₁ ⇑g₂ → Surjective ⇑g₂ → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) → Function.Injective ⇑(LinearMap.lTensor R g₁) → Function.Injective ⇑(LinearMap.lTensor (R ⧸ 𝔪) g₁)<VAR>x : k ⊗[R] ↥(LinearMap.ker i)<GOAL>(LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) x = (LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) 0
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝² : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this✝¹ : Finite R ↥(LinearMap.ker i)<VAR>this✝ : Surjective ⇑(LinearMap.baseChange k i)<VAR>hi' : Function.Bijective ⇑(LinearMap.baseChange k i)<VAR>this : ∀ {g₁ : ↥(LinearMap.ker i) →ₗ[R] I →₀ R} {g₂ : (I →₀ R) →ₗ[R] M}, Exact ⇑(Submodule.subtype 𝔪) ⇑(Submodule.mkQ 𝔪) → Surjective ⇑(Submodule.mkQ 𝔪) → Exact ⇑g₁ ⇑g₂ → Surjective ⇑g₂ → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) → Function.Injective ⇑(LinearMap.lTensor R g₁) → Function.Injective ⇑(LinearMap.lTensor (R ⧸ 𝔪) g₁)<VAR>x : k ⊗[R] ↥(LinearMap.ker i)<GOAL>(LinearMap.baseChange k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) x) = (LinearMap.baseChange k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) 0)
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝² : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this✝¹ : Finite R ↥(LinearMap.ker i)<VAR>this✝ : Surjective ⇑(LinearMap.baseChange k i)<VAR>hi' : Function.Bijective ⇑(LinearMap.baseChange k i)<VAR>this : ∀ {g₁ : ↥(LinearMap.ker i) →ₗ[R] I →₀ R} {g₂ : (I →₀ R) →ₗ[R] M}, Exact ⇑(Submodule.subtype 𝔪) ⇑(Submodule.mkQ 𝔪) → Surjective ⇑(Submodule.mkQ 𝔪) → Exact ⇑g₁ ⇑g₂ → Surjective ⇑g₂ → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) → Function.Injective ⇑(LinearMap.lTensor R g₁) → Function.Injective ⇑(LinearMap.lTensor (R ⧸ 𝔪) g₁)<VAR>x : k ⊗[R] ↥(LinearMap.ker i)<GOAL>(LinearMap.lTensor k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) x) = (LinearMap.lTensor k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) 0)
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝² : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this✝¹ : Finite R ↥(LinearMap.ker i)<VAR>this✝ : Surjective ⇑(LinearMap.baseChange k i)<VAR>hi' : Function.Bijective ⇑(LinearMap.baseChange k i)<VAR>this : ∀ {g₁ : ↥(LinearMap.ker i) →ₗ[R] I →₀ R} {g₂ : (I →₀ R) →ₗ[R] M}, Exact ⇑(Submodule.subtype 𝔪) ⇑(Submodule.mkQ 𝔪) → Surjective ⇑(Submodule.mkQ 𝔪) → Exact ⇑g₁ ⇑g₂ → Surjective ⇑g₂ → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) → Function.Injective ⇑(LinearMap.lTensor R g₁) → Function.Injective ⇑(LinearMap.lTensor (R ⧸ 𝔪) g₁)<VAR>x : k ⊗[R] ↥(LinearMap.ker i)<GOAL>(LinearMap.lTensor k (i ∘ₗ (LinearMap.ker i).subtype)) x = (LinearMap.lTensor k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) 0)
<VAR>R : Type u_1<VAR>S : Type ?u.189967<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N : Type ?u.190432<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>P : Type ?u.191572<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f✝ ⇑g<VAR>inst✝ : FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))<VAR>I : Type (max u_2 u_1) := Free.ChooseBasisIndex k (k ⊗[R] M)<VAR>b : Basis I k (k ⊗[R] M) := Free.chooseBasis k (k ⊗[R] M)<VAR>this✝² : IsNoetherian k (k ⊗[R] (I →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (I →₀ R))<VAR>f : k ⊗[R] M → M<VAR>hf : ∀ (b : k ⊗[R] M), ((TensorProduct.mk R k M) 1) (f b) = b<VAR>i : (I →₀ R) →ₗ[R] M := Finsupp.total I M R (f ∘ ⇑b)<VAR>hi : Surjective ⇑i<VAR>this✝¹ : Finite R ↥(LinearMap.ker i)<VAR>this✝ : Surjective ⇑(LinearMap.baseChange k i)<VAR>hi' : Function.Bijective ⇑(LinearMap.baseChange k i)<VAR>this : ∀ {g₁ : ↥(LinearMap.ker i) →ₗ[R] I →₀ R} {g₂ : (I →₀ R) →ₗ[R] M}, Exact ⇑(Submodule.subtype 𝔪) ⇑(Submodule.mkQ 𝔪) → Surjective ⇑(Submodule.mkQ 𝔪) → Exact ⇑g₁ ⇑g₂ → Surjective ⇑g₂ → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) → Function.Injective ⇑(LinearMap.lTensor R g₁) → Function.Injective ⇑(LinearMap.lTensor (R ⧸ 𝔪) g₁)<VAR>x : k ⊗[R] ↥(LinearMap.ker i)<GOAL>(LinearMap.lTensor k 0) x = (LinearMap.lTensor k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) 0)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f✝ : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>g : M →ₗ[R] Q<VAR>this : Fact (Function.Injective ⇑f)<VAR>x y : N<GOAL>(fun x => ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩) (x + y) = (fun x => ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩) x + (fun x => ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩) y
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f✝ : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>g : M →ₗ[R] Q<VAR>this : Fact (Function.Injective ⇑f)<VAR>x y : N<GOAL>(fun x => ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩) (x + y) = ↑(extensionOfMax f g).toLinearPMap (⟨x, ⋯⟩ + ⟨y, ⋯⟩)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f✝ : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>g : M →ₗ[R] Q<VAR>this : Fact (Function.Injective ⇑f)<VAR>r : R<VAR>x : N<GOAL>{ toFun := fun x => ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩, map_add' := ⋯ }.toFun (r • x) = (RingHom.id R) r • { toFun := fun x => ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩, map_add' := ⋯ }.toFun x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f✝ : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<VAR>g : M →ₗ[R] Q<VAR>this : Fact (Function.Injective ⇑f)<VAR>r : R<VAR>x : N<GOAL>{ toFun := fun x => ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩, map_add' := ⋯ }.toFun (r • x) = ↑(extensionOfMax f g).toLinearPMap ((RingHom.id R) r • ⟨x, ⋯⟩)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<GOAL>(engel R x).normalizer = engel R x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<GOAL>(engel R x).normalizer ≤ engel R x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x y : L<VAR>hy : y ∈ (engel R x).normalizer<GOAL>y ∈ engel R x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x y : L<VAR>hy : ∀ y_1 ∈ engel R x, ⁅y, y_1⁆ ∈ engel R x<GOAL>y ∈ engel R x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x y : L<VAR>hy : ⁅y, x⁆ ∈ engel R x<GOAL>y ∈ engel R x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x y : L<VAR>hy : ∃ n, ((ad R L) x ^ n) ⁅x, y⁆ = 0<GOAL>y ∈ engel R x