case pos
α β : Type u
c : Cardinal
h : c = 0
⊢ 0 ^ c ≤ 1

case neg
α β : Type u
c : Cardinal
h : ¬c = 0
⊢ 0 ^ c ≤ 1
α β : Type u
c : Cardinal
⊢ 0 ^ c ≤ 1
by_cases h : c = 0
no goals
case pos
α β : Type u
c : Cardinal
h : c = 0
⊢ 0 ^ c ≤ 1
rw [h, power_zero]
case neg
α β : Type u
c : Cardinal
h : ¬c = 0
⊢ 0 ≤ 1
case neg
α β : Type u
c : Cardinal
h : ¬c = 0
⊢ 0 ^ c ≤ 1
rw [zero_power h]
no goals
case neg
α β : Type u
c : Cardinal
h : ¬c = 0
⊢ 0 ≤ 1
apply zero_le