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

Proof state:
case neg
a b c : Ordinal.{u_1}
b0 : ¬b = 0
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
by_cases a0 : a = 0

Result:
case pos
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : a = 0
⊢ a ^ (b * c) = (a ^ b) ^ c

case neg
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
⊢ a ^ (b * c) = (a ^ b) ^ c

Proof state:
case pos
b c : Ordinal.{u_1}
b0 : ¬b = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

Tactic:
by_cases c0 : c = 0

Result:
case pos
b c : Ordinal.{u_1}
b0 : ¬b = 0
c0 : c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

case neg
b c : Ordinal.{u_1}
b0 : ¬b = 0
c0 : ¬c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

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

Tactic:
induction c using limitRecOn with
| H₁ => simp only [mul_zero, opow_zero]
| H₂ c IH =>
  rw [mul_succ, opow_add, IH, opow_succ]
| H₃ c l IH =>
  refine
    eq_of_forall_ge_iff fun d =>
      (((isNormal_opow a1).trans (isNormal_mul_right (Ordinal.pos_iff_ne_zero.2 b0))).limit_le
            l).trans
        ?_
  dsimp only [Function.comp_def]
  simp +contextual only [IH]
  exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm

Result:
no goals

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

Tactic:
refine
  eq_of_forall_ge_iff fun d =>
    (((isNormal_opow a1).trans (isNormal_mul_right (Ordinal.pos_iff_ne_zero.2 b0))).limit_le
          l).trans
      ?_

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

Proof state:
case pos
a b c : Ordinal.{u_1}
b0 : b = 0
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
simp only [b0, zero_mul, opow_zero, one_opow]

Result:
no goals

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

Tactic:
rw [mul_succ, opow_add, IH, opow_succ]

Result:
no goals

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

Tactic:
simp +contextual only [IH]

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

Proof state:
case neg.inl
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 = a
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
subst a1

Result:
case neg.inl
b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬1 = 0
⊢ 1 ^ (b * c) = (1 ^ b) ^ c

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

Tactic:
by_cases b0 : b = 0

Result:
case pos
a b c : Ordinal.{u_1}
b0 : b = 0
⊢ a ^ (b * c) = (a ^ b) ^ c

case neg
a b c : Ordinal.{u_1}
b0 : ¬b = 0
⊢ a ^ (b * c) = (a ^ b) ^ c

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

Tactic:
dsimp only [Function.comp_def]

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

Proof state:
case neg
b c : Ordinal.{u_1}
b0 : ¬b = 0
c0 : ¬c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

Tactic:
simp only [zero_opow b0, zero_opow c0, zero_opow (mul_ne_zero b0 c0)]

Result:
no goals

Proof state:
case pos
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : a = 0
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
subst a

Result:
case pos
b c : Ordinal.{u_1}
b0 : ¬b = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

Proof state:
case neg
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
⊢ a ^ (b * c) = (a ^ b) ^ c

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

Result:
case neg.inl
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 = a
⊢ a ^ (b * c) = (a ^ b) ^ c

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

Proof state:
case pos
b c : Ordinal.{u_1}
b0 : ¬b = 0
c0 : c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

Tactic:
simp only [c0, mul_zero, opow_zero]

Result:
no goals

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

Tactic:
exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm

Result:
no goals

Proof state:
case neg.inl
b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬1 = 0
⊢ 1 ^ (b * c) = (1 ^ b) ^ c

Tactic:
simp only [one_opow]

Result:
no goals

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

Tactic:
simp only [mul_zero, opow_zero]

Result:
no goals