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

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.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 : α
h : M.ConnectedTo e e
⊢ M✶.ConnectedTo e e

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
⊢ M✶.ConnectedTo e f

State before:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e g : α
h : M.ConnectedTo e e
⊢ M✶.ConnectedTo e e

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
⊢ M✶.ConnectedTo e f
Tactic:
exact connectedTo_self h.mem_ground_left
State after:
case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
h : M.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 : α
h : M.ConnectedTo e f
hne : e ≠ f
⊢ M✶.ConnectedTo e f
Tactic:
obtain ⟨C, hC, heC, hfC⟩ := h.exists_circuit_of_ne hne
State after:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.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 : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ M✶.ConnectedTo e f
Tactic:
have hpara : (M ／ (C \ {e,f})).Parallel e f := by
  rw [parallel_iff_circuit hne]
  apply hC.contract_diff_circuit (by simp) (by simp [pair_subset_iff, heC, hfC])
State after:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
⊢ M✶.ConnectedTo e f

State before:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
⊢ M✶.ConnectedTo e f
Tactic:
obtain ⟨B, hB, heB⟩ := hpara.nonloop_left.exists_mem_base
State after:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
⊢ M✶.ConnectedTo e f

State before:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
⊢ M✶.ConnectedTo e f
Tactic:
have hK := fundCocct_cocircuit heB hB
State after:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
hK : (M ／ (C \ {e, f})).Cocircuit (fundCocct e B)
⊢ M✶.ConnectedTo e f

State before:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
hK : (M ／ (C \ {e, f})).Cocircuit (fundCocct e B)
⊢ M✶.ConnectedTo e f
Tactic:
refine Circuit.mem_connectedTo_mem hK.of_contract.circuit (mem_fundCocct _ _ _) ?_
State after:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
hK : (M ／ (C \ {e, f})).Cocircuit (fundCocct e B)
⊢ f ∈ fundCocct e B

State before:
case inr.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
hpara : (M ／ (C \ {e, f})).Parallel e f
B : Set α
hB : (M ／ (C \ {e, f})).Base B
heB : e ∈ B
hK : (M ／ (C \ {e, f})).Cocircuit (fundCocct e B)
⊢ f ∈ fundCocct e B
Tactic:
exact hpara.mem_cocircuit_of_mem hK (mem_fundCocct _ _ _)
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ (M ／ (C \ {e, f})).Parallel e f
Tactic:
rw [parallel_iff_circuit hne]
State after:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ (M ／ (C \ {e, f})).Circuit {e, f}

State before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ (M ／ (C \ {e, f})).Circuit {e, f}
Tactic:
apply hC.contract_diff_circuit (by simp) (by simp [pair_subset_iff, heC, hfC])
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ {e, f}.Nonempty
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C✝ K : Set α
e f g : α
h : M.ConnectedTo e f
hne : e ≠ f
C : Set α
hC : M.Circuit C
heC : e ∈ C
hfC : f ∈ C
⊢ {e, f} ⊆ C
Tactic:
simp [pair_subset_iff, heC, hfC]
State after:
no goals