Theorem: Matroid.loopEquiv_diff (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 X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv X (X \ L)
Tactic:
rw [LoopEquiv.comm]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv (X \ L) X

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv (X \ L) X
Tactic:
refine (loopEquiv_union (X \ L) hL).trans ?_
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv (X \ L ∪ L) X

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv (X \ L ∪ L) X
Tactic:
rw [diff_union_self, LoopEquiv.comm]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv X (X ∪ L)

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv X (X ∪ L)
Tactic:
exact loopEquiv_union X hL
State after:
no goals