Theorem: Matroid.flat_iff_forall_circuit' (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ M.Flat F ↔ (∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F) ∧ F ⊆ M.E
Tactic:
refine' ⟨fun h ↦ ⟨(flat_iff_forall_circuit h.subset_ground).mp h, h.subset_ground⟩, fun h ↦
  (flat_iff_forall_circuit h.2).mpr h.1⟩
State after:
no goals