-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem LinearIndependent.pair_iff' {x y : V} (hx : x ≠ 0) :
    LinearIndependent K ![x, y] ↔ ∀ a : K, a • x ≠ y

Proof state:
case mp
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
⊢ (∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0) → ∀ (a : K), a • x ≠ y

Tactic:
intro H a ha

Result:
case mp
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0
a : K
ha : a • x = y
⊢ False

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
⊢ (∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (a : K), a • x ≠ y

Tactic:
constructor

Result:
case mp
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
⊢ (∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0) → ∀ (a : K), a • x ≠ y

case mpr
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
⊢ (∀ (a : K), a • x ≠ y) → ∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (a : K), a • x ≠ y
s t : K
ht : ¬t = 0
hst : (t⁻¹ * s) • x + 1 • y = t⁻¹ • 0
⊢ -(t⁻¹ * s) • x = y

Tactic:
linear_combination (norm := match_scalars <;> noncomm_ring) -hst

Result:
no goals

Proof state:
case mp
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0
a : K
ha : a • x = y
⊢ False

Tactic:
have := (H a (-1) (by simpa [← sub_eq_add_neg, sub_eq_zero])).2

Result:
case mp
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0
a : K
ha : a • x = y
this : -1 = 0
⊢ False

Proof state:
case mpr
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (a : K), a • x ≠ y
s t : K
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
by_cases ht : t = 0

Result:
case pos
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (a : K), a • x ≠ y
s t : K
hst : s • x + t • y = 0
ht : t = 0
⊢ s = 0 ∧ t = 0

case neg
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (a : K), a • x ≠ y
s t : K
hst : s • x + t • y = 0
ht : ¬t = 0
⊢ s = 0 ∧ t = 0

Proof state:
case mp
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0
a : K
ha : a • x = y
this : -1 = 0
⊢ False

Tactic:
simp only [neg_eq_zero, one_ne_zero] at this

Result:
no goals

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0
a : K
ha : a • x = y
⊢ a • x + -1 • y = 0

Tactic:
simpa [← sub_eq_add_neg, sub_eq_zero]

Result:
no goals

Proof state:
case pos
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (a : K), a • x ≠ y
s t : K
hst : s • x + t • y = 0
ht : t = 0
⊢ s = 0 ∧ t = 0

Tactic:
exact ⟨by simpa [ht, hx] using hst, ht⟩

Result:
no goals

Proof state:
case neg
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (a : K), a • x ≠ y
s t : K
ht : ¬t = 0
hst : (t⁻¹ * s) • x + 1 • y = t⁻¹ • 0
⊢ s = 0 ∧ t = 0

Tactic:
cases H (-(t⁻¹ * s)) <| by linear_combination (norm := match_scalars <;> noncomm_ring) -hst

Result:
no goals

Proof state:
case mpr
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
⊢ (∀ (a : K), a • x ≠ y) → ∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
intro H s t hst

Result:
case mpr
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (a : K), a • x ≠ y
s t : K
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
⊢ LinearIndependent K ![x, y] ↔ ∀ (a : K), a • x ≠ y

Tactic:
rw [LinearIndependent.pair_iff]

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
⊢ (∀ (s t : K), s • x + t • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (a : K), a • x ≠ y

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (a : K), a • x ≠ y
s t : K
hst : s • x + t • y = 0
ht : t = 0
⊢ s = 0

Tactic:
simpa [ht, hx] using hst

Result:
no goals

Proof state:
case neg
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (a : K), a • x ≠ y
s t : K
ht : ¬t = 0
hst : t⁻¹ • (s • x + t • y) = t⁻¹ • 0
⊢ s = 0 ∧ t = 0

Tactic:
simp only [smul_add, smul_smul, inv_mul_cancel₀ ht] at hst

Result:
case neg
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
H : ∀ (a : K), a • x ≠ y
s t : K
ht : ¬t = 0
hst : (t⁻¹ * s) • x + 1 • y = t⁻¹ • 0
⊢ s = 0 ∧ t = 0