case H₁
a : Ordinal
⊢ 1 ^ 0 = 1

case H₂
a : Ordinal
⊢ ∀ (o : Ordinal), 1 ^ o = 1 → 1 ^ succ o = 1

case H₃
a : Ordinal
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → 1 ^ o' = 1) → 1 ^ o = 1
a : Ordinal
⊢ 1 ^ a = 1
apply limitRecOn a
case H₃
a b : Ordinal
l : IsLimit b
IH : ∀ (o' : Ordinal), o' < b → 1 ^ o' = 1
c : Ordinal
⊢ 1 ^ b ≤ c ↔ 1 ≤ c
case H₃
a : Ordinal
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → 1 ^ o' = 1) → 1 ^ o = 1
refine' fun b l IH => eq_of_forall_ge_iff fun c => _
case H₃
a b : Ordinal
l : IsLimit b
IH : ∀ (o' : Ordinal), o' < b → 1 ^ o' = 1
c : Ordinal
⊢ (∀ (b' : Ordinal), b' < b → 1 ^ b' ≤ c) ↔ 1 ≤ c
case H₃
a b : Ordinal
l : IsLimit b
IH : ∀ (o' : Ordinal), o' < b → 1 ^ o' = 1
c : Ordinal
⊢ 1 ^ b ≤ c ↔ 1 ≤ c
rw [opow_le_of_limit Ordinal.one_ne_zero l]
no goals
case H₃
a b : Ordinal
l : IsLimit b
IH : ∀ (o' : Ordinal), o' < b → 1 ^ o' = 1
c : Ordinal
⊢ (∀ (b' : Ordinal), b' < b → 1 ^ b' ≤ c) ↔ 1 ≤ c
exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩
no goals
case H₁
a : Ordinal
⊢ 1 ^ 0 = 1
simp only [opow_zero]
case H₂
a o✝ : Ordinal
ih : 1 ^ o✝ = 1
⊢ 1 ^ succ o✝ = 1
case H₂
a : Ordinal
⊢ ∀ (o : Ordinal), 1 ^ o = 1 → 1 ^ succ o = 1
intro _ ih
no goals
case H₂
a o✝ : Ordinal
ih : 1 ^ o✝ = 1
⊢ 1 ^ succ o✝ = 1
simp only [opow_succ, ih, mul_one]
no goals
a b : Ordinal
l : IsLimit b
IH : ∀ (o' : Ordinal), o' < b → 1 ^ o' = 1
c : Ordinal
H : ∀ (b' : Ordinal), b' < b → 1 ^ b' ≤ c
⊢ 1 ≤ c
simpa only [opow_zero] using H 0 l.pos
no goals
a b : Ordinal
l : IsLimit b
IH : ∀ (o' : Ordinal), o' < b → 1 ^ o' = 1
c : Ordinal
H : 1 ≤ c
b' : Ordinal
h : b' < b
⊢ 1 ^ b' ≤ c
rwa [IH _ h]