-- Mathlib/LinearAlgebra/Dimension/Localization.lean
lemma IsLocalizedModule.linearIndependent_lift {ι} {v : ι → N} (hf : LinearIndependent S v) :
    ∃ w : ι → M, LinearIndependent R w

Proof state:
case h.a.a
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
sec : N → M × ↥p
hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1
t : Finset ι
g : ι → R
hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0
i : ι
hit : i ∈ t
⊢ (algebraMap R S) (g i * ↑(sec (v i)).2) = 0

Tactic:
refine hf t (fun i ↦ algebraMap R S (g i * (sec (v i)).2)) ?_ _ hit

Result:
case h.a.a
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
sec : N → M × ↥p
hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1
t : Finset ι
g : ι → R
hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0
i : ι
hit : i ∈ t
⊢ ∑ i ∈ t, (fun i => (algebraMap R S) (g i * ↑(sec (v i)).2)) i • v i = 0

Proof state:
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : LinearIndependent S v
⊢ ∃ w, LinearIndependent R w

Tactic:
choose sec hsec using IsLocalizedModule.surj p f

Result:
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : LinearIndependent S v
sec : N → M × ↥p
hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1
⊢ ∃ w, LinearIndependent R w

Proof state:
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : LinearIndependent S v
sec : N → M × ↥p
hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1
⊢ ∃ w, LinearIndependent R w

Tactic:
use fun i ↦ (sec (v i)).1

Result:
case h
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : LinearIndependent S v
sec : N → M × ↥p
hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1
⊢ LinearIndependent R fun i => (sec (v i)).1

Proof state:
case h
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
sec : N → M × ↥p
hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1
⊢ ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (sec (v i)).1 = 0 → ∀ i ∈ s, g i = 0

Tactic:
intro t g hg i hit

Result:
case h
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
sec : N → M × ↥p
hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1
t : Finset ι
g : ι → R
hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0
i : ι
hit : i ∈ t
⊢ g i = 0

Proof state:
case h.a.a
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
sec : N → M × ↥p
hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1
t : Finset ι
g : ι → R
hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0
i : ι
hit : i ∈ t
⊢ (algebraMap R S) (g i * ↑(sec (v i)).2) = (algebraMap R S) 0

Tactic:
rw [map_zero]

Result:
case h.a.a
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
sec : N → M × ↥p
hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1
t : Finset ι
g : ι → R
hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0
i : ι
hit : i ∈ t
⊢ (algebraMap R S) (g i * ↑(sec (v i)).2) = 0

Proof state:
case h
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
sec : N → M × ↥p
hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1
t : Finset ι
g : ι → R
hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0
i : ι
hit : i ∈ t
⊢ g i = 0

Tactic:
apply hp (sec (v i)).2.prop

Result:
case h.a
R : Type u
S : Type u'
M : Type v
N : Type v'
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
ι : Type u_1
v : ι → N
hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
sec : N → M × ↥p
hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1
t : Finset ι
g : ι → R
hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0
i : ι
hit : i ∈ t
⊢ g i * ↑(sec (v i)).2 = 0