case pos
α β : Type u
a b c : Cardinal
h : b ≤ c
ha : a = 0
⊢ a ^ b ≤ max (a ^ c) 1

case neg
α β : Type u
a b c : Cardinal
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1
α β : Type u
a b c : Cardinal
h : b ≤ c
⊢ a ^ b ≤ max (a ^ c) 1
by_cases ha : a = 0
no goals
case pos
α β : Type u
a b c : Cardinal
h : b ≤ c
ha : a = 0
⊢ a ^ b ≤ max (a ^ c) 1
simp [ha, zero_power_le]
no goals
case neg
α β : Type u
a b c : Cardinal
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1
exact (power_le_power_left ha h).trans (le_max_left _ _)