Theorem: Matroid.indep_of_card_lt_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 : ℕ∞
hI : I.encard < M.girth
hIE : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I
Tactic:
rw [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 : ℕ∞
hI : I.encard < M.girth
hIE : autoParam (I ⊆ M.E) _auto✝
⊢ ∀ C ⊆ I, ¬M.Circuit C

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
hI : I.encard < M.girth
hIE : autoParam (I ⊆ M.E) _auto✝
⊢ ∀ C ⊆ I, ¬M.Circuit C
Tactic:
exact fun C hCI hC ↦ ((hC.girth_le_card.trans (encard_mono hCI)).trans_lt hI).ne rfl
State after:
no goals