Theorem: Matroid.modular_cut_iff_modular_cut'_finite (Matroid/Old/ModularCut.lean)

State before:
α : Type u_1
C : Set (Set α)
M : Matroid α
inst✝ : M.Finite
⊢ M.Modular_cut C ↔ sorryAx Prop true
Tactic:
unfold Modular_cut Modular_cut'
State after:
α : Type u_1
C : Set (Set α)
M : Matroid α
inst✝ : M.Finite
⊢ sorryAx ({α : Type u_1} → Matroid α → Set (Set α) → Prop) true M C ↔ sorryAx Prop true