awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
l : Ordinal.{u_5}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_5 + 1)) → Sort u_4
o : (↑(Iio l) : Type (u_5 + 1))
zero : motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ⋯)
succ :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (Order.succ (↑o : Ordinal.{u_5})) ⋯)
limit :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_5}) → ((o' : (↑(Iio l) : Type (u_5 + 1))) → o' < o → motive o') → motive o
⊢ motive o
have obtain : (o : Ordinal.{u_5}) → (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)
Tactic: obtain ⟨o, ho⟩ := o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
l : Ordinal.{u_5}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_5 + 1)) → Sort u_4
zero : motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ⋯)
succ :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (Order.succ (↑o : Ordinal.{u_5})) ⋯)
limit :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_5}) → ((o' : (↑(Iio l) : Type (u_5 + 1))) → o' < o → motive o') → motive o
o : Ordinal.{u_5}
IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)
ho : o + 1 ∈ Iio l
⊢ motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (o + 1) ho)
have add_one : (ho' : o < l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (o + 1) ho)
Tactic: have ho' : o < l := (lt_succ o).trans ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
l : Ordinal.{u_5}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_5 + 1)) → Sort u_4
zero : motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ⋯)
succ :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (Order.succ (↑o : Ordinal.{u_5})) ⋯)
limit :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_5}) → ((o' : (↑(Iio l) : Type (u_5 + 1))) → o' < o → motive o') → motive o
o : Ordinal.{u_5}
ho : o ∈ Iio l
⊢ motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)
have zero₁ : (ho : 0 ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ho)
Tactic: induction o using limitRecOn with
  | zero => exact zero
  | add_one o IH =>
    have ho' : o < l := (lt_succ o).trans ho
    exact succ ⟨o, ho'⟩ (IH ho')
  | limit o ho' IH => exact limit _ ho' fun a ha ↦ IH a.1 ha (ha.trans (c := l) ho)
Cleared hypotheses: o, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
l : Ordinal.{u_5}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_5 + 1)) → Sort u_4
zero : motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ⋯)
succ :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (Order.succ (↑o : Ordinal.{u_5})) ⋯)
limit :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_5}) → ((o' : (↑(Iio l) : Type (u_5 + 1))) → o' < o → motive o') → motive o
o : Ordinal.{u_5}
ho : o ∈ Iio l
zero₁ : (ho : 0 ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ho)
⊢ motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)
have add_one : (o : Ordinal.{u_5}) →
  (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)) →
    (ho : o + 1 ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (o + 1) ho)
Tactic: induction o using limitRecOn with
  | zero => exact zero
  | add_one o IH =>
    have ho' : o < l := (lt_succ o).trans ho
    exact succ ⟨o, ho'⟩ (IH ho')
  | limit o ho' IH => exact limit _ ho' fun a ha ↦ IH a.1 ha (ha.trans (c := l) ho)
Cleared hypotheses: o, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
l : Ordinal.{u_5}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_5 + 1)) → Sort u_4
zero : motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ⋯)
succ :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (Order.succ (↑o : Ordinal.{u_5})) ⋯)
limit :
  (o : (↑(Iio l) : Type (u_5 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_5}) → ((o' : (↑(Iio l) : Type (u_5 + 1))) → o' < o → motive o') → motive o
o : Ordinal.{u_5}
ho : o ∈ Iio l
zero₁ : (ho : 0 ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) 0 ho)
add_one :
  (o : Ordinal.{u_5}) →
    (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)) →
      (ho : o + 1 ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) (o + 1) ho)
⊢ motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)
have limit₁ : (o : Ordinal.{u_5}) →
  (ho' : IsSuccLimit o) →
    (IH :
        (o' : Ordinal.{u_5}) →
          o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o' ho)) →
      (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_5}) ↦ x ∈ Iio l) o ho)
Tactic: induction o using limitRecOn with
  | zero => exact zero
  | add_one o IH =>
    have ho' : o < l := (lt_succ o).trans ho
    exact succ ⟨o, ho'⟩ (IH ho')
  | limit o ho' IH => exact limit _ ho' fun a ha ↦ IH a.1 ha (ha.trans (c := l) ho)
