-- Mathlib/RingTheory/LocalRing/Module.lean
/-- If `M` is of finite presentation over a local ring `(R, 𝔪, k)` such that
`𝔪 ⊗ M → M` is injective, then every family of elements that is a `k`-basis of
`k ⊗ M` is an `R`-basis of `M`. -/
lemma exists_basis_of_basis_baseChange [Module.FinitePresentation R M]
    {ι : Type u} (v : ι → M) (hli : LinearIndependent k (TensorProduct.mk R k M 1 ∘ v))
    (hsp : Submodule.span k (Set.range (TensorProduct.mk R k M 1 ∘ v)) = ⊤)
    (H : Function.Injective ((𝔪).subtype.rTensor M)) :
    ∃ (b : Basis ι R M), ∀ i, b i = v i

Proof state:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝³ : Finite ι
this✝² : Fintype ι := Fintype.ofFinite ι
this✝¹ : IsNoetherian k (k ⊗[R] (ι →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (ι →₀ R))
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this✝ : Module.Finite R ↥(LinearMap.ker i)
this : Surjective ⇑(LinearMap.baseChange k i)
hi' : Function.Bijective ⇑(LinearMap.baseChange k i)
x : k ⊗[R] ↥(LinearMap.ker i)
⊢ (LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) x = (LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) 0

Tactic:
apply hi'.injective

Result:
case refine_2.a
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝³ : Finite ι
this✝² : Fintype ι := Fintype.ofFinite ι
this✝¹ : IsNoetherian k (k ⊗[R] (ι →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (ι →₀ R))
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this✝ : Module.Finite R ↥(LinearMap.ker i)
this : Surjective ⇑(LinearMap.baseChange k i)
hi' : Function.Bijective ⇑(LinearMap.baseChange k i)
x : k ⊗[R] ↥(LinearMap.ker i)
⊢ (LinearMap.baseChange k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) x) =
    (LinearMap.baseChange k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) 0)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝³ : Finite ι
this✝² : Fintype ι := Fintype.ofFinite ι
this✝¹ : IsNoetherian k (k ⊗[R] (ι →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (ι →₀ R))
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this✝ : Module.Finite R ↥(LinearMap.ker i)
this : Surjective ⇑(LinearMap.baseChange k i)
⊢ Function.Injective ⇑(LinearMap.baseChange k i)

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]

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝³ : Finite ι
this✝² : Fintype ι := Fintype.ofFinite ι
this✝¹ : IsNoetherian k (k ⊗[R] (ι →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (ι →₀ R))
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this✝ : Module.Finite R ↥(LinearMap.ker i)
this : Surjective ⇑(LinearMap.baseChange k i)
⊢ finrank k (k ⊗[R] (ι →₀ R)) = finrank k (k ⊗[R] M) + 0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝² : Finite ι
this✝¹ : Fintype ι := Fintype.ofFinite ι
this✝ : IsNoetherian k (k ⊗[R] (ι →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (ι →₀ R))
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this : Module.Finite R ↥(LinearMap.ker i)
⊢ (ι →₀ R) ≃ₗ[R] M

Tactic:
refine LinearEquiv.ofBijective i ⟨?_, hi⟩

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝² : Finite ι
this✝¹ : Fintype ι := Fintype.ofFinite ι
this✝ : IsNoetherian k (k ⊗[R] (ι →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (ι →₀ R))
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this : Module.Finite R ↥(LinearMap.ker i)
⊢ Function.Injective ⇑i