awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ Eq (α := β)
    ((f : (a : α) → β)
        ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) (type t) ⋯) :
          α) :
      β)
    ((enum s : (a : (↑(Iio (type s)) : Type (u + 1))) → β)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type s)) (type t) ⋯) :
      β)
have rw : (f : (a : α) → β) (g.top (r := t) (s := r)) = (g.transRelIso (r := t) (s := r) (t := s) f).top (r := t) (s := s)
Tactic: rw [enum_type g, enum_type (g.transRelIso f)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u}
⊢ Small.{u, u + 1} (↑(Iic o) : Type (u + 1))
have rw : Small.{u, u + 1} (↑(Iio o ∪ {o}) : Type (u + 1))
Tactic: rw [← Iio_union_right]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_1}
ho : 0 < o
⊢ 0 ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)
have rwa : 0 ∈ Iio o
Tactic: rwa [type_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≼i s
a : α
⊢ Eq (α := Ordinal.{u_1})
    (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : β) → Ordinal.{u_1})
        ((f : (a : α) → β) a : β) :
      Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
have rw : Eq (α := Ordinal.{u_1})
  (((f.transPrincipal (r := r) (s := s) (t := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) (typein s)).toRelEmbedding (r := r)
          (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) :
        (a : α) → Ordinal.{u_1})
      a :
    Ordinal.{u_1})
  (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
    Ordinal.{u_1})
Tactic: rw [← f.transPrincipal_apply _ a, (f.transPrincipal _).eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≼i s
a : α
rw :
  Eq (α := Ordinal.{u_1})
    (((f.transPrincipal (r := r) (s := s) (t := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) (typein s)).toRelEmbedding (r :=
            r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) :
          (a : α) → Ordinal.{u_1})
        a :
      Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
⊢ Eq (α := Ordinal.{u_1})
    (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : β) → Ordinal.{u_1})
        ((f : (a : α) → β) a : β) :
      Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
have rw₁ : Eq (α := Ordinal.{u_1})
  (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
    Ordinal.{u_1})
  (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
    Ordinal.{u_1})
Tactic: rw [← f.transPrincipal_apply _ a, (f.transPrincipal _).eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≼i s
a : α
rw :
  Eq (α := Ordinal.{u_1})
    (((f.transPrincipal (r := r) (s := s) (t := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) (typein s)).toRelEmbedding (r :=
            r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) :
          (a : α) → Ordinal.{u_1})
        a :
      Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
rw₁ :
  Eq (α := Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
⊢ Eq (α := Ordinal.{u_1})
    (((typein s).toRelEmbedding (r := s) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : β) → Ordinal.{u_1})
        ((f : (a : α) → β) a : β) :
      Ordinal.{u_1})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2) : (a : α) → Ordinal.{u_1}) a :
      Ordinal.{u_1})
have g : r ≺i fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2
Tactic: rw [← f.transPrincipal_apply _ a, (f.transPrincipal _).eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
⊢ (type fun (x1 x2 : o.ToType) ↦ x1 < x2).card = o.card
have rw : o.card = o.card
Tactic: rw [Ordinal.type_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) ↔ Nonempty (r ≼i s)
have mp : lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) → Nonempty (r ≼i s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
mp : lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) → Nonempty (r ≼i s)
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) ↔ Nonempty (r ≼i s)
have mpr : Nonempty (r ≼i s) → lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) → Nonempty (r ≼i s)
have mp : lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) →
  (f :
      InitialSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
        ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
        (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)) →
    r ≼i s
Tactic: refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ Nonempty (r ≼i s) → lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)
have mpr : Nonempty (r ≼i s) →
  (f : r ≼i s) →
    InitialSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
      ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
      (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)
Tactic: refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ lift.{max v w, u} (type r) = lift.{max u w, v} (type s) ↔ Nonempty (r ≃r s)
have refine_1 : (isEquivalent : WellOrder → WellOrder → Prop)
    { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
      r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := sorry : WellOrder }
    { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
      r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := sorry } →
  Nonempty (r ≃r s)
Tactic: refine Quotient.eq'.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
refine_1 :
  (isEquivalent : WellOrder → WellOrder → Prop)
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := ⋯ : WellOrder }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := ⋯ } →
    Nonempty (r ≃r s)
⊢ lift.{max v w, u} (type r) = lift.{max u w, v} (type s) ↔ Nonempty (r ≃r s)
have refine_2 : Nonempty (r ≃r s) →
  (isEquivalent : WellOrder → WellOrder → Prop)
    { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
      r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := sorry : WellOrder }
    { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
      r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := sorry }
Tactic: refine Quotient.eq'.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ (isEquivalent : WellOrder → WellOrder → Prop)
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := ⋯ : WellOrder }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := ⋯ } →
    Nonempty (r ≃r s)
