Theorem: Matroid.unif_sub_dual (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 (b - a) b)✶ = unif a b
Tactic:
rw [eq_comm, eq_dual_comm, unif_dual]
State after:
no goals