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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
hC : M.Circuit C
⊢ M.girth ≤ C.encard
Tactic:
simp only [girth, mem_setOf_eq, iInf_le_iff, le_iInf_iff]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
hC : M.Circuit C
⊢ ∀ (b : ℕ∞), (∀ (i : Set α), M.Circuit i → b ≤ i.encard) → b ≤ C.encard

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
hC : M.Circuit C
⊢ ∀ (b : ℕ∞), (∀ (i : Set α), M.Circuit i → b ≤ i.encard) → b ≤ C.encard
Tactic:
exact fun b hb ↦ hb C hC
State after:
no goals