rw [← M.cl_union_cl_left_eq, ← M.cl_union_cl_right_eq]
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ X ∪ Y ⊆ M.cl (IX ∪ IY)
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ X ∪ Y ⊆ M.cl (M.cl IX ∪ M.cl IY)