case pos
a b c : Ordinal
ab : a ≤ b
a0 : a = 0
⊢ a ^ c ≤ b ^ c

case neg
a b c : Ordinal
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ c ≤ b ^ c
a b c : Ordinal
ab : a ≤ b
⊢ a ^ c ≤ b ^ c
by_cases a0 : a = 0
case pos
b c : Ordinal
ab : 0 ≤ b
⊢ 0 ^ c ≤ b ^ c
case pos
a b c : Ordinal
ab : a ≤ b
a0 : a = 0
⊢ a ^ c ≤ b ^ c
subst a
case pos
b c : Ordinal
ab : 0 ≤ b
c0 : c = 0
⊢ 0 ^ c ≤ b ^ c

case neg
b c : Ordinal
ab : 0 ≤ b
c0 : ¬c = 0
⊢ 0 ^ c ≤ b ^ c
case pos
b c : Ordinal
ab : 0 ≤ b
⊢ 0 ^ c ≤ b ^ c
by_cases c0 : c = 0
case pos
b : Ordinal
ab : 0 ≤ b
⊢ 0 ^ 0 ≤ b ^ 0
case pos
b c : Ordinal
ab : 0 ≤ b
c0 : c = 0
⊢ 0 ^ c ≤ b ^ c
subst c
no goals
case pos
b : Ordinal
ab : 0 ≤ b
⊢ 0 ^ 0 ≤ b ^ 0
simp only [opow_zero, le_refl]
no goals
case neg
b c : Ordinal
ab : 0 ≤ b
c0 : ¬c = 0
⊢ 0 ^ c ≤ b ^ c
simp only [zero_opow c0, Ordinal.zero_le]
case neg.H₁
a b c : Ordinal
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ 0 ≤ b ^ 0

case neg.H₂
a b c : Ordinal
ab : a ≤ b
a0 : ¬a = 0
⊢ ∀ (o : Ordinal), a ^ o ≤ b ^ o → a ^ succ o ≤ b ^ succ o

case neg.H₃
a b c : Ordinal
ab : a ≤ b
a0 : ¬a = 0
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → a ^ o' ≤ b ^ o') → a ^ o ≤ b ^ o
case neg
a b c : Ordinal
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ c ≤ b ^ c
apply limitRecOn c
no goals
case neg.H₁
a b c : Ordinal
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ 0 ≤ b ^ 0
simp only [opow_zero, le_refl]
case neg.H₂
a b c✝ : Ordinal
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal
IH : a ^ c ≤ b ^ c
⊢ a ^ succ c ≤ b ^ succ c
case neg.H₂
a b c : Ordinal
ab : a ≤ b
a0 : ¬a = 0
⊢ ∀ (o : Ordinal), a ^ o ≤ b ^ o → a ^ succ o ≤ b ^ succ o
intro c IH
no goals
case neg.H₂
a b c✝ : Ordinal
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal
IH : a ^ c ≤ b ^ c
⊢ a ^ succ c ≤ b ^ succ c
simpa only [opow_succ] using mul_le_mul' IH ab
no goals
case neg.H₃
a b c : Ordinal
ab : a ≤ b
a0 : ¬a = 0
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → a ^ o' ≤ b ^ o') → a ^ o ≤ b ^ o
exact fun c l IH =>
  (opow_le_of_limit a0 l).2 fun b' h =>
    (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 a0).trans_le ab) h.le)