-- 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.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)

Tactic:
rw [LinearMap.baseChange_eq_ltensor]

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.lTensor k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) x) =
    (LinearMap.lTensor k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) 0)

Proof state:
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.lTensor k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) x) =
    (LinearMap.lTensor k i) ((LinearMap.lTensor (R ⧸ 𝔪) (LinearMap.ker i).subtype) 0)

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

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.lTensor k (i ∘ₗ (LinearMap.ker i).subtype)) x =
    (LinearMap.lTensor 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 𝔪))
⊢ ∃ b, ∀ (i : ι), b i = v i

Tactic:
let bk : Basis ι k (k ⊗[R] M) := Basis.mk hli (by rw [hsp])

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 ⋯
⊢ ∃ b, ∀ (i : ι), b i = v i

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)
⊢ ∀ (y : k ⊗[R] ↥(LinearMap.ker i)), y = 0

Tactic:
have : Function.Surjective (i.baseChange k) := i.lTensor_surjective _ 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)
this : Surjective ⇑(LinearMap.baseChange k i)
⊢ ∀ (y : k ⊗[R] ↥(LinearMap.ker i)), y = 0