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

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
N : Matroid α
hef : N.ConnectedTo e f
h : N ≤m M
⊢ M.ConnectedTo e f
Tactic:
obtain ⟨C, D, -, -, -, rfl⟩ := h
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
C D : Set α
hef : (M ／ C ＼ D).ConnectedTo e f
⊢ M.ConnectedTo e f

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