[GOAL]
a : Ordinal.{u_1}
⊢ 0 ^ a = 1 - a
[PROOFSTEP]
simp only [opow_def, if_true]
[GOAL]
a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ 0 ^ a = 0
[PROOFSTEP]
rwa [zero_opow', Ordinal.sub_eq_zero_iff_le, one_le_iff_ne_zero]
[GOAL]
a : Ordinal.{u_1}
⊢ a ^ 0 = 1
[PROOFSTEP]
by_cases h : a = 0
[GOAL]
case pos
a : Ordinal.{u_1}
h : a = 0
⊢ a ^ 0 = 1
[PROOFSTEP]
simp only [opow_def, if_pos h, sub_zero]
[GOAL]
case neg
a : Ordinal.{u_1}
h : ¬a = 0
⊢ a ^ 0 = 1
[PROOFSTEP]
simp only [opow_def, if_neg h, limitRecOn_zero]
[GOAL]
a b : Ordinal.{u_1}
h : a = 0
⊢ a ^ succ b = a ^ b * a
[PROOFSTEP]
subst a
[GOAL]
b : Ordinal.{u_1}
⊢ 0 ^ succ b = 0 ^ b * 0
[PROOFSTEP]
simp only [zero_opow (succ_ne_zero _), mul_zero]
[GOAL]
a b : Ordinal.{u_1}
h : ¬a = 0
⊢ a ^ succ b = a ^ b * a
[PROOFSTEP]
simp only [opow_def, limitRecOn_succ, if_neg h]
[GOAL]
a b : Ordinal.{u}
a0 : a ≠ 0
h : IsLimit b
⊢ a ^ b = bsup b fun c x => a ^ c
[PROOFSTEP]
simp only [opow_def, if_neg a0]
[GOAL]
a b : Ordinal.{u}
a0 : a ≠ 0
h : IsLimit b
⊢ (limitRecOn b 1 (fun x IH => IH * a) fun b x => bsup b) =
    bsup b fun c x => limitRecOn c 1 (fun x IH => IH * a) fun b x => bsup b
[PROOFSTEP]
rw [limitRecOn_limit _ _ _ _ h]
[GOAL]
a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsLimit b
⊢ a ^ b ≤ c ↔ ∀ (b' : Ordinal.{u_1}), b' < b → a ^ b' ≤ c
[PROOFSTEP]
rw [opow_limit a0 h, bsup_le_iff]
[GOAL]
a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : IsLimit c
⊢ a < b ^ c ↔ ∃ c', c' < c ∧ a < b ^ c'
[PROOFSTEP]
rw [← not_iff_not, not_exists]
[GOAL]
a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : IsLimit c
⊢ ¬a < b ^ c ↔ ∀ (x : Ordinal.{u_1}), ¬(x < c ∧ a < b ^ x)
[PROOFSTEP]
simp only [not_lt, opow_le_of_limit b0 h, exists_prop, not_and]
[GOAL]
a : Ordinal.{u_1}
⊢ a ^ 1 = a
[PROOFSTEP]
rw [← succ_zero, opow_succ]
[GOAL]
a : Ordinal.{u_1}
⊢ a ^ 0 * a = a
[PROOFSTEP]
simp only [opow_zero, one_mul]
[GOAL]
a : Ordinal.{u_1}
⊢ 1 ^ a = 1
[PROOFSTEP]
induction a using limitRecOn with
| H₁ => simp only [opow_zero]
| H₂ _ ih => simp only [opow_succ, ih, mul_one]
| H₃ b l IH =>
  refine' eq_of_forall_ge_iff fun c => _
  rw [opow_le_of_limit Ordinal.one_ne_zero l]
  exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩
[GOAL]
a : Ordinal.{u_1}
⊢ 1 ^ a = 1
[PROOFSTEP]
induction a using limitRecOn with
| H₁ => simp only [opow_zero]
| H₂ _ ih => simp only [opow_succ, ih, mul_one]
| H₃ b l IH =>
  refine' eq_of_forall_ge_iff fun c => _
  rw [opow_le_of_limit Ordinal.one_ne_zero l]
  exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩
[GOAL]
case H₁
⊢ 1 ^ 0 = 1
[PROOFSTEP]

| H₁ => simp only [opow_zero]
[GOAL]
case H₁
⊢ 1 ^ 0 = 1
[PROOFSTEP]
simp only [opow_zero]
[GOAL]
case H₂
o✝ : Ordinal.{u_1}
ih : 1 ^ o✝ = 1
⊢ 1 ^ succ o✝ = 1
[PROOFSTEP]

| H₂ _ ih => simp only [opow_succ, ih, mul_one]
[GOAL]
case H₂
o✝ : Ordinal.{u_1}
ih : 1 ^ o✝ = 1
⊢ 1 ^ succ o✝ = 1
[PROOFSTEP]
simp only [opow_succ, ih, mul_one]
[GOAL]
case H₃
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
⊢ 1 ^ b = 1
[PROOFSTEP]

| H₃ b l IH =>
  refine' eq_of_forall_ge_iff fun c => _
  rw [opow_le_of_limit Ordinal.one_ne_zero l]
  exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩
[GOAL]
case H₃
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
⊢ 1 ^ b = 1
[PROOFSTEP]
refine' eq_of_forall_ge_iff fun c => _
[GOAL]
case H₃
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ 1 ^ b ≤ c ↔ 1 ≤ c
[PROOFSTEP]
rw [opow_le_of_limit Ordinal.one_ne_zero l]
[GOAL]
case H₃
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ (∀ (b' : Ordinal.{u_1}), b' < b → 1 ^ b' ≤ c) ↔ 1 ≤ c
[PROOFSTEP]
exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩
[GOAL]
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
c : Ordinal.{u_1}
H : ∀ (b' : Ordinal.{u_1}), b' < b → 1 ^ b' ≤ c
⊢ 1 ≤ c
[PROOFSTEP]
simpa only [opow_zero] using H 0 l.pos
[GOAL]
b : Ordinal.{u_1}
l : IsLimit b
IH : ∀ (o' : Ordinal.{u_1}), o' < b → 1 ^ o' = 1
c : Ordinal.{u_1}
H : 1 ≤ c
b' : Ordinal.{u_1}
h : b' < b
⊢ 1 ^ b' ≤ c
[PROOFSTEP]
rwa [IH _ h]
[GOAL]
a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < a ^ b
[PROOFSTEP]
have h0 : 0 < (a ^ 0) := by simp only [opow_zero, zero_lt_one]
[GOAL]
a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < a ^ 0
[PROOFSTEP]
simp only [opow_zero, zero_lt_one]
[GOAL]
a b : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ b
[PROOFSTEP]
induction b using limitRecOn with
| H₁ => exact h0
| H₂ b IH =>
  rw [opow_succ]
  exact mul_pos IH a0
| H₃ b l _ => exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩
[GOAL]
a b : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ b
[PROOFSTEP]
induction b using limitRecOn with
| H₁ => exact h0
| H₂ b IH =>
  rw [opow_succ]
  exact mul_pos IH a0
| H₃ b l _ => exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩
[GOAL]
case H₁
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ 0
[PROOFSTEP]

| H₁ => exact h0
[GOAL]
case H₁
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ 0
[PROOFSTEP]
exact h0
[GOAL]
case H₂
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ succ b
[PROOFSTEP]

| H₂ b IH =>
  rw [opow_succ]
  exact mul_pos IH a0
[GOAL]
case H₂
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ succ b
[PROOFSTEP]
rw [opow_succ]
[GOAL]
case H₂
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ b * a
[PROOFSTEP]
exact mul_pos IH a0
[GOAL]
case H₃
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
l : IsLimit b
a✝ : ∀ (o' : Ordinal.{u_1}), o' < b → 0 < a ^ o'
⊢ 0 < a ^ b
[PROOFSTEP]

| H₃ b l _ => exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩
[GOAL]
case H₃
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
l : IsLimit b
a✝ : ∀ (o' : Ordinal.{u_1}), o' < b → 0 < a ^ o'
⊢ 0 < a ^ b
[PROOFSTEP]
exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩
[GOAL]
a : Ordinal.{u_1}
h : 1 < a
a0 : 0 < a
b : Ordinal.{u_1}
⊢ (fun x x_1 => x ^ x_1) a b < (fun x x_1 => x ^ x_1) a (succ b)
[PROOFSTEP]
simpa only [mul_one, opow_succ] using (mul_lt_mul_iff_left (opow_pos b a0)).2 h
[GOAL]
a b : Ordinal.{u_1}
l : IsLimit a
hb : b ≠ 0
⊢ IsLimit (a ^ b)
[PROOFSTEP]
rcases zero_or_succ_or_limit b with (e | ⟨b, rfl⟩ | l')
[GOAL]
case inl
a b : Ordinal.{u_1}
l : IsLimit a
hb : b ≠ 0
e : b = 0
⊢ IsLimit (a ^ b)
[PROOFSTEP]
exact absurd e hb
[GOAL]
case inr.inl.intro
a : Ordinal.{u_1}
l : IsLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ IsLimit (a ^ succ b)
[PROOFSTEP]
rw [opow_succ]
[GOAL]
case inr.inl.intro
a : Ordinal.{u_1}
l : IsLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ IsLimit (a ^ b * a)
[PROOFSTEP]
exact mul_isLimit (opow_pos _ l.pos) l
[GOAL]
case inr.inr
a b : Ordinal.{u_1}
l : IsLimit a
hb : b ≠ 0
l' : IsLimit b
⊢ IsLimit (a ^ b)
[PROOFSTEP]
exact opow_isLimit l.one_lt l'
[GOAL]
a b c : Ordinal.{u_1}
h₁ : 0 < a
h₂ : b ≤ c
⊢ a ^ b ≤ a ^ c
[PROOFSTEP]
cases' lt_or_eq_of_le (one_le_iff_pos.2 h₁) with h₁ h₁
[GOAL]
case inl
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 < a
⊢ a ^ b ≤ a ^ c
[PROOFSTEP]
exact (opow_le_opow_iff_right h₁).2 h₂
[GOAL]
case inr
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 = a
⊢ a ^ b ≤ a ^ c
[PROOFSTEP]
subst a
[GOAL]
case inr
b c : Ordinal.{u_1}
h₂ : b ≤ c
h₁ : 0 < 1
⊢ 1 ^ b ≤ 1 ^ c
[PROOFSTEP]
simp only [one_opow, le_refl]
[GOAL]
a b c : Ordinal.{u_1}
ab : a ≤ b
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]
by_cases a0 :
  a =
    0
      -- Porting note: `le_refl` is required.
[GOAL]
case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
a0 : a = 0
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]
subst a
[GOAL]
case pos
b c : Ordinal.{u_1}
ab : 0 ≤ b
⊢ 0 ^ c ≤ b ^ c
[PROOFSTEP]
by_cases c0 : c = 0
[GOAL]
case pos
b c : Ordinal.{u_1}
ab : 0 ≤ b
c0 : c = 0
⊢ 0 ^ c ≤ b ^ c
[PROOFSTEP]
subst c
[GOAL]
case pos
b : Ordinal.{u_1}
ab : 0 ≤ b
⊢ 0 ^ 0 ≤ b ^ 0
[PROOFSTEP]
simp only [opow_zero, le_refl]
[GOAL]
case neg
b c : Ordinal.{u_1}
ab : 0 ≤ b
c0 : ¬c = 0
⊢ 0 ^ c ≤ b ^ c
[PROOFSTEP]
simp only [zero_opow c0, Ordinal.zero_le]
[GOAL]
case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]
induction c using limitRecOn with
| H₁ => simp only [opow_zero, le_refl]
| H₂ c IH => simpa only [opow_succ] using mul_le_mul' IH ab
| H₃ c l IH =>
  exact
    (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)
[GOAL]
case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]
induction c using limitRecOn with
| H₁ => simp only [opow_zero, le_refl]
| H₂ c IH => simpa only [opow_succ] using mul_le_mul' IH ab
| H₃ c l IH =>
  exact
    (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)
[GOAL]
case neg.H₁
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ 0 ≤ b ^ 0
[PROOFSTEP]

| H₁ => simp only [opow_zero, le_refl]
[GOAL]
case neg.H₁
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
⊢ a ^ 0 ≤ b ^ 0
[PROOFSTEP]
simp only [opow_zero, le_refl]
[GOAL]
case neg.H₂
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal.{u_1}
IH : a ^ c ≤ b ^ c
⊢ a ^ succ c ≤ b ^ succ c
[PROOFSTEP]

| H₂ c IH => simpa only [opow_succ] using mul_le_mul' IH ab
[GOAL]
case neg.H₂
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal.{u_1}
IH : a ^ c ≤ b ^ c
⊢ a ^ succ c ≤ b ^ succ c
[PROOFSTEP]
simpa only [opow_succ] using mul_le_mul' IH ab
[GOAL]
case neg.H₃
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ o' ≤ b ^ o'
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]

| H₃ c l IH =>
  exact
    (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)
[GOAL]
case neg.H₃
a b : Ordinal.{u_1}
ab : a ≤ b
a0 : ¬a = 0
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ o' ≤ b ^ o'
⊢ a ^ c ≤ b ^ c
[PROOFSTEP]
exact
  (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)
[GOAL]
a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ≤ a ^ b
[PROOFSTEP]
nth_rw 1 [← opow_one a]
[GOAL]
a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
cases' le_or_gt a 1 with a1 a1
[GOAL]
case inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
cases' lt_or_eq_of_le a1 with a0 a1
[GOAL]
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a < 1
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
rw [lt_one_iff_zero] at a0 
[GOAL]
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
rw [a0, zero_opow Ordinal.one_ne_zero]
[GOAL]
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ 0 ^ b
[PROOFSTEP]
exact Ordinal.zero_le _
[GOAL]
case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
rw [a1, one_opow, one_opow]
[GOAL]
case inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a > 1
⊢ a ^ 1 ≤ a ^ b
[PROOFSTEP]
rwa [opow_le_opow_iff_right a1, one_le_iff_pos]
[GOAL]
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ succ c < b ^ succ c
[PROOFSTEP]
rw [opow_succ, opow_succ]
[GOAL]
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c * a < b ^ c * b
[PROOFSTEP]
exact
  (mul_le_mul_right' (opow_le_opow_left c ab.le) a).trans_lt
    (mul_lt_mul_of_pos_left ab (opow_pos c ((Ordinal.zero_le a).trans_lt ab)))
[GOAL]
a b c : Ordinal.{u_1}
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | a0)
[GOAL]
case inl
b c : Ordinal.{u_1}
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
[PROOFSTEP]
rcases eq_or_ne c 0 with (rfl | c0)
[GOAL]
case inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ (b + 0) = 0 ^ b * 0 ^ 0
[PROOFSTEP]
simp
[GOAL]
case inl.inr
b c : Ordinal.{u_1}
c0 : c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
[PROOFSTEP]
have : b + c ≠ 0 := ((Ordinal.pos_iff_ne_zero.2 c0).trans_le (le_add_left _ _)).ne'
[GOAL]
case inl.inr
b c : Ordinal.{u_1}
c0 : c ≠ 0
this : b + c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
[PROOFSTEP]
simp only [zero_opow c0, zero_opow this, mul_zero]
[GOAL]
case inr
a b c : Ordinal.{u_1}
a0 : a ≠ 0
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]
rcases eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with (rfl | a1)
[GOAL]
case inr.inl
b c : Ordinal.{u_1}
a0 : 1 ≠ 0
⊢ 1 ^ (b + c) = 1 ^ b * 1 ^ c
[PROOFSTEP]
simp only [one_opow, mul_one]
[GOAL]
case inr.inr
a b c : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]
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 => (((opow_isNormal a1).trans (add_isNormal b)).limit_le l).trans _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (((mul_isNormal <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans (opow_isNormal a1)).limit_le l).symm
[GOAL]
case inr.inr
a b c : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]
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 => (((opow_isNormal a1).trans (add_isNormal b)).limit_le l).trans _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (((mul_isNormal <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans (opow_isNormal a1)).limit_le l).symm
[GOAL]
case inr.inr.H₁
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + 0) = a ^ b * a ^ 0
[PROOFSTEP]

| H₁ => simp
[GOAL]
case inr.inr.H₁
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
⊢ a ^ (b + 0) = a ^ b * a ^ 0
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]

| H₂ c IH => rw [add_succ, opow_succ, IH, opow_succ, mul_assoc]
[GOAL]
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
[PROOFSTEP]
rw [add_succ, opow_succ, IH, opow_succ, mul_assoc]
[GOAL]
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b + o') = a ^ b * a ^ o'
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]

