awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Module
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
⊢ 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
-- Module: Mathlib.RingTheory.LocalRing.Module
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)

Tactic:
⟨?_, this⟩

Premises used: And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.LocalRing.Module
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)
refine :
  Function.Injective (α := 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)

Tactic:
refine ⟨?_, this⟩
-- Module: Mathlib.RingTheory.LocalRing.Module
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)
rw : finrank k (k ⊗[R] (ι →₀ R)) = finrank k (k ⊗[R] M) + 0
⊢ Function.Injective (α := k ⊗[R] (ι →₀ R)) (β := k ⊗[R] M)
    (⇑(LinearMap.baseChange k i) : (a : k ⊗[R] (ι →₀ R)) → k ⊗[R] M)

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]

Premises used: Iff.mpr, LinearMap.range_eq_top, finrank_top
-- Module: Mathlib.RingTheory.LocalRing.Module
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)
simp : Fintype.card ι = finrank k (k ⊗[R] M)
⊢ finrank k (k ⊗[R] (ι →₀ R)) = finrank k (k ⊗[R] M) + 0

Tactic:
simp only [Module.finrank_tensorProduct, Module.finrank_self,
        Module.finrank_finsupp_self, one_mul, add_zero]

Premises used: Module.finrank_tensorProduct, Module.finrank_finsupp_self, Module.finrank_self, add_zero, one_mul
-- Module: Mathlib.RingTheory.LocalRing.Module
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)
rw rw₁ : Fintype.card ι = Fintype.card ι
⊢ Fintype.card ι = finrank k (k ⊗[R] M)

Tactic:
rw [Module.finrank_eq_card_basis bk]

Premises used: Module.finrank_eq_card_basis
-- Module: Mathlib.RingTheory.LocalRing.Module
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)

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]
-- Module: Mathlib.RingTheory.LocalRing.Module
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

Tactic:
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 ?_ ?_

Premises used: lTensor_injective_of_exact_of_exact_of_rTensor_injective, Set.Mem, LinearMap.exact_subtype_mkQ, IsLocalRing.maximalIdeal, IsLocalRing.ResidueField, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.LocalRing.Module
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))
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))
⊢ x = 0

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 ?_ ?_
-- Module: Mathlib.RingTheory.LocalRing.Module
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 (α := ↥i.ker) (β := ι →₀ R) (⇑i.ker.subtype : (a : ↥i.ker) → ι →₀ R)
⊢ Function.Injective (α := R ⊗[R] ↥i.ker) (β := R ⊗[R] (ι →₀ R))
    (⇑(LinearMap.lTensor R i.ker.subtype) : (a : R ⊗[R] ↥i.ker) → R ⊗[R] (ι →₀ R))

Tactic:
apply Module.Flat.lTensor_preserves_injective_linearMap

Premises used: Module.Flat.lTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.LocalRing.Module
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 (α := ↥i.ker) (β := ι →₀ R) (⇑i.ker.subtype : (a : ↥i.ker) → ι →₀ R)

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.RingTheory.LocalRing.Module
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 (α := ↥i.ker) (β := ι →₀ R) (⇑i.ker.subtype : (a : ↥i.ker) → ι →₀ R)

Tactic:
exact Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.RingTheory.LocalRing.Module
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_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)
⊢ 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:
apply hi'.injective

Premises used: Function.Bijective.injective
-- Module: Mathlib.RingTheory.LocalRing.Module
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_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)
⊢ 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)

Tactic:
erw [← LinearMap.comp_apply (i.lTensor k), ← LinearMap.lTensor_comp]

Premises used: LinearMap.lTensor_comp