Theorem: LinearIndependent.union_index' (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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict (⇑(span R (f '' s)).mkQ ∘ f))
⊢ LinearIndependent (ι := ↑(s ∪ t)) R ((s ∪ t).restrict f)
Tactic:
apply linearIndependent.union_index hs ht.of_comp
State after:
α : 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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict (⇑(span R (f '' s)).mkQ ∘ f))
⊢ Disjoint (span R (f '' s)) (span R (f '' t))

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict (⇑(span R (f '' s)).mkQ ∘ f))
⊢ Disjoint (span R (f '' s)) (span R (f '' t))
Tactic:
convert (Submodule.range_ker_disjoint ht).symm
State after:
case h.e'_4
α : 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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict (⇑(span R (f '' s)).mkQ ∘ f))
⊢ span R (f '' s) = LinearMap.ker (span R (f '' s)).mkQ

case h.e'_5.h.e'_6
α : 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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict (⇑(span R (f '' s)).mkQ ∘ f))
⊢ f '' t = range fun x => f ↑x

State before:
case h.e'_5.h.e'_6
α : 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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict (⇑(span R (f '' s)).mkQ ∘ f))
⊢ f '' t = range fun x => f ↑x
Tactic:
aesop
State after:
no goals

State before:
case h.e'_4
α : 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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict (⇑(span R (f '' s)).mkQ ∘ f))
⊢ span R (f '' s) = LinearMap.ker (span R (f '' s)).mkQ
Tactic:
simp
State after:
no goals