Theorem: Matroid.unif_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 a b)✶ = unif (b - a) b
Tactic:
obtain (hab | hba) := le_or_lt a b
State after:
case inl
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
hab : a ≤ b
⊢ (unif a b)✶ = unif (b - a) b

case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
hba : b < a
⊢ (unif a b)✶ = unif (b - a) b

State before:
case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
hba : b < a
⊢ (unif a b)✶ = unif (b - a) b
Tactic:
simp [unif_eq_freeOn hba.le, Nat.sub_eq_zero_of_le hba.le]
State after:
no goals

State before:
case inl
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
hab : a ≤ b
⊢ (unif a b)✶ = unif (b - a) b
Tactic:
exact unif_dual' (Nat.add_sub_of_le hab)
State after:
no goals