have refine_1 : (isEquivalent : WellOrder → WellOrder → Prop)
    { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
      r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := sorry : WellOrder }
    { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
      r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := sorry } →
  (f :
      RelIso (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
        ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
        (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)) →
    r ≃r s
Tactic: refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ Nonempty (r ≃r s) →
    (isEquivalent : WellOrder → WellOrder → Prop)
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst : WellOrder.{u} }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst : WellOrder.{u} }.r, wo := ⋯ : WellOrder }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r, wo := ⋯ }
have refine_2 : Nonempty (r ≃r s) →
  (f : r ≃r s) →
    RelIso (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
      ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
      (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)
Tactic: refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) ↔ Nonempty (r ≺i s)
have mp : lift.{max v w, u} (type r) < lift.{max u w, v} (type s) → Nonempty (r ≺i s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
mp : lift.{max v w, u} (type r) < lift.{max u w, v} (type s) → Nonempty (r ≺i s)
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) ↔ Nonempty (r ≺i s)
have mpr : Nonempty (r ≺i s) → lift.{max v w, u} (type r) < lift.{max u w, v} (type s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) → Nonempty (r ≺i s)
have mp : lift.{max v w, u} (type r) < lift.{max u w, v} (type s) →
  (f :
      PrincipalSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
        ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
        (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)) →
    r ≺i s
Tactic: refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
⊢ Nonempty (r ≺i s) → lift.{max v w, u} (type r) < lift.{max u w, v} (type s)
have mpr : Nonempty (r ≺i s) →
  (f : r ≺i s) →
    PrincipalSeg (α := ULift.{max v w, u} { α := α, r := r, wo := inst }.α) (β :=
      ULift.{max u w, v} { α := β, r := s, wo := inst_1 }.α) (ULift.down ⁻¹'o { α := α, r := r, wo := inst }.r)
      (ULift.down ⁻¹'o { α := β, r := s, wo := inst_1 }.r)
Tactic: refine fun ⟨f⟩ ↦ ⟨?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a b : Ordinal.{v}
α : Type v
r : α → α → Prop
h : IsWellOrder α r
β : Type v
s : β → β → Prop
h_1 : IsWellOrder β s
⊢ lift.{u, v} (type r) ≤ lift.{u, v} (type s) ↔ type r ≤ type s
have rw : lift.{max v u, v} (type r) ≤ lift.{max v u, v} (type s) ↔ type r ≤ type s
Tactic: rw [← lift_umax]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a b : Ordinal.{v}
⊢ lift.{u, v} a = lift.{u, v} b ↔ a = b
have simp_rw : lift.{u, v} a ≤ lift.{u, v} b ∧ lift.{u, v} b ≤ lift.{u, v} a ↔ a ≤ b ∧ b ≤ a
Tactic: simp_rw [le_antisymm_iff, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a b : Ordinal.{v}
⊢ lift.{u, v} a < lift.{u, v} b ↔ a < b
have simp_rw : lift.{u, v} a ≤ lift.{u, v} b ∧ ¬lift.{u, v} b ≤ lift.{u, v} a ↔ a ≤ b ∧ ¬b ≤ a
Tactic: simp_rw [lt_iff_le_not_ge, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u}
⊢ (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    lift.{u + 1, u} o
have nth_rw : (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
      (a : Ordinal.{u}) → Ordinal.{u + 1})
    o =
  lift.{u + 1, u} (type fun (x1 x2 : o.ToType) ↦ x1 < x2)
Tactic: nth_rw 2 [← o.type_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u}
⊢ (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    lift.{u + 1, u} (type fun (x1 x2 : o.ToType) ↦ x1 < x2)
have rw : (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
      (a : Ordinal.{u}) → Ordinal.{u + 1})
    o =
  lift.{u, u + 1} (type fun (x1 x2 : (↑(Iio o) : Type (u + 1))) ↦ x1 < x2)
Tactic: rw [← ToType.mk.toRelIsoLT.ordinal_lift_type_eq, lift_id'.{u, u + 1}, type_Iio_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u}
rw :
  (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    lift.{u, u + 1} (type fun (x1 x2 : (↑(Iio o) : Type (u + 1))) ↦ x1 < x2)
⊢ (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    lift.{u + 1, u} (type fun (x1 x2 : o.ToType) ↦ x1 < x2)
have rw₁ : (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
      (a : Ordinal.{u}) → Ordinal.{u + 1})
    o =
  type fun (x1 x2 : (↑(Iio o) : Type (u + 1))) ↦ x1 < x2
Tactic: rw [← ToType.mk.toRelIsoLT.ordinal_lift_type_eq, lift_id'.{u, u + 1}, type_Iio_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u}
rw :
  (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    lift.{u, u + 1} (type fun (x1 x2 : (↑(Iio o) : Type (u + 1))) ↦ x1 < x2)
rw₁ :
  (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    type fun (x1 x2 : (↑(Iio o) : Type (u + 1))) ↦ x1 < x2
⊢ (PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    lift.{u + 1, u} (type fun (x1 x2 : o.ToType) ↦ x1 < x2)
have rw₂ : Eq (α := Ordinal.{u + 1})
  ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o :
    Ordinal.{u + 1})
  ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o :
    Ordinal.{u + 1})
Tactic: rw [← ToType.mk.toRelIsoLT.ordinal_lift_type_eq, lift_id'.{u, u + 1}, type_Iio_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ (fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) ≼i fun (x1 x2 : Ordinal.{max u v}) ↦ x1 < x2
have refine : ∀ (a : Ordinal.{v}) (b : Ordinal.{max u v}) (α : Type v) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type (max u v))
  (s : β → β → Prop) (x_1 : IsWellOrder β s)
  (h :
    type s <
      (RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦
            x1 < x2) lift.{u, v} liftInitialSeg._proof_1 :
          (a : Ordinal.{v}) → Ordinal.{max u v})
        (type r)),
  Membership.mem (γ := Set Ordinal.{max u v})
    (range (ι := Ordinal.{v})
      (⇑(RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦
            x1 < x2) lift.{u, v} liftInitialSeg._proof_1) :
        (a : Ordinal.{v}) → Ordinal.{max u v}))
    (type s)
Tactic: refine ⟨RelEmbedding.ofMonotone lift.{u} (by simp),
    fun a b ↦ Ordinal.inductionOn₂ a b fun α r _ β s _ h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (hypothesis)
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
h_2 : IsWellOrder β s
h :
  type s <
    (RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦ x1 < x2)
          lift.{u, v} liftInitialSeg._proof_1 :
        (a : Ordinal.{v}) → Ordinal.{max u v})
      (type r)
⊢ Membership.mem (γ := Set Ordinal.{max u v})
    (range (ι := Ordinal.{v})
      (⇑(RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦
            x1 < x2) lift.{u, v} liftInitialSeg._proof_1) :
        (a : Ordinal.{v}) → Ordinal.{max u v}))
    (type s)
have h₁ : Nonempty (s ≺i r)
Tactic: rw [RelEmbedding.ofMonotone_coe, ← lift_id'.{max u v} (type s),
    ← lift_umax.{v, u}, lift_type_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
h_2 : IsWellOrder β s
h : Nonempty (s ≺i r)
⊢ Membership.mem (γ := Set Ordinal.{max u v})
    (range (ι := Ordinal.{v})
      (⇑(RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦
            x1 < x2) lift.{u, v} liftInitialSeg._proof_1) :
        (a : Ordinal.{v}) → Ordinal.{max u v}))
    (type s)
have obtain : ∀ (f : s ≺i r),
  Membership.mem (γ := Set Ordinal.{max u v})
    (range (ι := Ordinal.{v})
      (⇑(RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦
            x1 < x2) lift.{u, v} liftInitialSeg._proof_1) :
        (a : Ordinal.{v}) → Ordinal.{max u v}))
    (type s)
Tactic: obtain ⟨f⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
h : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
h_1 : IsWellOrder β s
f : s ≺i r
⊢ Membership.mem (γ := Set Ordinal.{max u v})
    (range (ι := Ordinal.{v})
      (⇑(RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦
            x1 < x2) lift.{u, v} liftInitialSeg._proof_1) :
        (a : Ordinal.{v}) → Ordinal.{max u v}))
    (type s)
have h : (RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦ x1 < x2)
        lift.{u, v} liftInitialSeg._proof_1 :
      (a : Ordinal.{v}) → Ordinal.{max u v})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) : (a : α) → Ordinal.{v})
      (f.top (r := s) (s := r))) =
  type s
