Theorem: Matroid.ConnectedTo.of_contract (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M ／ C).ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
replace hef := hef.to_dual
State after:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M ／ C)✶.ConnectedTo e f
⊢ M.ConnectedTo e f

State before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M ／ C)✶.ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
rw [contract_dual_eq_dual_delete] at hef
State after:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M✶ ＼ C).ConnectedTo e f
⊢ M.ConnectedTo e f

State before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C : Set α
hef : (M✶ ＼ C).ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
exact hef.of_delete.of_dual
State after:
no goals