α β : Type u
a b : Cardinal
hb✝ : 1 < b
hb : 2 ≤ b
⊢ a < b ^ a
α β : Type u
a b : Cardinal
hb : 1 < b
⊢ a < b ^ a
rw [← succ_le_iff, (by norm_cast : succ (1 : Cardinal) = 2)] at hb
no goals
α β : Type u
a b : Cardinal
hb✝ : 1 < b
hb : 2 ≤ b
⊢ a < b ^ a
exact (cantor a).trans_le (power_le_power_right hb)
no goals
α β : Type u
a b : Cardinal
hb✝ : 1 < b
hb : succ 1 ≤ b
⊢ succ 1 = 2
norm_cast