simp_rw [or_iff_not_imp_left, not_disjoint_iff]
α : 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
⊢ Disjoint C K ∨ (C ∩ K).Nontrivial
α : 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
⊢ (∃ x ∈ C, x ∈ K) → (C ∩ K).Nontrivial