-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_add (a b c : Ordinal) : a ^ (b + c) = a ^ b * a ^ c

Proof state:
case inr.inr.H₂
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ (b + succ c) = a ^ b * a ^ succ c

Tactic:
rw [add_succ, opow_succ, IH, opow_succ, mul_assoc]

Result:
no goals

Proof state:
a b c : Ordinal.{u_1}
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
rcases eq_or_ne a 0 with (rfl | a0)

Result:
case inl
b c : Ordinal.{u_1}
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

case inr
a b c : Ordinal.{u_1}
a0 : a ≠ 0
⊢ a ^ (b + c) = a ^ b * a ^ c

Proof state:
case inl.inr
b c : Ordinal.{u_1}
c0 : c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

Tactic:
have : b + c ≠ 0 := ((Ordinal.pos_iff_ne_zero.2 c0).trans_le (le_add_left _ _)).ne'

Result:
case inl.inr
b c : Ordinal.{u_1}
c0 : c ≠ 0
this : b + c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

Proof state:
case inr.inr.H₁
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + 0) = a ^ b * a ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : c.IsLimit
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ b_1 < c, a ^ (b + b_1) ≤ d) ↔ a ^ b * a ^ c ≤ d

Tactic:
simp +contextual only [IH]

Result:
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : c.IsLimit
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ b_1 < c, a ^ b * a ^ b_1 ≤ d) ↔ a ^ b * a ^ c ≤ d

Proof state:
case inr.inl
b c : Ordinal.{u_1}
a0 : 1 ≠ 0
⊢ 1 ^ (b + c) = 1 ^ b * 1 ^ c

Tactic:
simp only [one_opow, mul_one]

Result:
no goals

Proof state:
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : c.IsLimit
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ b_1 < c, ((fun x => a ^ x) ∘ fun x => b + x) b_1 ≤ d) ↔ a ^ b * a ^ c ≤ d

Tactic:
dsimp only [Function.comp_def]

Result:
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : c.IsLimit
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ b_1 < c, a ^ (b + b_1) ≤ d) ↔ a ^ b * a ^ c ≤ d

Proof state:
case inr
a b c : Ordinal.{u_1}
a0 : a ≠ 0
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
rcases eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with (rfl | a1)

Result:
case inr.inl
b c : Ordinal.{u_1}
a0 : 1 ≠ 0
⊢ 1 ^ (b + c) = 1 ^ b * 1 ^ c

case inr.inr
a b c : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c

Proof state:
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : c.IsLimit
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
refine
  eq_of_forall_ge_iff fun d =>
    (((isNormal_opow a1).trans (isNormal_add_right b)).limit_le l).trans ?_

Result:
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : c.IsLimit
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ b_1 < c, ((fun x => a ^ x) ∘ fun x => b + x) b_1 ≤ d) ↔ a ^ b * a ^ c ≤ d

Proof state:
case inl.inr
b c : Ordinal.{u_1}
c0 : c ≠ 0
this : b + c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

Tactic:
simp only [zero_opow c0, zero_opow this, mul_zero]

Result:
no goals

Proof state:
case inl
b c : Ordinal.{u_1}
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

Tactic:
rcases eq_or_ne c 0 with (rfl | c0)

Result:
case inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ (b + 0) = 0 ^ b * 0 ^ 0

case inl.inr
b c : Ordinal.{u_1}
c0 : c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

Proof state:
case inr.inr
a b c : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
induction c using limitRecOn with
| H₁ => simp
| H₂ c IH =>
  rw [add_succ, opow_succ, IH, opow_succ, mul_assoc]
| H₃ c l IH =>
  refine
    eq_of_forall_ge_iff fun d =>
      (((isNormal_opow a1).trans (isNormal_add_right b)).limit_le l).trans ?_
  dsimp only [Function.comp_def]
  simp +contextual only [IH]
  exact
    (((isNormal_mul_right <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans
            (isNormal_opow a1)).limit_le
        l).symm

Result:
no goals

Proof state:
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : c.IsLimit
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ b_1 < c, a ^ b * a ^ b_1 ≤ d) ↔ a ^ b * a ^ c ≤ d

Tactic:
exact
  (((isNormal_mul_right <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans
          (isNormal_opow a1)).limit_le
      l).symm

Result:
no goals

Proof state:
case inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ (b + 0) = 0 ^ b * 0 ^ 0

Tactic:
simp

Result:
no goals