awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this : Module.Finite R ↥i.ker
⊢ (ι →₀ R) ≃ₗ[R] M
have refine : Function.Injective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
Tactic: refine LinearEquiv.ofBijective i ⟨?_, hi⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this : Module.Finite R ↥i.ker
⊢ Function.Injective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
have rw : ∀ (y : k ⊗[R] ↥i.ker), y = 0
Tactic: rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot,
      ← IsLocalRing.subsingleton_tensorProduct (R := R), subsingleton_iff_forall_eq 0]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this : Module.Finite R ↥i.ker
⊢ ∀ (y : k ⊗[R] ↥i.ker), y = 0
have this₁ : Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
Tactic: have : Function.Surjective (i.baseChange k) := i.lTensor_surjective _ hi
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
⊢ Function.Bijective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
    (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
have refine : Function.Injective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
  (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
Tactic: refine ⟨?_, this⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
⊢ Function.Injective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
    (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
have rw : finrank k (k ⊗[R] (ι →₀ R)) = finrank k (k ⊗[R] M) + 0
Tactic: rw [← LinearMap.ker_eq_bot (M := k ⊗[R] (ι →₀ R)) (f := i.baseChange k),
        ← Submodule.finrank_eq_zero (R := k) (M := k ⊗[R] (ι →₀ R)),
        ← Nat.add_right_inj (n := Module.finrank k (LinearMap.range <| i.baseChange k)),
        LinearMap.finrank_range_add_finrank_ker (V := k ⊗[R] (ι →₀ R)),
        LinearMap.range_eq_top.mpr this, finrank_top]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
⊢ finrank k (k ⊗[R] (ι →₀ R)) = finrank k (k ⊗[R] M) + 0
have simp : Fintype.card ι = finrank k (k ⊗[R] M)
Tactic: simp only [Module.finrank_tensorProduct, Module.finrank_self,
        Module.finrank_finsupp_self, one_mul, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
⊢ Fintype.card ι = finrank k (k ⊗[R] M)
have rw : Fintype.card ι = Fintype.card ι
Tactic: rw [Module.finrank_eq_card_basis bk]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
⊢ ∀ (y : k ⊗[R] ↥i.ker), y = 0
have hi' : Function.Bijective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
  (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
Tactic: have hi' : Function.Bijective (i.baseChange k) := by
      refine ⟨?_, this⟩
      rw [← LinearMap.ker_eq_bot (M := k ⊗[R] (ι →₀ R)) (f := i.baseChange k),
        ← Submodule.finrank_eq_zero (R := k) (M := k ⊗[R] (ι →₀ R)),
        ← Nat.add_right_inj (n := Module.finrank k (LinearMap.range <| i.baseChange k)),
        LinearMap.finrank_range_add_finrank_ker (V := k ⊗[R] (ι →₀ R)),
        LinearMap.range_eq_top.mpr this, finrank_top]
      simp only [Module.finrank_tensorProduct, Module.finrank_self,
        Module.finrank_finsupp_self, one_mul, add_zero]
      rw [Module.finrank_eq_card_basis bk]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
hi' :
  Function.Bijective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
    (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
x : k ⊗[R] ↥i.ker
⊢ x = 0
have refine_1 : Function.Injective (α := R ⊗[R] ↥i.ker) (β := R ⊗[R] (ι →₀ R))
  (⇑(LinearMap.lTensor R i.ker.subtype) : (a : R ⊗[R] ↥i.ker) → R ⊗[R] (ι →₀ R))
Tactic: refine lTensor_injective_of_exact_of_exact_of_rTensor_injective
      (N₁ := LinearMap.ker i) (N₂ := ι →₀ R) (N₃ := M)
      (f₁ := (𝔪).subtype) (f₂ := Submodule.mkQ 𝔪)
      (g₁ := (LinearMap.ker i).subtype) (g₂ := i) (LinearMap.exact_subtype_mkQ 𝔪)
      (Submodule.mkQ_surjective _) (LinearMap.exact_subtype_ker_map i) hi H ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
hi' :
  Function.Bijective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
    (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
x : k ⊗[R] ↥i.ker
refine_1 :
  Function.Injective (α := R ⊗[R] ↥i.ker) (β := R ⊗[R] (ι →₀ R))
    (⇑(LinearMap.lTensor R i.ker.subtype) : (a : R ⊗[R] ↥i.ker) → R ⊗[R] (ι →₀ R))
⊢ x = 0
have refine_2 : Eq (α := HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R) ⊗[R] (ι →₀ R))
  ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
        (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
      x :
    HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R) ⊗[R] (ι →₀ R))
  ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
        (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
      0 :
    HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R) ⊗[R] (ι →₀ R))
Tactic: refine lTensor_injective_of_exact_of_exact_of_rTensor_injective
      (N₁ := LinearMap.ker i) (N₂ := ι →₀ R) (N₃ := M)
      (f₁ := (𝔪).subtype) (f₂ := Submodule.mkQ 𝔪)
      (g₁ := (LinearMap.ker i).subtype) (g₂ := i) (LinearMap.exact_subtype_mkQ 𝔪)
      (Submodule.mkQ_surjective _) (LinearMap.exact_subtype_ker_map i) hi H ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
hi' :
  Function.Bijective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
    (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
x : k ⊗[R] ↥i.ker
⊢ Function.Injective (α := R ⊗[R] ↥i.ker) (β := R ⊗[R] (ι →₀ R))
    (⇑(LinearMap.lTensor R i.ker.subtype) : (a : R ⊗[R] ↥i.ker) → R ⊗[R] (ι →₀ R))
have refine_1 : Function.Injective (α := ↥i.ker) (β := ι →₀ R) (⇑i.ker.subtype : (a : ↥i.ker) → ι →₀ R)
Tactic: apply Module.Flat.lTensor_preserves_injective_linearMap
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
hi' :
  Function.Bijective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
    (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
x : k ⊗[R] ↥i.ker
⊢ Eq (α := HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R) ⊗[R] (ι →₀ R))
    ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
          (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
        x :
      HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R) ⊗[R] (ι →₀ R))
    ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
          (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
        0 :
      HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R) ⊗[R] (ι →₀ R))
have refine_2 : Eq (α := k ⊗[R] M)
  ((LinearMap.baseChange k i : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
      ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
          (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
        x) :
    k ⊗[R] M)
  ((LinearMap.baseChange k i : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
      ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
          (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
        0) :
    k ⊗[R] M)
Tactic: apply hi'.injective
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
hi' :
  Function.Bijective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
    (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
x : k ⊗[R] ↥i.ker
⊢ Eq (α := k ⊗[R] M)
    ((LinearMap.lTensor k i : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
        ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
            (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
          x) :
      k ⊗[R] M)
    ((LinearMap.lTensor k i : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
        ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
            (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
          0) :
      k ⊗[R] M)
have refine_2 : Eq (α := k ⊗[R] M) ((LinearMap.lTensor k (i ∘ₗ i.ker.subtype) : (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → k ⊗[R] M) x : k ⊗[R] M)
  ((LinearMap.lTensor k i : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
      ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
          (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
        0) :
    k ⊗[R] M)
Tactic: erw [← LinearMap.comp_apply (i.lTensor k), ← LinearMap.lTensor_comp]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this_3 : Module.Finite R ↥i.ker
this :
  Surjective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M) (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
hi' :
  Function.Bijective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
    (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
x : k ⊗[R] ↥i.ker
⊢ Eq (α := k ⊗[R] M) ((LinearMap.lTensor k (i ∘ₗ i.ker.subtype) : (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → k ⊗[R] M) x : k ⊗[R] M)
    ((LinearMap.lTensor k i : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
        ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
            (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
          0) :
      k ⊗[R] M)
have refine_2 : Eq (α := k ⊗[R] M) ((LinearMap.lTensor k 0 : (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → k ⊗[R] M) x : k ⊗[R] M)
  ((LinearMap.lTensor k i : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)
      ((LinearMap.lTensor (HasQuotient.Quotient R (B := Submodule R R) (𝔪 : Ideal R)) i.ker.subtype :
          (a : (R ⧸ 𝔪) ⊗[R] ↥i.ker) → (R ⧸ 𝔪) ⊗[R] (ι →₀ R))
        0) :
    k ⊗[R] M)
Tactic: rw [(LinearMap.exact_subtype_ker_map i).linearMap_comp_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : FinitePresentation R M
ι : Type u_5
v : ι → M
hli :
  LinearIndependent k (M := k ⊗[R] M)
    ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)
hsp :
  Eq (α := Submodule k (k ⊗[R] M))
    (Submodule.span k
      (Set.range ((⇑((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) : (a : M) → k ⊗[R] M) ∘ v)))
    ⊤
H :
  Function.Injective (α := ↥𝔪 ⊗[R] M) (β := R ⊗[R] M)
    (⇑(LinearMap.rTensor M (Submodule.subtype 𝔪)) : (a : ↥𝔪 ⊗[R] M) → R ⊗[R] M)
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this_1 : Finite ι
this_2 : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective (α := ι →₀ R) (β := M) (⇑i : (a : ι →₀ R) → M)
this : Module.Finite R ↥i.ker
iequiv : (ι →₀ R) ≃ₗ[R] M := LinearEquiv.ofBijective i ⋯
⊢ ∃ (b : Basis ι R M), ∀ (i : ι), (b : (a : ι) → M) i = v i
have h : ∀ (i : ι), ({ repr := iequiv.symm : Basis ι R M } : (a : ι) → M) i = v i
Tactic: use Basis.ofRepr iequiv.symm