Tactic: use typein r f.top
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
h : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
h_1 : IsWellOrder β s
f : s ≺i r
⊢ (RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦ x1 < x2)
          lift.{u, v} liftInitialSeg._proof_1 :
        (a : Ordinal.{v}) → Ordinal.{max u v})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) : (a : α) → Ordinal.{v})
        (f.top (r := s) (s := r))) =
    type s
have h : lift.{u, v}
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) : (a : α) → Ordinal.{v})
      (f.top (r := s) (s := r))) =
  type s
Tactic: rw [RelEmbedding.ofMonotone_coe, ← lift_umax, lift_typein_top, lift_id']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r_1 : α_1 → α_1 → Prop
s_1 : β_1 → β_1 → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
h_1 : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
h_2 : IsWellOrder β s
f : s ≺i r
h :
  lift.{u, v}
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) : (a : α) → Ordinal.{v})
        (f.top (r := s) (s := r))) =
    type s
⊢ (RelEmbedding.ofMonotone (r := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max u v}) ↦ x1 < x2)
          lift.{u, v} liftInitialSeg._proof_1 :
        (a : Ordinal.{v}) → Ordinal.{max u v})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) : (a : α) → Ordinal.{v})
        (f.top (r := s) (s := r))) =
    type s
have h₁ : lift.{max v u, v}
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{v}) ↦ x1 < x2) : (a : α) → Ordinal.{v})
      (f.top (r := s) (s := r))) =
  type s
Tactic: rw [RelEmbedding.ofMonotone_coe, ← lift_umax, lift_typein_top, lift_id']