no goals
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
h : f = g
⊢ f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
simp [h]
case H₁
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a : Ordinal
⊢ f 0 = g 0

case H₂
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a : Ordinal
⊢ ∀ (o : Ordinal), f o = g o → f (succ o) = g (succ o)

case H₃
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a : Ordinal
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → f o' = g o') → f o = g o
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a : Ordinal
⊢ f a = g a
apply a.limitRecOn
case H₃
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a : Ordinal
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → f o' = g o') → f o = g o
case H₁
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a : Ordinal
⊢ f 0 = g 0

case H₂
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a : Ordinal
⊢ ∀ (o : Ordinal), f o = g o → f (succ o) = g (succ o)

case H₃
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a : Ordinal
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → f o' = g o') → f o = g o
assumption'
case H₃
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a o : Ordinal
ho : IsLimit o
H : ∀ (o' : Ordinal), o' < o → f o' = g o'
⊢ f o = g o
case H₃
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a : Ordinal
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → f o' = g o') → f o = g o
intro o ho H
case H₃
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a o : Ordinal
ho : IsLimit o
H : ∀ (o' : Ordinal), o' < o → f o' = g o'
⊢ (Ordinal.bsup o fun x x_1 => f x) = Ordinal.bsup o fun x x_1 => g x
case H₃
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a o : Ordinal
ho : IsLimit o
H : ∀ (o' : Ordinal), o' < o → f o' = g o'
⊢ f o = g o
rw [← IsNormal.bsup_eq.{u, u} hf ho, ← IsNormal.bsup_eq.{u, u} hg ho]
case H₃.e_f
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a o : Ordinal
ho : IsLimit o
H : ∀ (o' : Ordinal), o' < o → f o' = g o'
⊢ (fun x x_1 => f x) = fun x x_1 => g x
case H₃
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a o : Ordinal
ho : IsLimit o
H : ∀ (o' : Ordinal), o' < o → f o' = g o'
⊢ (Ordinal.bsup o fun x x_1 => f x) = Ordinal.bsup o fun x x_1 => g x
congr
case H₃.e_f.h.h
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a o : Ordinal
ho : IsLimit o
H : ∀ (o' : Ordinal), o' < o → f o' = g o'
b : Ordinal
hb : b < o
⊢ f b = g b
case H₃.e_f
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a o : Ordinal
ho : IsLimit o
H : ∀ (o' : Ordinal), o' < o → f o' = g o'
⊢ (fun x x_1 => f x) = fun x x_1 => g x
ext (b hb)
no goals
case H₃.e_f.h.h
α : Type ?u.371664
β : Type ?u.371667
γ : Type ?u.371670
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f g : Ordinal → Ordinal
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal), f a = g a → f (succ a) = g (succ a)
a o : Ordinal
ho : IsLimit o
H : ∀ (o' : Ordinal), o' < o → f o' = g o'
b : Ordinal
hb : b < o
⊢ f b = g b
exact H b hb