Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops (Matroid/Loop.lean)

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
⊢ M = uniqueBaseOn (M✶.cl ∅) M.E
Tactic:
refine eq_of_base_iff_base_forall rfl (fun B hBE ↦ ?_)
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B ⊆ M.E
⊢ M.Base B ↔ (uniqueBaseOn (M✶.cl ∅) M.E).Base B

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B ⊆ M.E
⊢ M.Base B ↔ (uniqueBaseOn (M✶.cl ∅) M.E).Base B
Tactic:
rw [uniqueBaseOn_base_iff (show M✶.cl ∅ ⊆ M.E from M✶.cl_subset_ground _)]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B ⊆ M.E
⊢ M.Base B ↔ B = M✶.cl ∅

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B ⊆ M.E
⊢ M.Base B ↔ B = M✶.cl ∅
Tactic:
rw [hE, ← diff_subset_iff] at hBE
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
⊢ M.Base B ↔ B = M✶.cl ∅

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
⊢ M.Base B ↔ B = M✶.cl ∅
Tactic:
use fun h ↦ h.coloops_subset.antisymm' (by rwa [sdiff_eq_left.mpr h.indep.disjoint_loops] at hBE)
State after:
case mpr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
⊢ B = M✶.cl ∅ → M.Base B

State before:
case mpr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
⊢ B = M✶.cl ∅ → M.Base B
Tactic:
rintro rfl
State after:
case mpr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
⊢ M.Base (M✶.cl ∅)

State before:
case mpr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
⊢ M.Base (M✶.cl ∅)
Tactic:
obtain ⟨B, hB⟩ := M.exists_base
State after:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ M.Base (M✶.cl ∅)

State before:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ M.Base (M✶.cl ∅)
Tactic:
rwa [hB.coloops_subset.antisymm ]
State after:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ B ⊆ M✶.cl ∅

State before:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ B ⊆ M✶.cl ∅
Tactic:
refine subset_trans ?_ (diff_subset_iff.2 hE.subset)
State after:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ B ⊆ M.E \ M.cl ∅

State before:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ B ⊆ M.E \ M.cl ∅
Tactic:
rw [subset_diff, and_iff_right hB.subset_ground]
State after:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ Disjoint B (M.cl ∅)

State before:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ Disjoint B (M.cl ∅)
Tactic:
exact hB.indep.disjoint_loops
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
h : M.Base B
⊢ B ⊆ M✶.cl ∅
Tactic:
rwa [sdiff_eq_left.mpr h.indep.disjoint_loops] at hBE
State after:
no goals