rw [image_union]
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 ι✝
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 f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ LinearIndependent R fun (x : ↑(f '' (s ∪ t))) => ↑x
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 ι✝
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 f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ LinearIndependent R fun (x : ↑(f '' s ∪ f '' t)) => ↑x