internlm/Lean-Github huggingface dataset:
Theorem: exists_linearIndependent_extension'
Proof state before:
case 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 ι
hli : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
hzorn :
  ∃ m ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)},
    s₀ ⊆ m ∧ ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
⊢ ∃ s, s₀ ⊆ s ∧ s ⊆ t ∧ f '' t ⊆ ↑(span K (f '' s)) ∧ LinearIndependent (ι := ↑s) K (s.restrict f)
Tactic:
obtain ⟨m, ⟨hs₀m, hmt, hli⟩, -, hmax⟩ := hzorn
Proof state after:
case refine_2.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
⊢ ∃ s, s₀ ⊆ s ∧ s ⊆ t ∧ f '' t ⊆ ↑(span K (f '' s)) ∧ LinearIndependent (ι := ↑s) K (s.restrict f)
Theorem: exists_linearIndependent_extension'
Proof state before:
case refine_2.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
⊢ ∃ s, s₀ ⊆ s ∧ s ⊆ t ∧ f '' t ⊆ ↑(span K (f '' s)) ∧ LinearIndependent (ι := ↑s) K (s.restrict f)
Tactic:
refine ⟨m, hs₀m, hmt, ?_, hli⟩
Proof state after:
case refine_2.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
⊢ f '' t ⊆ ↑(span K (f '' m))
Theorem: exists_linearIndependent_extension'
Proof state before:
case refine_2.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
⊢ f '' t ⊆ ↑(span K (f '' m))
Tactic:
rintro _ ⟨x, hx, rfl⟩
Proof state after:
case refine_2.intro.intro.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
x : ι
hx : x ∈ t
⊢ f x ∈ ↑(span K (f '' m))
Theorem: exists_linearIndependent_extension'
Proof state before:
case refine_2.intro.intro.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
x : ι
hx : x ∈ t
⊢ f x ∈ ↑(span K (f '' m))
Tactic:
by_contra hxm
Proof state after:
case refine_2.intro.intro.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
x : ι
hx : x ∈ t
hxm : f x ∉ ↑(span K (f '' m))
⊢ False
Theorem: exists_linearIndependent_extension'
Proof state before:
case refine_2.intro.intro.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
x : ι
hx : x ∈ t
hxm : f x ∉ ↑(span K (f '' m))
⊢ False
Tactic:
have hxm' : x ∉ m := fun hxm' ↦ hxm <| subset_span <| mem_image_of_mem _ hxm'
Proof state after:
case refine_2.intro.intro.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
x : ι
hx : x ∈ t
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ m
⊢ False
Theorem: exists_linearIndependent_extension'
Proof state before:
case refine_2.intro.intro.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
x : ι
hx : x ∈ t
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ m
⊢ False
Tactic:
have hli' := (linearIndependent_insert' hxm').2 ⟨hli, hxm⟩
Proof state after:
case refine_2.intro.intro.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
x : ι
hx : x ∈ t
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ m
hli' : LinearIndependent K fun (x_1 : ↑(insert x m)) => f ↑x_1
⊢ False
Theorem: exists_linearIndependent_extension'
Proof state before:
case refine_2.intro.intro.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
x : ι
hx : x ∈ t
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ m
hli' : LinearIndependent K fun (x_1 : ↑(insert x m)) => f ↑x_1
⊢ False
Tactic:
rw [← hmax _ ⟨hs₀m.trans <| subset_insert _ _, insert_subset hx hmt, hli'⟩ (subset_insert _ _)]
  at hxm'
Proof state after:
case refine_2.intro.intro.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
x : ι
hx : x ∈ t
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ insert x m
hli' : LinearIndependent K fun (x_1 : ↑(insert x m)) => f ↑x_1
⊢ False
Theorem: exists_linearIndependent_extension'
Proof state before:
case refine_2.intro.intro.intro.intro.intro.intro.intro
α : 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 ι
hli✝ : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
x : ι
hx : x ∈ t
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ insert x m
hli' : LinearIndependent K fun (x_1 : ↑(insert x m)) => f ↑x_1
⊢ False
Tactic:
exact hxm' <| mem_insert _ _
Proof state after:
no goals
Theorem: linearIndependent_restrict_pair_iff
Proof 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
Proof 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})
Theorem: linearIndependent_restrict_pair_iff
Proof 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]
Proof 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
Theorem: linearIndependent_restrict_pair_iff
Proof 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⁻¹ ?_⟩
Proof 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
Theorem: linearIndependent_restrict_pair_iff
Proof 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]
Proof 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
Theorem: linearIndependent_restrict_pair_iff
Proof 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
Proof 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
Theorem: linearIndependent_restrict_pair_iff
Proof 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']
Proof state after:
no goals
Theorem: linearIndependent_restrict_pair_iff
Proof 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
Proof state after:
no goals
Theorem: linearIndependent_restrict_pair_iff
Proof 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
Proof 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
Theorem: linearIndependent_restrict_pair_iff
Proof 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
Proof state after:
no goals
Theorem: linearIndependent_restrict_pair_iff
Proof 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]
Proof 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
Theorem: linearIndependent_restrict_pair_iff
Proof 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
Proof 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
Theorem: linearIndependent_restrict_pair_iff
Proof 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]
Proof state after:
no goals
Theorem: linearIndependent_restrict_pair_iff
Proof 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]
Proof state after:
no goals