exact fun C hC ↦ (show (1 : ℕ∞) < 3 from Nat.one_lt_ofNat).trans_le (h C hC)
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ ∀ (C : Set α), M.Circuit C → 1 < C.encard
no goals