case refine'_3
ι : Type u'
ι' : Type ?u.638952
R : Type u_3
K : Type ?u.638958
M : Type u_1
M' : Type u_2
M'' : Type ?u.638967
V : Type u
V' : Type ?u.638972
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 : Set M
t : Set M'
hs : LinearIndependent R fun x => ↑x
ht : LinearIndependent R fun x => ↑x
⊢ Disjoint (span R (↑(inl R M M') '' s)) (span R (↑(inr R M M') '' t))
ι : Type u'
ι' : Type ?u.638952
R : Type u_3
K : Type ?u.638958
M : Type u_1
M' : Type u_2
M'' : Type ?u.638967
V : Type u
V' : Type ?u.638972
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 : Set M
t : Set M'
hs : LinearIndependent R fun x => ↑x
ht : LinearIndependent R fun x => ↑x
⊢ LinearIndependent R fun x => ↑x
refine' (hs.image_subtype _).union (ht.image_subtype _) _ <;> [simp; simp; skip]
case refine'_3
ι : Type u'
ι' : Type ?u.638952
R : Type u_3
K : Type ?u.638958
M : Type u_1
M' : Type u_2
M'' : Type ?u.638967
V : Type u
V' : Type ?u.638972
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 : Set M
t : Set M'
hs : LinearIndependent R fun x => ↑x
ht : LinearIndependent R fun x => ↑x
⊢ Disjoint (Submodule.map (inl R M M') (span R s)) (Submodule.map (inr R M M') (span R t))
case refine'_3
ι : Type u'
ι' : Type ?u.638952
R : Type u_3
K : Type ?u.638958
M : Type u_1
M' : Type u_2
M'' : Type ?u.638967
V : Type u
V' : Type ?u.638972
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 : Set M
t : Set M'
hs : LinearIndependent R fun x => ↑x
ht : LinearIndependent R fun x => ↑x
⊢ Disjoint (span R (↑(inl R M M') '' s)) (span R (↑(inr R M M') '' t))
simp only [span_image]
no goals
case refine'_3
ι : Type u'
ι' : Type ?u.638952
R : Type u_3
K : Type ?u.638958
M : Type u_1
M' : Type u_2
M'' : Type ?u.638967
V : Type u
V' : Type ?u.638972
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 : Set M
t : Set M'
hs : LinearIndependent R fun x => ↑x
ht : LinearIndependent R fun x => ↑x
⊢ Disjoint (Submodule.map (inl R M M') (span R s)) (Submodule.map (inr R M M') (span R t))
simp [disjoint_iff, prod_inf_prod]