Theorem: Matroid.one_le_girth (Matroid/Circuit.lean)

State before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
⊢ 1 ≤ M.girth
Tactic:
simp_rw [girth, le_iInf_iff, one_le_encard_iff_nonempty]
State after:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
⊢ ∀ i ∈ {C | M.Circuit C}, i.Nonempty

State before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
⊢ ∀ i ∈ {C | M.Circuit C}, i.Nonempty
Tactic:
exact fun _ ↦ Circuit.nonempty
State after:
no goals