swap
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}))
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}))