-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.eq_iff_zero_and_succ {f g : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f)
    (hg : IsNormal g) : f = g ↔ f 0 = g 0 ∧ ∀ a, f a = g a → f (succ a) = g (succ a) :=
  ⟨fun h => by simp [h], fun ⟨h₁, h₂⟩ =>
    funext fun a => by
      induction a using limitRecOn with
      | H₁ => solve_by_elim
      | H₂ => solve_by_elim
      | H₃ _ ho H =>
        rw [← IsNormal.bsup_eq.{u, u} hf ho, ← IsNormal.bsup_eq.{u, u} hg ho]
        congr
        ext b hb
        exact H b hb⟩

Proof state:
case H₁
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
⊢ f 0 = g 0

Tactic:
solve_by_elim

Result:
no goals

Proof state:
case H₃.e_f
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
o✝ : Ordinal.{u}
ho : o✝.IsLimit
H : ∀ o' < o✝, f o' = g o'
⊢ (fun x x_1 => f x) = fun x x_1 => g x

Tactic:
ext b hb

Result:
case H₃.e_f.h.h
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
o✝ : Ordinal.{u}
ho : o✝.IsLimit
H : ∀ o' < o✝, f o' = g o'
b : Ordinal.{u}
hb : b < o✝
⊢ f b = g b

Proof state:
case H₃
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
o✝ : Ordinal.{u}
ho : o✝.IsLimit
H : ∀ o' < o✝, f o' = g o'
⊢ f o✝ = g o✝

Tactic:
rw [← IsNormal.bsup_eq.{u, u} hf ho, ← IsNormal.bsup_eq.{u, u} hg ho]

Result:
case H₃
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
o✝ : Ordinal.{u}
ho : o✝.IsLimit
H : ∀ o' < o✝, f o' = g o'
⊢ (o✝.bsup fun x x_1 => f x) = o✝.bsup fun x x_1 => g x

Proof state:
case H₂
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
o✝ : Ordinal.{u}
a✝ : f o✝ = g o✝
⊢ f (succ o✝) = g (succ o✝)

Tactic:
solve_by_elim

Result:
no goals

Proof state:
case H₃
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
o✝ : Ordinal.{u}
ho : o✝.IsLimit
H : ∀ o' < o✝, f o' = g o'
⊢ (o✝.bsup fun x x_1 => f x) = o✝.bsup fun x x_1 => g x

Tactic:
congr

Result:
case H₃.e_f
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
o✝ : Ordinal.{u}
ho : o✝.IsLimit
H : ∀ o' < o✝, f o' = g o'
⊢ (fun x x_1 => f x) = fun x x_1 => g x

Proof state:
case H₃.e_f.h.h
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
o✝ : Ordinal.{u}
ho : o✝.IsLimit
H : ∀ o' < o✝, f o' = g o'
b : Ordinal.{u}
hb : b < o✝
⊢ f b = g b

Tactic:
exact H b hb

Result:
no goals

Proof state:
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
h : f = g
⊢ f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)

Tactic:
simp [h]

Result:
no goals

Proof state:
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
x✝ : f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
h₁ : f 0 = g 0
h₂ : ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)
a : Ordinal.{u}
⊢ f a = g a

Tactic:
induction a using limitRecOn with
| H₁ => solve_by_elim
| H₂ => solve_by_elim
| H₃ _ ho H =>
  rw [← IsNormal.bsup_eq.{u, u} hf ho, ← IsNormal.bsup_eq.{u, u} hg ho]
  congr
  ext b hb
  exact H b hb

Result:
no goals