α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
⊢ limitRecOn (succ o) H₁ H₂ H₃ = H₂ o (limitRecOn o H₁ H₂ H₃)
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
⊢ limitRecOn (succ o) H₁ H₂ H₃ = H₂ o (limitRecOn o H₁ H₂ H₃)
have h : ∃ a, succ o = succ a := ⟨_, rfl⟩
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
⊢ Eq.mpr (_ : C (succ o) = C (succ (pred (succ o))))
      (H₂ (pred (succ o))
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          (pred (succ o)) (_ : pred (succ o) < succ o))) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
⊢ limitRecOn (succ o) H₁ H₂ H₃ = H₂ o (limitRecOn o H₁ H₂ H₃)
rw [limitRecOn, lt_wf.fix_eq, dif_neg (succ_ne_zero o), dif_pos h]
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
h₂ : C (succ o) = C (succ (pred (succ o)))
⊢ Eq.mpr h₂
      (H₂ (pred (succ o))
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          (pred (succ o)) (_ : pred (succ o) < succ o))) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
⊢ Eq.mpr (_ : C (succ o) = C (succ (pred (succ o))))
      (H₂ (pred (succ o))
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          (pred (succ o)) (_ : pred (succ o) < succ o))) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
generalize limitRecOn.proof_2 (succ o) h = h₂
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
h₂ : C (succ o) = C (succ (pred (succ o)))
h₃ : pred (succ o) < succ o
⊢ Eq.mpr h₂
      (H₂ (pred (succ o))
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          (pred (succ o)) h₃)) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
h₂ : C (succ o) = C (succ (pred (succ o)))
⊢ Eq.mpr h₂
      (H₂ (pred (succ o))
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          (pred (succ o)) (_ : pred (succ o) < succ o))) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
generalize limitRecOn.proof_3 (succ o) h = h₃
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
⊢ ∀ (h₂ : C (succ o) = C (succ (pred (succ o)))) (h₃ : pred (succ o) < succ o),
    Eq.mpr h₂
        (H₂ (pred (succ o))
          ((fun y x =>
              WellFounded.fix lt_wf
                (fun o IH =>
                  if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                  else
                    if h : ∃ a, o = succ a then
                      Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                    else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
                y)
            (pred (succ o)) h₃)) =
      H₂ o (limitRecOn o H₁ H₂ H₃)
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
h₂ : C (succ o) = C (succ (pred (succ o)))
h₃ : pred (succ o) < succ o
⊢ Eq.mpr h₂
      (H₂ (pred (succ o))
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          (pred (succ o)) h₃)) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
revert h₂ h₃
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
o' : Ordinal
e : pred (succ o) = o'
⊢ ∀ (h₂ : C (succ o) = C (succ o')) (h₃ : o' < succ o),
    Eq.mpr h₂
        (H₂ o'
          ((fun y x =>
              WellFounded.fix lt_wf
                (fun o IH =>
                  if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                  else
                    if h : ∃ a, o = succ a then
                      Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                    else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
                y)
            o' h₃)) =
      H₂ o (limitRecOn o H₁ H₂ H₃)
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
⊢ ∀ (h₂ : C (succ o) = C (succ (pred (succ o)))) (h₃ : pred (succ o) < succ o),
    Eq.mpr h₂
        (H₂ (pred (succ o))
          ((fun y x =>
              WellFounded.fix lt_wf
                (fun o IH =>
                  if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                  else
                    if h : ∃ a, o = succ a then
                      Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                    else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
                y)
            (pred (succ o)) h₃)) =
      H₂ o (limitRecOn o H₁ H₂ H₃)
generalize e : pred (succ o) = o'
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
o' : Ordinal
e : pred (succ o) = o'
h₂✝ : C (succ o) = C (succ o')
h₃✝ : o' < succ o
⊢ Eq.mpr h₂✝
      (H₂ o'
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          o' h₃✝)) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
o' : Ordinal
e : pred (succ o) = o'
⊢ ∀ (h₂ : C (succ o) = C (succ o')) (h₃ : o' < succ o),
    Eq.mpr h₂
        (H₂ o'
          ((fun y x =>
              WellFounded.fix lt_wf
                (fun o IH =>
                  if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                  else
                    if h : ∃ a, o = succ a then
                      Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                    else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
                y)
            o' h₃)) =
      H₂ o (limitRecOn o H₁ H₂ H₃)
intros
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
o' : Ordinal
e : o = o'
h₂✝ : C (succ o) = C (succ o')
h₃✝ : o' < succ o
⊢ Eq.mpr h₂✝
      (H₂ o'
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          o' h₃✝)) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
o' : Ordinal
e : pred (succ o) = o'
h₂✝ : C (succ o) = C (succ o')
h₃✝ : o' < succ o
⊢ Eq.mpr h₂✝
      (H₂ o'
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          o' h₃✝)) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
rw [pred_succ] at e
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
h₂✝ : C (succ o) = C (succ o)
h₃✝ : o < succ o
⊢ Eq.mpr h₂✝
      (H₂ o
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          o h₃✝)) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
o' : Ordinal
e : o = o'
h₂✝ : C (succ o) = C (succ o')
h₃✝ : o' < succ o
⊢ Eq.mpr h₂✝
      (H₂ o'
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          o' h₃✝)) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
subst o'
no goals
α : Type ?u.96324
β : Type ?u.96327
γ : Type ?u.96330
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
o : Ordinal
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
h : ∃ a, succ o = succ a
h₂✝ : C (succ o) = C (succ o)
h₃✝ : o < succ o
⊢ Eq.mpr h₂✝
      (H₂ o
        ((fun y x =>
            WellFounded.fix lt_wf
              (fun o IH =>
                if o0 : o = 0 then Eq.mpr (_ : C o = C 0) H₁
                else
                  if h : ∃ a, o = succ a then
                    Eq.mpr (_ : C o = C (succ (pred o))) (H₂ (pred o) (IH (pred o) (_ : pred o < o)))
                  else H₃ o (_ : o ≠ 0 ∧ ∀ (a : Ordinal), a < o → succ a < o) IH)
              y)
          o h₃✝)) =
    H₂ o (limitRecOn o H₁ H₂ H₃)
rfl