no goals
α : Type ?u.222044
β : Type ?u.222047
γ : Type ?u.222050
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
⊢ 0 • a = a * ↑0
rw [zero_smul, Nat.cast_zero, mul_zero]
no goals
α : Type ?u.222044
β : Type ?u.222047
γ : Type ?u.222050
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
a : Ordinal
⊢ (n + 1) • a = a * ↑(n + 1)
rw [succ_nsmul', Nat.cast_add, mul_add, Nat.cast_one, mul_one, smul_eq_mul n]