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

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
obtain (rfl | hne) := eq_or_ne e f
State after:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e e
⊢ M.ConnectedTo e e

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
⊢ M.ConnectedTo e f

State before:
case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
⊢ M.ConnectedTo e f
Tactic:
obtain ⟨C, hC, heC, hfC⟩ := hef.exists_circuit_of_ne hne
State after:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
C : Set α
hC : (M ↾ R).Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo e f

State before:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
C : Set α
hC : (M ↾ R).Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo e f
Tactic:
rw [restrict_circuit_iff] at hC
State after:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C ∧ C ⊆ R
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo e f

State before:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C ∧ C ⊆ R
heC : e ∈ C
hfC : f ∈ C
⊢ M.ConnectedTo e f
Tactic:
exact hC.1.mem_connectedTo_mem heC hfC
State after:
no goals

State before:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
R : Set α
hR : R ⊆ M.E
hef : (M ↾ R).ConnectedTo e e
⊢ M.ConnectedTo e e
Tactic:
simp [hR hef.mem_ground_left]
State after:
no goals