awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
⊢ Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    (lift.{max (u + 1) v, max (u + 1) v} (type s))
have mpr : ∀ (f : PrincipalSeg s fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2),
  Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    (lift.{max (u + 1) v, max (u + 1) v} (type s))
Tactic: obtain ⟨f⟩ := lift_type_lt.{_,_,v}.1 h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
f : PrincipalSeg s fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
⊢ Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    (lift.{max (u + 1) v, max (u + 1) v} (type s))
have mpr : ∀ (f : s ↪r fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (a : Ordinal.{u})
  (hf :
    ∀ (b : Ordinal.{u}),
      Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < a),
  Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    (lift.{max (u + 1) v, max (u + 1) v} (type s))
Tactic: obtain ⟨f, a, hf⟩ := f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
f : s ↪r fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
a : Ordinal.{u}
hf :
  ∀ (b : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < a
⊢ Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    (lift.{max (u + 1) v, max (u + 1) v} (type s))
have mpr : (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
        fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
      (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
    a =
  lift.{max (u + 1) v, max (u + 1) v} (type s)
Tactic: exists a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
f : s ↪r fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
a : Ordinal.{u}
hf :
  ∀ (b : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < a
⊢ (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      a =
    lift.{max (u + 1) v, max (u + 1) v} (type s)
have mpr : ∀ (α : Type u) (r : α → α → Prop) [inst_1 : IsWellOrder α r]
  (hf :
    ∀ (b : Ordinal.{u}),
      Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < type r),
  (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      (type r) =
    lift.{max (u + 1) v, max (u + 1) v} (type s)
Tactic: induction a using inductionOn with | type α r
Cleared hypotheses: a, hf
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
f : s ↪r fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
α : Type u
r : α → α → Prop
inst_1 : IsWellOrder α r
hf :
  ∀ (b : Ordinal.{u}),
    Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < type r
⊢ (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      (type r) =
    lift.{max (u + 1) v, max (u + 1) v} (type s)
have mpr : β → α
Tactic: refine lift_type_eq.{u, max (u + 1) v, max (u + 1) v}.2
        ⟨(RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ ?_) ?_).symm⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
f : s ↪r fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
α : Type u
r : α → α → Prop
inst_1 : IsWellOrder α r
hf :
  ∀ (b : Ordinal.{u}),
    Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < type r
mpr : β → α
⊢ (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      (type r) =
    lift.{max (u + 1) v, max (u + 1) v} (type s)
have mpr₁ : ∀ (a b : β),
  s a b →
    r
      ((enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) a) sorry :
          { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
      ((enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) sorry :
          { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
Tactic: refine lift_type_eq.{u, max (u + 1) v, max (u + 1) v}.2
        ⟨(RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ ?_) ?_).symm⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
f : s ↪r fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
α : Type u
r : α → α → Prop
inst_1 : IsWellOrder α r
hf :
  ∀ (b : Ordinal.{u}),
    Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < type r
mpr : β → α
mpr₁ :
  ∀ (a b : β),
    s a b →
      r
        ((enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) a) ⋯ :
            { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
        ((enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) ⋯ :
            { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
⊢ (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      (type r) =
    lift.{max (u + 1) v, max (u + 1) v} (type s)
have mpr₂ : Function.Surjective (α := β) (β := α)
  (⇑(RelEmbedding.ofMonotone (r := s) (s := r)
        (fun (b : β) ↦
          (enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) sorry :
              { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
        sorry) :
    (a : β) → α)
Tactic: refine lift_type_eq.{u, max (u + 1) v, max (u + 1) v}.2
        ⟨(RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ ?_) ?_).symm⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
f : s ↪r fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
α : Type u
r : α → α → Prop
inst_1 : IsWellOrder α r
hf :
  ∀ (b : Ordinal.{u}),
    Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < type r
⊢ ∀ (a b : β),
    s a b →
      r
        ((enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) a) ⋯ :
            { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
        ((enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) ⋯ :
            { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
have mpr : ∀ (a b : β) (h : s a b),
  LT.lt (α := Ordinal.{u})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
        ((enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) a) sorry :
              { x : Ordinal.{u} // x ∈ Set.Iio (type r) }) :
          α) :
      Ordinal.{u})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
        ((enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) sorry :
              { x : Ordinal.{u} // x ∈ Set.Iio (type r) }) :
          α) :
      Ordinal.{u})
Tactic: refine fun a b h => (typein_lt_typein r).1 ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b_1 : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h_1 :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
f : s ↪r fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
α : Type u
r : α → α → Prop
inst_1 : IsWellOrder α r
hf :
  ∀ (b : Ordinal.{u}),
    Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < type r
a b : β
h : s a b
⊢ LT.lt (α := Ordinal.{u})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
        ((enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) a) ⋯ :
              { x : Ordinal.{u} // x ∈ Set.Iio (type r) }) :
          α) :
      Ordinal.{u})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
        ((enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) ⋯ :
              { x : Ordinal.{u} // x ∈ Set.Iio (type r) }) :
          α) :
      Ordinal.{u})
have mpr : LT.lt.{u + 1} (α := Ordinal.{u}) ((f : (a : β) → Ordinal.{u}) a : Ordinal.{u})
  ((f : (a : β) → Ordinal.{u}) b : Ordinal.{u})
Tactic: rw [typein_enum, typein_enum]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
f : s ↪r fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
α : Type u
r : α → α → Prop
inst_1 : IsWellOrder α r
hf :
  ∀ (b : Ordinal.{u}),
    Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < type r
a' : α
⊢ ∃ (a : β),
    (RelEmbedding.ofMonotone (r := s) (s := r)
            (fun (b : β) ↦
              (enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
                (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) ⋯ :
                  { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
            ⋯ :
          (a : β) → α)
        a =
      a'
have mpr : ∀ (b : β)
  (e :
    Eq.{u + 2} (α := Ordinal.{u}) ((f : (a : β) → Ordinal.{u}) b : Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a' :
        Ordinal.{u})),
  ∃ (a : β),
    (RelEmbedding.ofMonotone (r := s) (s := r)
            (fun (b : β) ↦
              (enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
                (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) sorry :
                  { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
            sorry :
          (a : β) → α)
        a =
      a'
Tactic: obtain ⟨b, e⟩ := (hf _).2 (typein_lt_type _ a')
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b_1 : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
f : s ↪r fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
α : Type u
r : α → α → Prop
inst_1 : IsWellOrder α r
hf :
  ∀ (b : Ordinal.{u}),
    Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < type r
a' : α
b : β
e :
  Eq.{u + 2} (α := Ordinal.{u}) ((f : (a : β) → Ordinal.{u}) b : Ordinal.{u})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a' :
      Ordinal.{u})
⊢ ∃ (a : β),
    (RelEmbedding.ofMonotone (r := s) (s := r)
            (fun (b : β) ↦
              (enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
                (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) ⋯ :
                  { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
            ⋯ :
          (a : β) → α)
        a =
      a'
have mpr : (RelEmbedding.ofMonotone (r := s) (s := r)
        (fun (b : β) ↦
          (enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) sorry :
              { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
        sorry :
      (a : β) → α)
    b =
  a'
Tactic: exists b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b_1 : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
f : s ↪r fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
α : Type u
r : α → α → Prop
inst_1 : IsWellOrder α r
hf :
  ∀ (b : Ordinal.{u}),
    Membership.mem (γ := Set Ordinal.{u}) (Set.range (ι := β) (⇑f : (a : β) → Ordinal.{u})) b ↔ b < type r
a' : α
b : β
e :
  Eq.{u + 2} (α := Ordinal.{u}) ((f : (a : β) → Ordinal.{u}) b : Ordinal.{u})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a' :
      Ordinal.{u})
⊢ (RelEmbedding.ofMonotone (r := s) (s := r)
          (fun (b : β) ↦
            (enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) ⋯ :
                { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
          ⋯ :
        (a : β) → α)
      b =
    a'
have mpr : (enum r : (a : (↑(Set.Iio (type r)) : Type (u + 1))) → α)
    (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio (type r)) ((f : (a : β) → Ordinal.{u}) b) sorry :
      { x : Ordinal.{u} // x ∈ Set.Iio (type r) }) =
  a'
Tactic: simp only [RelEmbedding.ofMonotone_coe]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (hypothesis)
Goal:
c : Cardinal.{u}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}
have this : lift.{max (u + 1) v, u + 1} (lift.{u + 1, u} c) < lift.{max (u + 1) v, u + 1} univ.{u, u + 1}
Tactic: have := lift_lt.{_, max (u + 1) v}.2 (lift_lt_univ c)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
⊢ univ.{u, v}.ord = Ordinal.univ.{u, v}
have refine : ∀ (o : Ordinal.{max (u + 1) v}) (h : o < Ordinal.univ.{u, v}), o.card < univ.{u, v}
Tactic: refine le_antisymm (ord_card_le _) <| le_of_forall_lt fun o h => lt_ord.2 ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (hypothesis)
Goal:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ o.card < univ.{u, v}
have this : Membership.mem (γ := Set Ordinal.{max (u + 1) v})
  (Set.range (ι := Ordinal.{u})
    (⇑(Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (u + 1) v}) ↦ x1 < x2)) :
      (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
  o
Tactic: have := Ordinal.liftPrincipalSeg.mem_range_of_rel_top (by simpa using h)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
this :
  Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (u + 1) v}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    o
⊢ o.card < univ.{u, v}
have rcases : ∀ (o_1 : Ordinal.{u})
  (h' :
    (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (u + 1) v}) ↦ x1 < x2) :
          (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
        o_1 =
      o),
  o.card < univ.{u, v}
Tactic: rcases this with ⟨o, h'⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
o_1 : Ordinal.{max (u + 1) v}
h : o_1 < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' :
  (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (u + 1) v}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      o =
    o_1
⊢ o_1.card < univ.{u, v}
have rw : lift.{max (u + 1) v, u} o.card < univ.{u, v}
Tactic: rw [← h', Ordinal.liftPrincipalSeg_coe, ← Ordinal.lift_card]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (hypothesis)
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
⊢ ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'
have this : c.ord < univ.{u, u + 1}.ord
Tactic: have := ord_lt_ord.2 h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (hypothesis)
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < univ.{u, u + 1}.ord
⊢ ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'
have this₁ : c.ord < Ordinal.univ.{u, u + 1}
Tactic: rw [ord_univ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
⊢ ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'
have obtain : ∀ (o : Ordinal.{u})
  (e :
    (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) :
          (a : Ordinal.{u}) → Ordinal.{u + 1})
        o =
      c.ord),
  ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'
Tactic: obtain ⟨o, e⟩ := Ordinal.liftPrincipalSeg.mem_range_of_rel_top (by simpa)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (hypothesis)
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e :
  (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    c.ord
⊢ ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'
have this₁ : c.ord.card = c
Tactic: have := card_ord c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (hypothesis)
Goal:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this_1 : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e :
  (Ordinal.liftPrincipalSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o =
    c.ord
this : c.ord.card = c
⊢ ∃ (c' : Cardinal.{u}), c = lift.{u + 1, u} c'
have this₁ : lift.{u + 1, u} o.card = c
Tactic: rw [← e, Ordinal.liftPrincipalSeg_coe, ← Ordinal.lift_card] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
⊢ ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'
have let : ∀ (a : Cardinal.{u + 1}) (h' : a < #Ordinal.{u}) (e : lift.{v, u + 1} a = c),
  ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'
Tactic: let ⟨a, h', e⟩ := lt_lift_iff.1 h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (hypothesis)
Goal:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < #Ordinal.{u}
e : lift.{v, u + 1} a = c
⊢ ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'
have h'₁ : a < univ.{u, u + 1}
Tactic: rw [mk_ordinal] at h'
Cleared hypotheses: h', e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < univ.{u, u + 1}
e : lift.{v, u + 1} a = c
⊢ ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'
have rcases : ∀ (c' : Cardinal.{u}) (h' : lift.{u + 1, u} c' < univ.{u, u + 1}) (e : lift.{v, u + 1} (lift.{u + 1, u} c') = c),
  ∃ (c' : Cardinal.{u}), c = lift.{max (u + 1) v, u} c'
Tactic: rcases lt_univ.{u}.1 h' with ⟨c', rfl⟩
Cleared hypotheses: a, h', e
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
α : Type u
⊢ Small.{v, u} α ↔ lift.{v + 1, u} #α < univ.{v, max u (v + 1)}
have rw : Small.{v, u} α ↔ ∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
Tactic: rw [lt_univ']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
α : Type u
⊢ Small.{v, u} α ↔ ∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
have mp : Small.{v, u} α → ∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
α : Type u
mp : Small.{v, u} α → ∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
⊢ Small.{v, u} α ↔ ∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
have mpr : (∃ (c' : Cardinal.{v}), lift.{v + 1, u} #α = lift.{max u (v + 1), v} c') → Small.{v, u} α
Tactic: constructor