awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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)
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)
⊢ 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)
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
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 ⋯) 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₁
⊢ boundedLimitRecOn lLim (motive := motive) (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) 0 ⋯) H₁ H₂ H₃ = H₁

Tactic:
rw [boundedLimitRecOn]
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
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)) 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₁
⊢ (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 ⋯) 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₁

Tactic:
dsimp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
rw rw₁ : H₁ = H₁
⊢ 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₁

Tactic:
rw [limitRecOn_zero]

Premises used: Ordinal.limitRecOn_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
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})) ⋯)
      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 (boundedLimitRecOn lLim (motive := motive) o H₁ H₂ H₃)
⊢ 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₃)

Tactic:
rw [boundedLimitRecOn]
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
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))
      (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₃)
⊢ (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})) ⋯)
      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 (boundedLimitRecOn lLim (motive := motive) o H₁ H₂ H₃)

Tactic:
dsimp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
rw :
  H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (↑o : Ordinal.{u_4}) ⋯)
      (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 ⋯) (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₃)
⊢ 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₃)

Tactic:
rw [limitRecOn_succ]

Premises used: Ordinal.limitRecOn_succ
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
⊢ H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (↑o : Ordinal.{u_4}) ⋯)
      (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 ⋯) (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₃)

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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})
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' := ⋯;
          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₃
⊢ 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₃

Tactic:
rw [boundedLimitRecOn]
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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})
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 ⋯) (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 oLim fun (x : (↑(Iio l) : Type (u_4 + 1))) (x_1 : x < o) ↦ boundedLimitRecOn lLim (motive := motive) x H₁ H₂ H₃
⊢ (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₃

Tactic:
dsimp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
⊢ Eq (α := (succ o).ToType)
    ((enum fun (x1 x2 : (succ o).ToType) ↦ x1 < x2 :
          (a : (↑(Iio (type fun (x1 x2 : (succ o).ToType) ↦ x1 < x2)) : Type (u_4 + 1))) → (succ o).ToType)
        (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio (type fun (x1 x2 : (succ o).ToType) ↦ x1 < x2)) o ⋯) :
      (succ o).ToType)
    (⊤ : (succ o).ToType)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
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))
          ⋯ :
        { x : Ordinal.{u_4} // x ∈ Iio (type r) }))
⊢ ∃ (y : α), r x y

Tactic:
use enum r ⟨succ (typein r x), h _ (typein_lt_type r x)⟩

Premises used: Order.succ, PrincipalSeg.toRelEmbedding, Ordinal.typein_lt_type, Subtype.mk, Ordinal.enum, DFunLike.coe, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ r
    ((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) }))
    ((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) }))

Tactic:
enum_lt_enum.mpr _

Premises used: Iff.mpr, Ordinal.enum_lt_enum