|
  H₃ c l IH =>
  refine' eq_of_forall_ge_iff fun d => (((opow_isNormal a1).trans (add_isNormal b)).limit_le l).trans _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (((mul_isNormal <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans (opow_isNormal a1)).limit_le l).symm
[GOAL]
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b + o') = a ^ b * a ^ o'
⊢ a ^ (b + c) = a ^ b * a ^ c
[PROOFSTEP]
refine' eq_of_forall_ge_iff fun d => (((opow_isNormal a1).trans (add_isNormal b)).limit_le l).trans _
[GOAL]
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), 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
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), b_1 < c → a ^ (b + b_1) ≤ d) ↔ a ^ b * a ^ c ≤ d
[PROOFSTEP]
simp (config := { contextual := true }) only [IH]
[GOAL]
case inr.inr.H₃
a b : Ordinal.{u_1}
a0 : a ≠ 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), b_1 < c → a ^ b * a ^ b_1 ≤ d) ↔ a ^ b * a ^ c ≤ d
[PROOFSTEP]
exact (((mul_isNormal <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans (opow_isNormal a1)).limit_le l).symm
[GOAL]
a b : Ordinal.{u_1}
⊢ a ^ (1 + b) = a * a ^ b
[PROOFSTEP]
rw [opow_add, opow_one]
[GOAL]
a b c : Ordinal.{u_1}
h : b ≤ c
⊢ a ^ c = a ^ b * a ^ (c - b)
[PROOFSTEP]
rw [← opow_add, Ordinal.add_sub_cancel_of_le h]
[GOAL]
a b c : Ordinal.{u_1}
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
by_cases b0 : b = 0
[GOAL]
case pos
a b c : Ordinal.{u_1}
b0 : b = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
simp only [b0, zero_mul, opow_zero, one_opow]
[GOAL]
case neg
a b c : Ordinal.{u_1}
b0 : ¬b = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
by_cases a0 : a = 0
[GOAL]
case pos
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : a = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
subst a
[GOAL]
case pos
b c : Ordinal.{u_1}
b0 : ¬b = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
[PROOFSTEP]
by_cases c0 : c = 0
[GOAL]
case pos
b c : Ordinal.{u_1}
b0 : ¬b = 0
c0 : c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
[PROOFSTEP]
simp only [c0, mul_zero, opow_zero]
[GOAL]
case neg
b c : Ordinal.{u_1}
b0 : ¬b = 0
c0 : ¬c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
[PROOFSTEP]
simp only [zero_opow b0, zero_opow c0, zero_opow (mul_ne_zero b0 c0)]
[GOAL]
case neg
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
cases' eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with a1 a1
[GOAL]
case neg.inl
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 = a
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
subst a1
[GOAL]
case neg.inl
b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬1 = 0
⊢ 1 ^ (b * c) = (1 ^ b) ^ c
[PROOFSTEP]
simp only [one_opow]
[GOAL]
case neg.inr
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
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 =>
      (((opow_isNormal a1).trans (mul_isNormal (Ordinal.pos_iff_ne_zero.2 b0))).limit_le l).trans _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm
[GOAL]
case neg.inr
a b c : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
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 =>
      (((opow_isNormal a1).trans (mul_isNormal (Ordinal.pos_iff_ne_zero.2 b0))).limit_le l).trans _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm
[GOAL]
case neg.inr.H₁
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * 0) = (a ^ b) ^ 0
[PROOFSTEP]

