Theorem: Matroid.Indep.eq_union_image_of_disjointSum (Matroid/Constructions/DirectSum.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : (M.disjointSum N h).Indep I
⊢ ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN
Tactic:
rw [disjointSum_indep_iff] at hI
State after:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN
Tactic:
refine ⟨I ∩ M.E, I ∩ N.E, hI.1, hI.2.1, h.mono inf_le_right inf_le_right, ?_⟩
State after:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ M.E ∪ I ∩ N.E

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ M.E ∪ I ∩ N.E
Tactic:
rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hI.2.2]
State after:
no goals