Theorem: linearIndependent_restrict_pair_iff (Matroid/ForMathlib/LinearAlgebra/LinearIndependent.lean)

State before:
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
⊢ LinearIndependent (ι := ↑{i, j}) K ({i, j}.restrict f) ↔ ∀ (c : K), c • f i ≠ f j
Tactic:
convert linearIndependent_insert' (s := {j}) (a := i) (by simpa using hij) using 2
State after:
case h.e'_2.a
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
⊢ (∀ (c : K), c • f i ≠ f j) ↔ (LinearIndependent K fun (x : ↑{j}) => f ↑x) ∧ f i ∉ span K (f '' {j})

State before:
case h.e'_2.a
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
⊢ (∀ (c : K), c • f i ≠ f j) ↔ (LinearIndependent K fun (x : ↑{j}) => f ↑x) ∧ f i ∉ span K (f '' {j})
Tactic:
simp only [ne_eq, linearIndependent_unique_iff, default_coe_singleton, image_singleton,
  mem_span_singleton, not_exists]
State after:
case h.e'_2.a
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
⊢ (∀ (c : K), ¬c • f i = f j) ↔ ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i

State before:
case h.e'_2.a
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
⊢ (∀ (c : K), ¬c • f i = f j) ↔ ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i
Tactic:
refine ⟨fun h ↦ ⟨fun h0 ↦ ?_, fun c hc ↦ h c⁻¹ ?_⟩, fun h c h' ↦ h.2 c⁻¹ ?_⟩
State after:
case h.e'_2.a.refine_1
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ∀ (c : K), ¬c • f i = f j
h0 : f j = 0
⊢ False

case h.e'_2.a.refine_2
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ∀ (c : K), ¬c • f i = f j
c : K
hc : c • f j = f i
⊢ c⁻¹ • f i = f j

case h.e'_2.a.refine_3
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i
c : K
h' : c • f i = f j
⊢ c⁻¹ • f j = f i

State before:
case h.e'_2.a.refine_3
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i
c : K
h' : c • f i = f j
⊢ c⁻¹ • f j = f i
Tactic:
rw [← h', smul_smul, inv_mul_cancel, one_smul]
State after:
case h.e'_2.a.refine_3
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i
c : K
h' : c • f i = f j
⊢ c ≠ 0

State before:
case h.e'_2.a.refine_3
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i
c : K
h' : c • f i = f j
⊢ c ≠ 0
Tactic:
rintro rfl
State after:
case h.e'_2.a.refine_3
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i
h' : 0 • f i = f j
⊢ False

State before:
case h.e'_2.a.refine_3
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i
h' : 0 • f i = f j
⊢ False
Tactic:
exact h.1 <| by simp [← h']
State after:
no goals

State before:
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
⊢ i ∉ {j}
Tactic:
simpa using hij
State after:
no goals

State before:
case h.e'_2.a.refine_1
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ∀ (c : K), ¬c • f i = f j
h0 : f j = 0
⊢ False
Tactic:
simp only [h0, smul_eq_zero] at h
State after:
case h.e'_2.a.refine_1
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h0 : f j = 0
h : ∀ (c : K), ¬(c = 0 ∨ f i = 0)
⊢ False

State before:
case h.e'_2.a.refine_1
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h0 : f j = 0
h : ∀ (c : K), ¬(c = 0 ∨ f i = 0)
⊢ False
Tactic:
simpa using h 0
State after:
no goals

State before:
case h.e'_2.a.refine_2
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ∀ (c : K), ¬c • f i = f j
c : K
hc : c • f j = f i
⊢ c⁻¹ • f i = f j
Tactic:
rw [← hc, smul_smul, inv_mul_cancel, one_smul]
State after:
case h.e'_2.a.refine_2
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ∀ (c : K), ¬c • f i = f j
c : K
hc : c • f j = f i
⊢ c ≠ 0

State before:
case h.e'_2.a.refine_2
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ∀ (c : K), ¬c • f i = f j
c : K
hc : c • f j = f i
⊢ c ≠ 0
Tactic:
rintro rfl
State after:
case h.e'_2.a.refine_2
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ∀ (c : K), ¬c • f i = f j
hc : 0 • f j = f i
⊢ False

State before:
case h.e'_2.a.refine_2
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ∀ (c : K), ¬c • f i = f j
hc : 0 • f j = f i
⊢ False
Tactic:
exact hi <| by simp [← hc]
State after:
no goals

State before:
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ∀ (c : K), ¬c • f i = f j
hc : 0 • f j = f i
⊢ f i = 0
Tactic:
simp [← hc]
State after:
no goals

State before:
α : Type u_1
ι✝¹ : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁷ : AddCommGroup W
inst✝⁶ : AddCommGroup W'
K✝ : Type u_7
V✝ : Type u_8
ι✝ : Type u_9
inst✝⁵ : DivisionRing K✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module K✝ V✝
f✝ : ι✝ → V✝
s₀ s t : Set ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i
h' : 0 • f i = f j
⊢ f j = 0
Tactic:
simp [← h']
State after:
no goals