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

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ (unif a b).erk = ↑(min a b)
Tactic:
rw [erk_eq_er_ground, unif_er_eq]
State after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ min (unif a b).E.encard ↑a = ↑(min a b)

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ min (unif a b).E.encard ↑a = ↑(min a b)
Tactic:
simp only [unif_ground_eq, ge_iff_le, min_comm, encard_univ_fin]
State after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ min ↑a ↑b = ↑(min a b)

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ min ↑a ↑b = ↑(min a b)
Tactic:
rfl
State after:
no goals