intro he
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
⊢ C ∩ K ≠ {e}
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
⊢ False