Theorem: Matroid.unifOn_eq_unifOn_min (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ unifOn E k = unifOn E (min k E.encard)
Tactic:
simp only [ge_iff_le, eq_iff_indep_iff_indep_forall, unifOn_ground_eq, unifOn_indep_iff,
  le_min_iff, and_congr_left_iff, iff_self_and, true_and]
State after:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∀ I ⊆ E, I ⊆ E → I.encard ≤ k → I.encard ≤ E.encard

State before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∀ I ⊆ E, I ⊆ E → I.encard ≤ k → I.encard ≤ E.encard
Tactic:
exact fun I hI _ _ ↦ encard_mono hI
State after:
no goals