case inl
b c : Ordinal
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

case inr
a b c : Ordinal
a0 : a ≠ 0
⊢ a ^ (b + c) = a ^ b * a ^ c
a b c : Ordinal
⊢ a ^ (b + c) = a ^ b * a ^ c
rcases eq_or_ne a 0 with (rfl | a0)
case inr.inl
b c : Ordinal
a0 : 1 ≠ 0
⊢ 1 ^ (b + c) = 1 ^ b * 1 ^ c

case inr.inr
a b c : Ordinal
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
case inr
a b c : Ordinal
a0 : a ≠ 0
⊢ a ^ (b + c) = a ^ b * a ^ c
rcases eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with (rfl | a1)
case inr.inr.H₁
a b c : Ordinal
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + 0) = a ^ b * a ^ 0

case inr.inr.H₂
a b c : Ordinal
a0 : a ≠ 0
a1 : 1 < a
⊢ ∀ (o : Ordinal), a ^ (b + o) = a ^ b * a ^ o → a ^ (b + succ o) = a ^ b * a ^ succ o

case inr.inr.H₃
a b c : Ordinal
a0 : a ≠ 0
a1 : 1 < a
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → a ^ (b + o') = a ^ b * a ^ o') → a ^ (b + o) = a ^ b * a ^ o
case inr.inr
a b c : Ordinal
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
apply limitRecOn c
case inl.inl
b : Ordinal
⊢ 0 ^ (b + 0) = 0 ^ b * 0 ^ 0

case inl.inr
b c : Ordinal
c0 : c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
case inl
b c : Ordinal
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
rcases eq_or_ne c 0 with (rfl | c0)
case inl.inr
b c : Ordinal
c0 : c ≠ 0
this : b + c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
case inl.inr
b c : Ordinal
c0 : c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
have : b + c ≠ 0 := ((Ordinal.pos_iff_ne_zero.2 c0).trans_le (le_add_left _ _)).ne'
no goals
case inl.inr
b c : Ordinal
c0 : c ≠ 0
this : b + c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
simp only [zero_opow c0, zero_opow this, mul_zero]
no goals
case inl.inl
b : Ordinal
⊢ 0 ^ (b + 0) = 0 ^ b * 0 ^ 0
simp
no goals
case inr.inl
b c : Ordinal
a0 : 1 ≠ 0
⊢ 1 ^ (b + c) = 1 ^ b * 1 ^ c
simp only [one_opow, mul_one]
no goals
case inr.inr.H₁
a b c : Ordinal
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + 0) = a ^ b * a ^ 0
simp
case inr.inr.H₂
a b c✝ : Ordinal
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ (b + succ c) = a ^ b * a ^ succ c
case inr.inr.H₂
a b c : Ordinal
a0 : a ≠ 0
a1 : 1 < a
⊢ ∀ (o : Ordinal), a ^ (b + o) = a ^ b * a ^ o → a ^ (b + succ o) = a ^ b * a ^ succ o
intro c IH
no goals
case inr.inr.H₂
a b c✝ : Ordinal
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ (b + succ c) = a ^ b * a ^ succ c
rw [add_succ, opow_succ, IH, opow_succ, mul_assoc]
case inr.inr.H₃
a b c✝ : Ordinal
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b + o') = a ^ b * a ^ o'
⊢ a ^ (b + c) = a ^ b * a ^ c
case inr.inr.H₃
a b c : Ordinal
a0 : a ≠ 0
a1 : 1 < a
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → a ^ (b + o') = a ^ b * a ^ o') → a ^ (b + o) = a ^ b * a ^ o
intro c l IH
case inr.inr.H₃
a b c✝ : Ordinal
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal
⊢ (∀ (b_1 : Ordinal), b_1 < c → ((fun x x_1 => x ^ x_1) a ∘ (fun x x_1 => x + x_1) b) b_1 ≤ d) ↔ a ^ b * a ^ c ≤ d
case inr.inr.H₃
a b c✝ : Ordinal
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b + o') = a ^ b * a ^ o'
⊢ a ^ (b + c) = a ^ b * a ^ c
refine'
  eq_of_forall_ge_iff fun d =>
    (((opow_isNormal a1).trans (add_isNormal b)).limit_le l).trans _
case inr.inr.H₃
a b c✝ : Ordinal
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal
⊢ (∀ (b_1 : Ordinal), b_1 < c → a ^ (b + b_1) ≤ d) ↔ a ^ b * a ^ c ≤ d
case inr.inr.H₃
a b c✝ : Ordinal
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal
⊢ (∀ (b_1 : Ordinal), b_1 < c → ((fun x x_1 => x ^ x_1) a ∘ (fun x x_1 => x + x_1) b) b_1 ≤ d) ↔ a ^ b * a ^ c ≤ d
dsimp only [Function.comp]
case inr.inr.H₃
a b c✝ : Ordinal
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal
⊢ (∀ (b_1 : Ordinal), b_1 < c → a ^ b * a ^ b_1 ≤ d) ↔ a ^ b * a ^ c ≤ d
case inr.inr.H₃
a b c✝ : Ordinal
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal
⊢ (∀ (b_1 : Ordinal), b_1 < c → a ^ (b + b_1) ≤ d) ↔ a ^ b * a ^ c ≤ d
simp (config := { contextual := true }) only [IH]
no goals
case inr.inr.H₃
a b c✝ : Ordinal
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal
⊢ (∀ (b_1 : Ordinal), b_1 < c → a ^ b * a ^ b_1 ≤ d) ↔ a ^ b * a ^ c ≤ d
exact
  (((mul_isNormal <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans
          (opow_isNormal a1)).limit_le
      l).symm