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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
inst✝ : M.Finitary
⊢ M.girth = ⊤ ↔ M.Indep M.E
Tactic:
rw [girth_eq_top_iff, indep_iff_forall_subset_not_circuit]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
inst✝ : M.Finitary
⊢ (∀ (C : Set α), M.Circuit C → C.Infinite) ↔ ∀ C ⊆ M.E, ¬M.Circuit C

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
inst✝ : M.Finitary
⊢ (∀ (C : Set α), M.Circuit C → C.Infinite) ↔ ∀ C ⊆ M.E, ¬M.Circuit C
Tactic:
exact ⟨fun h C _ hC ↦ h C hC hC.finite, fun h C hC _ ↦ h C hC.subset_ground hC⟩
State after:
no goals