case inl
α β : Type u
b : Cardinal
hb : 1 ≤ b
⊢ 0 ≤ 0 ^ b

case inr
α β : Type u
a b : Cardinal
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b
α β : Type u
a b : Cardinal
hb : 1 ≤ b
⊢ a ≤ a ^ b
rcases eq_or_ne a 0 with (rfl | ha)
no goals
case inl
α β : Type u
b : Cardinal
hb : 1 ≤ b
⊢ 0 ≤ 0 ^ b
exact zero_le _
case h.e'_3
α β : Type u
a b : Cardinal
hb : 1 ≤ b
ha : a ≠ 0
⊢ a = a ^ 1
case inr
α β : Type u
a b : Cardinal
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b
convert power_le_power_left ha hb
no goals
case h.e'_3
α β : Type u
a b : Cardinal
hb : 1 ≤ b
ha : a ≠ 0
⊢ a = a ^ 1
exact power_one.symm