-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem FinrankQuotientMap.linearIndependent_of_nontrivial [IsDedekindDomain R]
    (hRS : RingHom.ker (algebraMap R S) ≠ ⊤) (f : V'' →ₗ[R] V) (hf : Function.Injective f)
    (f' : V'' →ₗ[R] V') {ι : Type*} {b : ι → V''} (hb' : LinearIndependent S (f' ∘ b)) :
    LinearIndependent K (f ∘ b)

Proof state:
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker (algebraMap R S) ≠ ⊤
f : V'' →ₗ[R] V
hf : Function.Injective ⇑f
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI✝ : a * g j ∉ ↑(RingHom.ker (algebraMap R S))
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i => if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i
hgI : (algebraMap R S) (g' j) ≠ 0
⊢ ∀ x ∈ s, f (g' x • b x) = a • g x • (⇑f ∘ b) x

Tactic:
intro i hi

Result:
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker (algebraMap R S) ≠ ⊤
f : V'' →ₗ[R] V
hf : Function.Injective ⇑f
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI✝ : a * g j ∉ ↑(RingHom.ker (algebraMap R S))
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i => if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i
hgI : (algebraMap R S) (g' j) ≠ 0
i : ι
hi : i ∈ s
⊢ f (g' i • b i) = a • g i • (⇑f ∘ b) i

Proof state:
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker (algebraMap R S) ≠ ⊤
f : V'' →ₗ[R] V
hf : Function.Injective ⇑f
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb : ¬LinearIndependent K (⇑f ∘ b)
⊢ ¬LinearIndependent S (⇑f' ∘ b)

Tactic:
simp only [linearIndependent_iff', not_forall] at hb ⊢

Result:
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker (algebraMap R S) ≠ ⊤
f : V'' →ₗ[R] V
hf : Function.Injective ⇑f
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb : ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • (⇑f ∘ b) i = 0), ∃ x_2, ∃ (_ : x_2 ∈ x), ¬x_1 x_2 = 0
⊢ ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • (⇑f' ∘ b) i = 0), ∃ x_2, ∃ (_ : x_2 ∈ x), ¬x_1 x_2 = 0

Proof state:
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker (algebraMap R S) ≠ ⊤
f : V'' →ₗ[R] V
hf : Function.Injective ⇑f
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI : a * g j ∉ ↑(RingHom.ker (algebraMap R S))
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i => if h : i ∈ s then g'' i h else 0
⊢ ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i

Tactic:
intro i hi

Result:
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker (algebraMap R S) ≠ ⊤
f : V'' →ₗ[R] V
hf : Function.Injective ⇑f
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI : a * g j ∉ ↑(RingHom.ker (algebraMap R S))
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i => if h : i ∈ s then g'' i h else 0
i : ι
hi : i ∈ s
⊢ (algebraMap R K) (g' i) = a * g i