rintro rfl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
h : M.Basis I C
⊢ I ≠ C
α : Type u_1
M : Matroid α
C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit I
h : M.Basis I I
⊢ False