Cleared hypotheses: o, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
l : Ordinal.{u_4}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_4 + 1)) → Sort u_5
H₁ : motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) 0 ⋯)
H₂ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (succ (↑o : Ordinal.{u_4})) ⋯)
H₃ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_4}) → ((o' : (↑(Iio l) : Type (u_4 + 1))) → o' < o → motive o') → motive o
⊢ boundedLimitRecOn lLim (motive := motive) (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) 0 ⋯) H₁ H₂ H₃ = H₁
have rw : (Subtype.casesOn (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (motive := fun (x : (↑(Iio l) : Type (u_4 + 1))) ↦ motive x)
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) 0 sorry) fun (o : Ordinal.{u_4}) (ho : o ∈ Iio l) ↦
    limitRecOn (motive := fun (o : Ordinal.{u_4}) ↦
      (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho)) o
      (fun (ho : 0 ∈ Iio l) ↦ H₁)
      (fun (o : Ordinal.{u_4})
          (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho))
          (ho : o + 1 ∈ Iio l) ↦
        have ho' := sorry;
        H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho') (IH ho'))
      (fun (o : Ordinal.{u_4}) (ho' : IsSuccLimit o)
          (IH :
            (o' : Ordinal.{u_4}) →
              o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o' ho))
          (ho : o ∈ Iio l) ↦
        H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ho'
          fun (a : (↑(Iio l) : Type (u_4 + 1))) (ha : a < Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ↦
          IH (↑a : Ordinal.{u_4}) ha sorry)
      ho) =
  H₁
Tactic: rw [boundedLimitRecOn]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
l : Ordinal.{u_4}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_4 + 1)) → Sort u_5
H₁ : motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) 0 ⋯)
H₂ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (succ (↑o : Ordinal.{u_4})) ⋯)
H₃ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_4}) → ((o' : (↑(Iio l) : Type (u_4 + 1))) → o' < o → motive o') → motive o
⊢ limitRecOn (motive := fun (o : Ordinal.{u_4}) ↦
      (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho)) 0
      (fun (ho : 0 ∈ Iio l) ↦ H₁)
      (fun (o : Ordinal.{u_4})
          (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho))
          (ho : o + 1 ∈ Iio l) ↦
        H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ⋯) (IH ⋯))
      (fun (o : Ordinal.{u_4}) (ho' : IsSuccLimit o)
          (IH :
            (o' : Ordinal.{u_4}) →
              o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o' ho))
          (ho : o ∈ Iio l) ↦
        H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ho'
          fun (a : (↑(Iio l) : Type (u_4 + 1))) (ha : a < Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ↦
          IH (↑a : Ordinal.{u_4}) ha ⋯)
      ⋯ =
    H₁
have rw : H₁ = H₁
Tactic: rw [limitRecOn_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
l : Ordinal.{u_4}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_4 + 1)) → Sort u_5
o : (↑(Iio l) : Type (u_4 + 1))
H₁ : motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) 0 ⋯)
H₂ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (succ (↑o : Ordinal.{u_4})) ⋯)
H₃ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_4}) → ((o' : (↑(Iio l) : Type (u_4 + 1))) → o' < o → motive o') → motive o
⊢ boundedLimitRecOn lLim (motive := motive)
      (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (succ (↑o : Ordinal.{u_4})) ⋯) H₁ H₂ H₃ =
    H₂ o (boundedLimitRecOn lLim (motive := motive) o H₁ H₂ H₃)
have rw : (Subtype.casesOn (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (motive := fun (x : (↑(Iio l) : Type (u_4 + 1))) ↦ motive x)
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (succ (↑o : Ordinal.{u_4})) sorry)
    fun (o : Ordinal.{u_4}) (ho : o ∈ Iio l) ↦
    limitRecOn (motive := fun (o : Ordinal.{u_4}) ↦
      (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho)) o
      (fun (ho : 0 ∈ Iio l) ↦ H₁)
      (fun (o : Ordinal.{u_4})
          (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho))
          (ho : o + 1 ∈ Iio l) ↦
        have ho' := sorry;
        H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho') (IH ho'))
      (fun (o : Ordinal.{u_4}) (ho' : IsSuccLimit o)
          (IH :
            (o' : Ordinal.{u_4}) →
              o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o' ho))
          (ho : o ∈ Iio l) ↦
        H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ho'
          fun (a : (↑(Iio l) : Type (u_4 + 1))) (ha : a < Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ↦
          IH (↑a : Ordinal.{u_4}) ha sorry)
      ho) =
  H₂ o (boundedLimitRecOn lLim (motive := motive) o H₁ H₂ H₃)
Tactic: rw [boundedLimitRecOn]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
l : Ordinal.{u_4}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_4 + 1)) → Sort u_5
o : (↑(Iio l) : Type (u_4 + 1))
H₁ : motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) 0 ⋯)
H₂ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (succ (↑o : Ordinal.{u_4})) ⋯)
H₃ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_4}) → ((o' : (↑(Iio l) : Type (u_4 + 1))) → o' < o → motive o') → motive o
⊢ limitRecOn (motive := fun (o : Ordinal.{u_4}) ↦
      (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho))
      (succ (↑o : Ordinal.{u_4})) (fun (ho : 0 ∈ Iio l) ↦ H₁)
      (fun (o : Ordinal.{u_4})
          (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho))
          (ho : o + 1 ∈ Iio l) ↦
        H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ⋯) (IH ⋯))
      (fun (o : Ordinal.{u_4}) (ho' : IsSuccLimit o)
          (IH :
            (o' : Ordinal.{u_4}) →
              o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o' ho))
          (ho : o ∈ Iio l) ↦
        H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ho'
          fun (a : (↑(Iio l) : Type (u_4 + 1))) (ha : a < Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ↦
          IH (↑a : Ordinal.{u_4}) ha ⋯)
      ⋯ =
    H₂ o (boundedLimitRecOn lLim (motive := motive) o H₁ H₂ H₃)
have rw : H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (↑o : Ordinal.{u_4}) sorry)
    (limitRecOn (motive := fun (o : Ordinal.{u_4}) ↦
      (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho)) (↑o : Ordinal.{u_4})
      (fun (ho : 0 ∈ Iio l) ↦ H₁)
      (fun (o : Ordinal.{u_4})
          (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho))
          (ho : o + 1 ∈ Iio l) ↦
        H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o sorry) (IH sorry))
      (fun (o : Ordinal.{u_4}) (ho' : IsSuccLimit o)
          (IH :
            (o' : Ordinal.{u_4}) →
              o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o' ho))
          (ho : o ∈ Iio l) ↦
        H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ho'
          fun (a : (↑(Iio l) : Type (u_4 + 1))) (ha : a < Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ↦
          IH (↑a : Ordinal.{u_4}) ha sorry)
      sorry) =
  H₂ o (boundedLimitRecOn lLim (motive := motive) o H₁ H₂ H₃)
Tactic: rw [limitRecOn_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
l : Ordinal.{u_4}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_4 + 1)) → Sort u_5
o : (↑(Iio l) : Type (u_4 + 1))
H₁ : motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) 0 ⋯)
H₂ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (succ (↑o : Ordinal.{u_4})) ⋯)
H₃ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_4}) → ((o' : (↑(Iio l) : Type (u_4 + 1))) → o' < o → motive o') → motive o
oLim : IsSuccLimit (↑o : Ordinal.{u_4})
⊢ boundedLimitRecOn lLim (motive := motive) o H₁ H₂ H₃ =
    H₃ o oLim fun (x : (↑(Iio l) : Type (u_4 + 1))) (x_1 : x < o) ↦ boundedLimitRecOn lLim (motive := motive) x H₁ H₂ H₃
have rw : (Subtype.casesOn (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (motive := fun (x : (↑(Iio l) : Type (u_4 + 1))) ↦ motive x)
    o fun (o : Ordinal.{u_4}) (ho : o ∈ Iio l) ↦
    limitRecOn (motive := fun (o : Ordinal.{u_4}) ↦
      (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho)) o
      (fun (ho : 0 ∈ Iio l) ↦ H₁)
      (fun (o : Ordinal.{u_4})
          (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho))
          (ho : o + 1 ∈ Iio l) ↦
        have ho' := sorry;
        H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho') (IH ho'))
      (fun (o : Ordinal.{u_4}) (ho' : IsSuccLimit o)
          (IH :
            (o' : Ordinal.{u_4}) →
              o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o' ho))
          (ho : o ∈ Iio l) ↦
        H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ho'
          fun (a : (↑(Iio l) : Type (u_4 + 1))) (ha : a < Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ↦
          IH (↑a : Ordinal.{u_4}) ha sorry)
      ho) =
  H₃ o oLim fun (x : (↑(Iio l) : Type (u_4 + 1))) (x_1 : x < o) ↦ boundedLimitRecOn lLim (motive := motive) x H₁ H₂ H₃
Tactic: rw [boundedLimitRecOn]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
l : Ordinal.{u_4}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_4 + 1)) → Sort u_5
o : (↑(Iio l) : Type (u_4 + 1))
H₁ : motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) 0 ⋯)
H₂ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (succ (↑o : Ordinal.{u_4})) ⋯)
H₃ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_4}) → ((o' : (↑(Iio l) : Type (u_4 + 1))) → o' < o → motive o') → motive o
oLim : IsSuccLimit (↑o : Ordinal.{u_4})
⊢ (Subtype.casesOn (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (motive := fun (x : (↑(Iio l) : Type (u_4 + 1))) ↦
      motive x) o fun (o : Ordinal.{u_4}) (ho : o ∈ Iio l) ↦
      limitRecOn (motive := fun (o : Ordinal.{u_4}) ↦
        (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho)) o
        (fun (ho : 0 ∈ Iio l) ↦ H₁)
        (fun (o : Ordinal.{u_4})
            (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho))
            (ho : o + 1 ∈ Iio l) ↦
          have ho' := ⋯;
          H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho') (IH ho'))
        (fun (o : Ordinal.{u_4}) (ho' : IsSuccLimit o)
            (IH :
              (o' : Ordinal.{u_4}) →
                o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o' ho))
            (ho : o ∈ Iio l) ↦
          H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ho'
            fun (a : (↑(Iio l) : Type (u_4 + 1)))
              (ha : a < Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ↦
            IH (↑a : Ordinal.{u_4}) ha ⋯)
        ho) =
    H₃ o oLim fun (x : (↑(Iio l) : Type (u_4 + 1))) (x_1 : x < o) ↦ boundedLimitRecOn lLim (motive := motive) x H₁ H₂ H₃
have dsimp : limitRecOn (motive := fun (o : Ordinal.{u_4}) ↦
    (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho)) (↑o : Ordinal.{u_4})
    (fun (ho : 0 ∈ Iio l) ↦ H₁)
    (fun (o : Ordinal.{u_4})
        (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho))
        (ho : o + 1 ∈ Iio l) ↦
      H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o sorry) (IH sorry))
    (fun (o : Ordinal.{u_4}) (ho' : IsSuccLimit o)
        (IH :
          (o' : Ordinal.{u_4}) →
            o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o' ho))
        (ho : o ∈ Iio l) ↦
      H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ho'
        fun (a : (↑(Iio l) : Type (u_4 + 1))) (ha : a < Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ↦
        IH (↑a : Ordinal.{u_4}) ha sorry)
    sorry =
  H₃ o oLim fun (x : (↑(Iio l) : Type (u_4 + 1))) (x_1 : x < o) ↦ boundedLimitRecOn lLim (motive := motive) x H₁ H₂ H₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ∃ (y : α), r x y
have h₁ : r x
  ((enum r : (a : (↑(Iio (type r)) : Type (u_4 + 1))) → α)
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
        (succ
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
            x))
        sorry :
      { x : Ordinal.{u_4} // x ∈ Iio (type r) }))
Tactic: use enum r ⟨succ (typein r x), h _ (typein_lt_type r x)⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ r x
    ((enum r : (a : (↑(Iio (type r)) : Type (u_4 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
              x))
          ⋯ :
        { x : Ordinal.{u_4} // x ∈ Iio (type r) }))
have h₁ : x =
  (enum r : (a : (↑(Iio (type r)) : Type (u_4 + 1))) → α)
    (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x)
        sorry :
      { x : Ordinal.{u_4} // x ∈ Iio (type r) })
Tactic: convert! enum_lt_enum.mpr _
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
h₁ :
  x =
    (enum r : (a : (↑(Iio (type r)) : Type (u_4 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
            x)
          ⋯ :
        { x : Ordinal.{u_4} // x ∈ Iio (type r) })
⊢ r x
    ((enum r : (a : (↑(Iio (type r)) : Type (u_4 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
              x))
          ⋯ :
        { x : Ordinal.{u_4} // x ∈ Iio (type r) }))
have h₂ : (↑(Iio (type r)) : Type (u_4 + 1))
Tactic: convert! enum_lt_enum.mpr _
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
h₁ :
  x =
    (enum r : (a : (↑(Iio (type r)) : Type (u_4 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
            x)
          ⋯ :
        { x : Ordinal.{u_4} // x ∈ Iio (type r) })
h₂ : (↑(Iio (type r)) : Type (u_4 + 1))
⊢ r x
    ((enum r : (a : (↑(Iio (type r)) : Type (u_4 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
          (succ
            (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
              x))
          ⋯ :
        { x : Ordinal.{u_4} // x ∈ Iio (type r) }))
have h₃ : LT.lt (α := (↑(Iio (type r)) : Type (u_4 + 1)))
  (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x)
      sorry :
    { x : Ordinal.{u_4} // x ∈ Iio (type r) })
  (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
      (succ
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4}) x))
      sorry :
    { x : Ordinal.{u_4} // x ∈ Iio (type r) })
Tactic: convert! enum_lt_enum.mpr _
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ x =
    (enum r : (a : (↑(Iio (type r)) : Type (u_4 + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type r))
          (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_4}) ↦ x1 < x2) : (a : α) → Ordinal.{u_4})
            x)
          ⋯ :
        { x : Ordinal.{u_4} // x ∈ Iio (type r) })
have h₁ : x = x
Tactic: rw [enum_typein]