refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
⊢ M.Circuit M.E ↔ M = circuitOn M.E
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M.Circuit M.E
⊢ M = circuitOn M.E

case refine_2
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
inst✝ : M.Nonempty
h : M = circuitOn M.E
⊢ M.Circuit M.E