rintro rfl
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C✝ : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
C : Set α
hC : C ⊆ M.E
⊢ C = M.E → M.Circuit C
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
hC : M.E ⊆ M.E
⊢ M.Circuit M.E