no goals
ι : Type u'
ι' : Type ?u.376032
R : Type u_2
K : Type ?u.376038
M : Type u_1
M' : Type ?u.376044
M'' : Type ?u.376047
V : Type u
V' : Type ?u.376052
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s t : Set M
hs : LinearIndependent R fun x => ↑x
ht : LinearIndependent R fun x => ↑x
hst : Disjoint (span R s) (span R t)
⊢ Disjoint (span R (range fun x => ↑x)) (span R (range fun x => ↑x))
simpa
no goals
ι : Type u'
ι' : Type ?u.376032
R : Type u_2
K : Type ?u.376038
M : Type u_1
M' : Type ?u.376044
M'' : Type ?u.376047
V : Type u
V' : Type ?u.376052
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s t : Set M
hs : LinearIndependent R fun x => ↑x
ht : LinearIndependent R fun x => ↑x
hst : Disjoint (span R s) (span R t)
⊢ range (Sum.elim (fun x => ↑x) fun x => ↑x) = s ∪ t
simp