| H₁ => simp only [mul_zero, opow_zero]
[GOAL]
case neg.inr.H₁
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
⊢ a ^ (b * 0) = (a ^ b) ^ 0
[PROOFSTEP]
simp only [mul_zero, opow_zero]
[GOAL]
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
[PROOFSTEP]

| H₂ c IH => rw [mul_succ, opow_add, IH, opow_succ]
[GOAL]
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
[PROOFSTEP]
rw [mul_succ, opow_add, IH, opow_succ]
[GOAL]
case neg.inr.H₃
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b * o') = (a ^ b) ^ o'
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]

|
  H₃ c l IH =>
  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 _
  dsimp only [Function.comp]
  simp (config := { contextual := true }) only [IH]
  exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm
[GOAL]
case neg.inr.H₃
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b * o') = (a ^ b) ^ o'
⊢ a ^ (b * c) = (a ^ b) ^ c
[PROOFSTEP]
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 _
[GOAL]
case neg.inr.H₃
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), 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
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
case neg.inr.H₃
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), b_1 < c → a ^ (b * b_1) ≤ d) ↔ (a ^ b) ^ c ≤ d
[PROOFSTEP]
simp (config := { contextual := true }) only [IH]
[GOAL]
case neg.inr.H₃
a b : Ordinal.{u_1}
b0 : ¬b = 0
a0 : ¬a = 0
a1 : 1 < a
c : Ordinal.{u_1}
l : IsLimit c
IH : ∀ (o' : Ordinal.{u_1}), o' < c → a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal.{u_1}
⊢ (∀ (b_1 : Ordinal.{u_1}), b_1 < c → (a ^ b) ^ b_1 ≤ d) ↔ (a ^ b) ^ c ≤ d
[PROOFSTEP]
exact (opow_le_of_limit (opow_ne_zero _ a0) l).symm
[GOAL]
b : Ordinal.{u_1}
h : 1 < b
x : Ordinal.{u_1}
⊢ log b x = pred (sInf {o | x < b ^ o})
[PROOFSTEP]
simp only [log, dif_pos h]
[GOAL]
b : Ordinal.{u_1}
h : ¬1 < b
x : Ordinal.{u_1}
⊢ log b x = 0
[PROOFSTEP]
simp only [log, dif_neg h]
[GOAL]
b : Ordinal.{u_1}
b1 : 1 < b
⊢ log b 0 = 0
[PROOFSTEP]
rw [log_def b1, ← Ordinal.le_zero, pred_le]
[GOAL]
b : Ordinal.{u_1}
b1 : 1 < b
⊢ sInf {o | 0 < b ^ o} ≤ succ 0
[PROOFSTEP]
apply csInf_le'
[GOAL]
case h
b : Ordinal.{u_1}
b1 : 1 < b
⊢ succ 0 ∈ {o | 0 < b ^ o}
[PROOFSTEP]
dsimp
[GOAL]
case h
b : Ordinal.{u_1}
b1 : 1 < b
⊢ 0 < b ^ succ 0
[PROOFSTEP]
rw [succ_zero, opow_one]
[GOAL]
case h
b : Ordinal.{u_1}
b1 : 1 < b
⊢ 0 < b
[PROOFSTEP]
exact zero_lt_one.trans b1
[GOAL]
b : Ordinal.{u_1}
b1 : ¬1 < b
⊢ log b 0 = 0
[PROOFSTEP]
simp only [log_of_not_one_lt_left b1]
[GOAL]
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
let t := sInf {o | x < (b ^ o)}
[GOAL]
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
have : x < (b ^ t) := csInf_mem (log_nonempty hb)
[GOAL]
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
rcases zero_or_succ_or_limit t with (h | h | h)
[GOAL]
case inl
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
h : t = 0
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
refine' ((one_le_iff_ne_zero.2 hx).not_lt _).elim
[GOAL]
case inl
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
h : t = 0
⊢ x < 1
[PROOFSTEP]
simpa only [h, opow_zero] using this
[GOAL]
case inr.inl
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
h : ∃ a, t = succ a
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
rw [show log b x = pred t from log_def hb x, succ_pred_iff_is_succ.2 h]
[GOAL]
case inr.inr
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
h : IsLimit t
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
rcases(lt_opow_of_limit (zero_lt_one.trans hb).ne' h).1 this with ⟨a, h₁, h₂⟩
[GOAL]
case inr.inr.intro.intro
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
t : Ordinal.{u_1} := sInf {o | x < b ^ o}
this : x < b ^ t
h : IsLimit t
a : Ordinal.{u_1}
h₁ : a < t
h₂ : x < b ^ a
⊢ succ (log b x) = sInf {o | x < b ^ o}
[PROOFSTEP]
exact h₁.not_le.elim ((le_csInf_iff'' (log_nonempty hb)).1 le_rfl a h₂)
[GOAL]
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x < b ^ succ (log b x)
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b ^ succ (log b 0)
[PROOFSTEP]
apply opow_pos _ (zero_lt_one.trans hb)
[GOAL]
case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)
[PROOFSTEP]
rw [succ_log_def hb hx]
[GOAL]
case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ sInf {o | x < b ^ o}
[PROOFSTEP]
exact csInf_mem (log_nonempty hb)
[GOAL]
b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ b ^ log b x ≤ x
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | b0)
[GOAL]
case inl
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ 0 ^ log 0 x ≤ x
[PROOFSTEP]
rw [zero_opow']
[GOAL]
case inl
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ 1 - log 0 x ≤ x
[PROOFSTEP]
refine' (sub_le_self _ _).trans (one_le_iff_ne_zero.2 hx)
[GOAL]
case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
⊢ b ^ log b x ≤ x
[PROOFSTEP]
rcases lt_or_eq_of_le (one_le_iff_ne_zero.2 b0) with (hb | rfl)
[GOAL]
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
⊢ b ^ log b x ≤ x
[PROOFSTEP]
refine' le_of_not_lt fun h => (lt_succ (log b x)).not_le _
[GOAL]
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
⊢ succ (log b x) ≤ log b x
[PROOFSTEP]
have := @csInf_le' _ _ {o | x < (b ^ o)} _ h
[GOAL]
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
b0 : b ≠ 0
hb : 1 < b
h : x < b ^ log b x
this : sInf {o | x < b ^ o} ≤ log b x
⊢ succ (log b x) ≤ log b x
[PROOFSTEP]
rwa [← succ_log_def hb hx] at this 
[GOAL]
case inr.inr
x : Ordinal.{u_1}
hx : x ≠ 0
b0 : 1 ≠ 0
⊢ 1 ^ log 1 x ≤ x
[PROOFSTEP]
rwa [one_opow, one_le_iff_ne_zero]
[GOAL]
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ 0 < log b o
[PROOFSTEP]
rwa [← succ_le_iff, succ_zero, ← opow_le_iff_le_log hb ho, opow_one]
[GOAL]
b o : Ordinal.{u_1}
hbo : o < b
⊢ log b o = 0
[PROOFSTEP]
rcases eq_or_ne o 0 with (rfl | ho)
[GOAL]
case inl
b : Ordinal.{u_1}
hbo : 0 < b
⊢ log b 0 = 0
[PROOFSTEP]
exact log_zero_right b
[GOAL]
case inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
⊢ log b o = 0
[PROOFSTEP]
cases' le_or_lt b 1 with hb hb
[GOAL]
case inr.inl
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : b ≤ 1
⊢ log b o = 0
[PROOFSTEP]
rcases le_one_iff.1 hb with (rfl | rfl)
[GOAL]
case inr.inl.inl
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 0
hb : 0 ≤ 1
⊢ log 0 o = 0
[PROOFSTEP]
exact log_zero_left o
[GOAL]
case inr.inl.inr
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 1
hb : 1 ≤ 1
⊢ log 1 o = 0
[PROOFSTEP]
exact log_one_left o
[GOAL]
case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o = 0
[PROOFSTEP]
rwa [← Ordinal.le_zero, ← lt_succ_iff, succ_zero, ← lt_opow_iff_log_lt hb ho, opow_one]
[GOAL]
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x = 0
⊢ log b x ≤ log b y
[PROOFSTEP]
simp only [hx, log_zero_right, Ordinal.zero_le]
[GOAL]
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : ¬x = 0
hb : ¬1 < b
⊢ log b x ≤ log b y
[PROOFSTEP]
simp only [log_of_not_one_lt_left hb, Ordinal.zero_le]
[GOAL]
b x : Ordinal.{u_1}
hx : x = 0
⊢ log b x ≤ x
[PROOFSTEP]
simp only [hx, log_zero_right, Ordinal.zero_le]
[GOAL]
b x : Ordinal.{u_1}
hx : ¬x = 0
hb : ¬1 < b
⊢ log b x ≤ x
[PROOFSTEP]
simp only [log_of_not_one_lt_left hb, Ordinal.zero_le]
[GOAL]
b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % b ^ log b o < o
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb)
[GOAL]
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % 0 ^ log 0 o < o
[PROOFSTEP]
simpa using Ordinal.pos_iff_ne_zero.2 ho
[GOAL]
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : b ≠ 0
⊢ o % b ^ log b o < o
[PROOFSTEP]
exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)
[GOAL]
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ log b (o % b ^ log b o) < log b o
[PROOFSTEP]
cases' eq_or_ne (o % (b ^ log b o)) 0 with h h
[GOAL]
case inl
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ log b (o % b ^ log b o) < log b o
[PROOFSTEP]
rw [h, log_zero_right]
[GOAL]
case inl
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o
[PROOFSTEP]
apply log_pos hb ho hbo
[GOAL]
case inr
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b (o % b ^ log b o) < log b o
[PROOFSTEP]
rw [← succ_le_iff, succ_log_def hb h]
[GOAL]
case inr
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ sInf {o_1 | o % b ^ log b o < b ^ o_1} ≤ log b o
[PROOFSTEP]
apply csInf_le'
[GOAL]
case inr.h
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b o ∈ {o_1 | o % b ^ log b o < b ^ o_1}
[PROOFSTEP]
apply mod_lt
[GOAL]
case inr.h.h
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ b ^ log b o ≠ 0
[PROOFSTEP]
rw [← Ordinal.pos_iff_ne_zero]
[GOAL]
case inr.h.h
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ 0 < b ^ log b o
[PROOFSTEP]
exact opow_pos _ (zero_lt_one.trans hb)
[GOAL]
b u w v : Ordinal.{u_1}
hw : w < b ^ u
⊢ b ^ u * v + w < b ^ u * succ v
[PROOFSTEP]
rwa [mul_succ, add_lt_add_iff_left]
[GOAL]
b u v w : Ordinal.{u_1}
hvb : v < b
hw : w < b ^ u
⊢ b ^ u * v + w < b ^ succ u
[PROOFSTEP]
convert (opow_mul_add_lt_opow_mul_succ v hw).trans_le (mul_le_mul_left' (succ_le_of_lt hvb) _) using 1
[GOAL]
case h.e'_4
b u v w : Ordinal.{u_1}
hvb : v < b
hw : w < b ^ u
⊢ b ^ succ u = b ^ u * b
[PROOFSTEP]
exact opow_succ b u
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
⊢ log b (b ^ u * v + w) = u
[PROOFSTEP]
have hne' := (opow_mul_add_pos (zero_lt_one.trans hb).ne' u hv w).ne'
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
⊢ log b (b ^ u * v + w) = u
[PROOFSTEP]
by_contra' hne
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
⊢ False
[PROOFSTEP]
cases' lt_or_gt_of_ne hne with h h
[GOAL]
case inl
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : log b (b ^ u * v + w) < u
⊢ False
[PROOFSTEP]
rw [← lt_opow_iff_log_lt hb hne'] at h 
[GOAL]
case inl
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : b ^ u * v + w < b ^ u
⊢ False
[PROOFSTEP]
exact h.not_le ((le_mul_left _ (Ordinal.pos_iff_ne_zero.2 hv)).trans (le_add_right _ _))
[GOAL]
case inr
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : log b (b ^ u * v + w) > u
⊢ False
[PROOFSTEP]
conv at h => change u < log b (b ^ u * v + w)
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : log b (b ^ u * v + w) > u
| log b (b ^ u * v + w) > u
[PROOFSTEP]
change u < log b (b ^ u * v + w)
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : log b (b ^ u * v + w) > u
| log b (b ^ u * v + w) > u
[PROOFSTEP]
change u < log b (b ^ u * v + w)
[GOAL]
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : log b (b ^ u * v + w) > u
| log b (b ^ u * v + w) > u
[PROOFSTEP]
change u < log b (b ^ u * v + w)
[GOAL]
case inr
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h : u < log b (b ^ u * v + w)
⊢ False
[PROOFSTEP]
rw [← succ_le_iff, ← opow_le_iff_le_log hb hne'] at h 
[GOAL]
case inr
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hvb : v < b
hw : w < b ^ u
hne' : b ^ u * v + w ≠ 0
hne : log b (b ^ u * v + w) ≠ u
h✝ : u < log b (b ^ u * v + w)
h : b ^ succ u ≤ b ^ u * v + w
⊢ False
[PROOFSTEP]
exact (not_lt_of_le h) (opow_mul_add_lt_opow_succ hvb hw)
[GOAL]
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = x
[PROOFSTEP]
convert log_opow_mul_add hb zero_ne_one.symm hb (opow_pos x (zero_lt_one.trans hb)) using 1
[GOAL]
case h.e'_2
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = log b (b ^ x * 1 + 0)
[PROOFSTEP]
rw [add_zero, mul_one]
[GOAL]
b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / b ^ log b o
[PROOFSTEP]
rcases eq_zero_or_pos b with (rfl | hb)
[GOAL]
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / 0 ^ log 0 o
[PROOFSTEP]
simpa using Ordinal.pos_iff_ne_zero.2 ho
[GOAL]
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ 0 < o / b ^ log b o
[PROOFSTEP]
rw [div_pos (opow_ne_zero _ hb.ne')]
[GOAL]
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ b ^ log b o ≤ o
[PROOFSTEP]
exact opow_log_le_self b ho
[GOAL]
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o / b ^ log b o < b
[PROOFSTEP]
rw [div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ]
[GOAL]
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o < b ^ succ (log b o)
[PROOFSTEP]
exact lt_opow_succ_log_self hb o
[GOAL]
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
⊢ log b x + log b y ≤ log b (x * y)
[PROOFSTEP]
by_cases hb : 1 < b
[GOAL]
case pos
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ log b x + log b y ≤ log b (x * y)
[PROOFSTEP]
rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]
[GOAL]
case pos
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ log b x * b ^ log b y ≤ x * y
[PROOFSTEP]
exact
  mul_le_mul' (opow_log_le_self b hx)
    (opow_log_le_self b hy)
      -- Porting note: `le_refl` is required.
[GOAL]
case neg
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : ¬1 < b
⊢ log b x + log b y ≤ log b (x * y)
[PROOFSTEP]
simp only [log_of_not_one_lt_left hb, zero_add, le_refl]
[GOAL]
m : ℕ
⊢ ↑(m ^ 0) = ↑m ^ ↑0
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
⊢ ↑(m ^ (n + 1)) = ↑m ^ ↑(n + 1)
[PROOFSTEP]
rw [pow_succ', nat_cast_mul, nat_cast_opow m n, Nat.cast_succ, add_one_eq_succ, opow_succ]
[GOAL]
o : Ordinal.{u_1}
ho : 0 < o
⊢ (sup fun n => o ^ ↑n) = o ^ ω
[PROOFSTEP]
rcases lt_or_eq_of_le (one_le_iff_pos.2 ho) with (ho₁ | rfl)
[GOAL]
case inl
o : Ordinal.{u_1}
ho : 0 < o
ho₁ : 1 < o
⊢ (sup fun n => o ^ ↑n) = o ^ ω
[PROOFSTEP]
exact (opow_isNormal ho₁).apply_omega
[GOAL]
case inr
ho : 0 < 1
⊢ (sup fun n => 1 ^ ↑n) = 1 ^ ω
[PROOFSTEP]
rw [one_opow]
[GOAL]
case inr
ho : 0 < 1
⊢ (sup fun n => 1 ^ ↑n) = 1
[PROOFSTEP]
refine' le_antisymm (sup_le fun n => by rw [one_opow]) _
[GOAL]
ho : 0 < 1
n : ℕ
⊢ 1 ^ ↑n ≤ 1
[PROOFSTEP]
rw [one_opow]
[GOAL]
case inr
ho : 0 < 1
⊢ 1 ≤ sup fun n => 1 ^ ↑n
[PROOFSTEP]
convert le_sup (fun n : ℕ => 1 ^ n) 0
[GOAL]
case h.e'_3
ho : 0 < 1
⊢ 1 = 1 ^ ↑0
[PROOFSTEP]
rw [Nat.cast_zero, opow_zero]
