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

Tactic:
let i := Finsupp.linearCombination R v

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
⊢ ∃ 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 𝔪))
⊢ ⊤ ≤ Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v))

Tactic:
rw [hsp]

Result:
no goals

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

Tactic:
simp only [LinearMap.lTensor_zero, LinearMap.zero_apply, map_zero]

Result:
no goals

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
x✝ : ι
⊢ 1 ⊗ₜ[R] v x✝ = bk x✝

Tactic:
simp [bk]

Result:
no goals

Proof state:
case h
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)
iequiv : (ι →₀ R) ≃ₗ[R] M := LinearEquiv.ofBijective i ⋯
⊢ ∀ (i : ι), { repr := iequiv.symm } i = v i

Tactic:
intro j

Result:
case h
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)
iequiv : (ι →₀ R) ≃ₗ[R] M := LinearEquiv.ofBijective i ⋯
j : ι
⊢ { repr := iequiv.symm } j = v j

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

Tactic:
rw [(LinearMap.exact_subtype_ker_map i).linearMap_comp_eq_zero]

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