Theorem: Matroid.Circuit.cocircuit_inter_nontrivial (Matroid/Circuit.lean)

State before:
α : 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
hCK : (C ∩ K).Nonempty
⊢ (C ∩ K).Nontrivial
Tactic:
simpa [or_iff_not_imp_left, not_disjoint_iff_nonempty_inter, imp_iff_right hCK] using
  hC.cocircuit_disjoint_or_nontrivial_inter hK
State after:
no goals