Theorem: Matroid.LoopEquiv.symmDiff_subset_loops (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 α
⊢ M.LoopEquiv X Y ↔ X ∆ Y ⊆ M.cl ∅
Tactic:
rw [Set.symmDiff_def, union_subset_iff]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ M.LoopEquiv X Y ↔ X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ 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 α
⊢ M.LoopEquiv X Y ↔ X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
Tactic:
refine ⟨fun h ↦ ⟨h.diff_subset_loops, h.symm.diff_subset_loops⟩, fun ⟨h1, h2⟩ ↦ ?_⟩
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X \ Y ⊆ M.cl ∅
h2 : Y \ X ⊆ M.cl ∅
⊢ M.LoopEquiv X Y

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X \ Y ⊆ M.cl ∅
h2 : Y \ X ⊆ M.cl ∅
⊢ M.LoopEquiv X Y
Tactic:
rw [diff_subset_iff] at h1 h2
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X ⊆ Y ∪ M.cl ∅
h2 : Y ⊆ X ∪ M.cl ∅
⊢ M.LoopEquiv X Y

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X ⊆ Y ∪ M.cl ∅
h2 : Y ⊆ X ∪ M.cl ∅
⊢ M.LoopEquiv X Y
Tactic:
rw [loopEquiv_iff_union_eq_union, subset_antisymm_iff, union_subset_iff, union_subset_iff]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X ⊆ Y ∪ M.cl ∅
h2 : Y ⊆ X ∪ M.cl ∅
⊢ (X ⊆ Y ∪ M.cl ∅ ∧ M.cl ∅ ⊆ Y ∪ M.cl ∅) ∧ Y ⊆ X ∪ M.cl ∅ ∧ M.cl ∅ ⊆ X ∪ 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 α
x✝ : X \ Y ⊆ M.cl ∅ ∧ Y \ X ⊆ M.cl ∅
h1 : X ⊆ Y ∪ M.cl ∅
h2 : Y ⊆ X ∪ M.cl ∅
⊢ (X ⊆ Y ∪ M.cl ∅ ∧ M.cl ∅ ⊆ Y ∪ M.cl ∅) ∧ Y ⊆ X ∪ M.cl ∅ ∧ M.cl ∅ ⊆ X ∪ M.cl ∅
Tactic:
exact ⟨⟨h1, subset_union_right⟩, h2, subset_union_right⟩
State after:
no goals