case pos
a b c : Ordinal
b0 : b = 0
⊢ a ^ (b * c) = (a ^ b) ^ c

case neg
a b c : Ordinal
b0 : ¬b = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
a b c : Ordinal
⊢ a ^ (b * c) = (a ^ b) ^ c
by_cases b0 : b = 0
case pos
a b c : Ordinal
b0 : ¬b = 0
a0 : a = 0
⊢ a ^ (b * c) = (a ^ b) ^ c

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

case neg.inr
a b c : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * c) = (a ^ b) ^ c
case neg
a b c : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
cases' eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with a1 a1
case neg.inr.H₁
a b c : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * 0) = (a ^ b) ^ 0

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

case neg.inr.H₃
a b c : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → a ^ (b * o') = (a ^ b) ^ o') → a ^ (b * o) = (a ^ b) ^ o
case neg.inr
a b c : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * c) = (a ^ b) ^ c
apply limitRecOn c
no goals
case pos
a b c : Ordinal
b0 : b = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
simp only [b0, zero_mul, opow_zero, one_opow]
case pos
b c : Ordinal
b0 : ¬b = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
case pos
a b c : Ordinal
b0 : ¬b = 0
a0 : a = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
subst a
case pos
b c : Ordinal
b0 : ¬b = 0
c0 : c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

case neg
b c : Ordinal
b0 : ¬b = 0
c0 : ¬c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
case pos
b c : Ordinal
b0 : ¬b = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
by_cases c0 : c = 0
no goals
case neg
b c : Ordinal
b0 : ¬b = 0
c0 : ¬c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
simp only [zero_opow b0, zero_opow c0, zero_opow (mul_ne_zero b0 c0)]
no goals
case pos
b c : Ordinal
b0 : ¬b = 0
c0 : c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
simp only [c0, mul_zero, opow_zero]
case neg.inl
b c : Ordinal
b0 : ¬b = 0
a0 : ¬1 = 0
⊢ 1 ^ (b * c) = (1 ^ b) ^ c
case neg.inl
a b c : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 = a
⊢ a ^ (b * c) = (a ^ b) ^ c
subst a1
no goals
case neg.inl
b c : Ordinal
b0 : ¬b = 0
a0 : ¬1 = 0
⊢ 1 ^ (b * c) = (1 ^ b) ^ c
simp only [one_opow]
no goals
case neg.inr.H₁
a b c : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * 0) = (a ^ b) ^ 0
simp only [mul_zero, opow_zero]
case neg.inr.H₂
a b c✝ : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal
IH : a ^ (b * c) = (a ^ b) ^ c
⊢ a ^ (b * succ c) = (a ^ b) ^ succ c
case neg.inr.H₂
a b c : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ ∀ (o : Ordinal), a ^ (b * o) = (a ^ b) ^ o → a ^ (b * succ o) = (a ^ b) ^ succ o
intro c IH
no goals
case neg.inr.H₂
a b c✝ : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal
IH : a ^ (b * c) = (a ^ b) ^ c
⊢ a ^ (b * succ c) = (a ^ b) ^ succ c
rw [mul_succ, opow_add, IH, opow_succ]
case neg.inr.H₃
a b c✝ : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b * o') = (a ^ b) ^ o'
⊢ a ^ (b * c) = (a ^ b) ^ c
case neg.inr.H₃
a b c : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → a ^ (b * o') = (a ^ b) ^ o') → a ^ (b * o) = (a ^ b) ^ o
intro c l IH
case neg.inr.H₃
a b c✝ : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b * o') = (a ^ b) ^ 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) ^ c ≤ d
case neg.inr.H₃
a b c✝ : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b * o') = (a ^ b) ^ o'
⊢ a ^ (b * c) = (a ^ b) ^ c
refine'
  eq_of_forall_ge_iff fun d =>
    (((opow_isNormal a1).trans (mul_isNormal (Ordinal.pos_iff_ne_zero.2 b0))).limit_le
          l).trans
      _
case neg.inr.H₃
a b c✝ : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal
⊢ (∀ (b_1 : Ordinal), b_1 < c → a ^ (b * b_1) ≤ d) ↔ (a ^ b) ^ c ≤ d
case neg.inr.H₃
a b c✝ : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b * o') = (a ^ b) ^ 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) ^ c ≤ d
dsimp only [Function.comp]
case neg.inr.H₃
a b c✝ : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal
⊢ (∀ (b_1 : Ordinal), b_1 < c → (a ^ b) ^ b_1 ≤ d) ↔ (a ^ b) ^ c ≤ d
case neg.inr.H₃
a b c✝ : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal
⊢ (∀ (b_1 : Ordinal), b_1 < c → a ^ (b * b_1) ≤ d) ↔ (a ^ b) ^ c ≤ d
simp (config := { contextual := true }) only [IH]
no goals
case neg.inr.H₃
a b c✝ : Ordinal
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal
l : IsLimit c
IH : ∀ (o' : Ordinal), o' < c → a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal
⊢ (∀ (b_1 : Ordinal), b_1 < c → (a ^ b) ^ b_1 ≤ d) ↔ (a ^ b) ^ c ≤ d
exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm