Theorem: Matroid.parallelExtend_circuit_iff (Matroid/Constructions/ParallelExtension.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
have hef : e ≠ f := by rintro rfl; exact hf he.mem_ground
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
have aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C') := by
  intro C' hfC'
  suffices h' : ((M.parallelExtend e f) ＼ f).Circuit C' ↔ M.Circuit C' by
    simpa [deleteElem, delete_circuit_iff, hfC'] using h'
  rw [parallelExtend_delete_eq _ hf]
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
by_cases hfC : f ∈ C
State after:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

State before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
swap
State after:
case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

State before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
simp only [show ¬M.Circuit C from fun h ↦ hf <| h.subset_ground hfC, hfC, true_and, false_or]
State after:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

State before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
by_cases heC : e ∈ C
State after:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

State before:
case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
rw [← (M.parallelExtend_parallel he f).parallel'.eq_mapEquiv_swap, mapEquiv_circuit_iff,
  Equiv.symm_swap, Equiv.swap_comm, Equiv.swap_image_eq_exchange hfC heC, aux (by simp [hef.symm])]
State after:
case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ M.Circuit (insert e (C \ {f})) ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))

State before:
case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ M.Circuit (insert e (C \ {f})) ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
simp [heC, show C ≠ {e,f} by rintro rfl; simp at heC]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
⊢ e ≠ f
Tactic:
rintro rfl
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
hf : e ∉ M.E
⊢ False

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e x : α
I C : Set α
he : M.Nonloop e
hf : e ∉ M.E
⊢ False
Tactic:
exact hf he.mem_ground
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
⊢ ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
Tactic:
intro C' hfC'
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
C' : Set α
hfC' : f ∉ C'
⊢ (M.parallelExtend e f).Circuit C' ↔ M.Circuit C'

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
C' : Set α
hfC' : f ∉ C'
⊢ (M.parallelExtend e f).Circuit C' ↔ M.Circuit C'
Tactic:
suffices h' : ((M.parallelExtend e f) ＼ f).Circuit C' ↔ M.Circuit C' by
  simpa [deleteElem, delete_circuit_iff, hfC'] using h'
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
C' : Set α
hfC' : f ∉ C'
⊢ (M.parallelExtend e f ＼ f).Circuit C' ↔ M.Circuit C'

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
C' : Set α
hfC' : f ∉ C'
⊢ (M.parallelExtend e f ＼ f).Circuit C' ↔ M.Circuit C'
Tactic:
rw [parallelExtend_delete_eq _ hf]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
C' : Set α
hfC' : f ∉ C'
h' : (M.parallelExtend e f ＼ f).Circuit C' ↔ M.Circuit C'
⊢ (M.parallelExtend e f).Circuit C' ↔ M.Circuit C'
Tactic:
simpa [deleteElem, delete_circuit_iff, hfC'] using h'
State after:
no goals

State before:
case neg
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ C
⊢ (M.parallelExtend e f).Circuit C ↔ M.Circuit C ∨ C = {e, f} ∨ f ∈ C ∧ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
simp [aux hfC, hfC, show C ≠ {e,f} by rintro rfl; simp at hfC]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ C
⊢ C ≠ {e, f}
Tactic:
rintro rfl
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ {e, f}
⊢ False

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∉ {e, f}
⊢ False
Tactic:
simp at hfC
State after:
no goals

State before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
suffices (M.parallelExtend e f).Circuit C ↔ C = {e, f} by simpa [heC]
State after:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f}

State before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f}
Tactic:
have hC := (M.parallelExtend_parallel he f).circuit_of_ne hef
State after:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
hC : (M.parallelExtend e f).Circuit {e, f}
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f}

State before:
case pos
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
hC : (M.parallelExtend e f).Circuit {e, f}
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f}
Tactic:
exact ⟨fun h ↦ Eq.symm <| hC.eq_of_subset_circuit h (by simp [pair_subset_iff, heC, hfC]),
  by rintro rfl; assumption⟩
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
this : (M.parallelExtend e f).Circuit C ↔ C = {e, f}
⊢ (M.parallelExtend e f).Circuit C ↔ C = {e, f} ∨ e ∉ C ∧ M.Circuit (insert e (C \ {f}))
Tactic:
simpa [heC]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
hC : (M.parallelExtend e f).Circuit {e, f}
h : (M.parallelExtend e f).Circuit C
⊢ {e, f} ⊆ C
Tactic:
simp [pair_subset_iff, heC, hfC]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∈ C
hC : (M.parallelExtend e f).Circuit {e, f}
⊢ C = {e, f} → (M.parallelExtend e f).Circuit C
Tactic:
rintro rfl
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hC : (M.parallelExtend e f).Circuit {e, f}
hfC : f ∈ {e, f}
heC : e ∈ {e, f}
⊢ (M.parallelExtend e f).Circuit {e, f}

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hC : (M.parallelExtend e f).Circuit {e, f}
hfC : f ∈ {e, f}
heC : e ∈ {e, f}
⊢ (M.parallelExtend e f).Circuit {e, f}
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ f ∉ insert e (C \ {f})
Tactic:
simp [hef.symm]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ C
heC : e ∉ C
⊢ C ≠ {e, f}
Tactic:
rintro rfl
State after:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ {e, f}
heC : e ∉ {e, f}
⊢ False

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I : Set α
he : M.Nonloop e
hf : f ∉ M.E
hef : e ≠ f
aux : ∀ ⦃C' : Set α⦄, f ∉ C' → ((M.parallelExtend e f).Circuit C' ↔ M.Circuit C')
hfC : f ∈ {e, f}
heC : e ∉ {e, f}
⊢ False
Tactic:
simp at heC
State after:
no goals