awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Univ
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)
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))
⊢ 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
-- Module: Mathlib.SetTheory.Ordinal.Univ
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
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))
⊢ 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
-- Module: Mathlib.SetTheory.Ordinal.Univ
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
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)
⊢ 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:
exists a
-- Module: Mathlib.SetTheory.Ordinal.Univ
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
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)
⊢ (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:
induction a using inductionOn with | type α r

Premises used: Ordinal.type
-- Module: Mathlib.SetTheory.Ordinal.Univ
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)

Tactic:
lift_type_eq.{u, max (u + 1) v, max (u + 1) v}.2
        ⟨(RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ ?_) ?_).symm⟩

Premises used: Iff.mpr, Ordinal.lift_type_eq, Ordinal.lift, Ordinal.type, RelIso.symm, Nonempty.intro, RelEmbedding.ofMonotone, RelIso.ofSurjective
-- Module: Mathlib.SetTheory.Ordinal.Univ
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) }))
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) ⋯ :
                { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
          ⋯) :
      (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})
      (type r) =
    lift.{max (u + 1) v, max (u + 1) v} (type s)

Tactic:
refine lift_type_eq.{u, max (u + 1) v, max (u + 1) v}.2
        ⟨(RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ ?_) ?_).symm⟩
-- Module: Mathlib.SetTheory.Ordinal.Univ
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
⊢ β → α

Tactic:
exact fun b => enum r ⟨f b, (hf _).1 ⟨_, rfl⟩⟩

Premises used: Subtype.mk, Exists.intro, Iff.mp, Ordinal.enum, DFunLike.coe, rfl
-- Module: Mathlib.SetTheory.Ordinal.Univ
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) }))

Tactic:
fun a b h => (typein_lt_typein r).1 ?_

Premises used: Ordinal.typein_lt_typein, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Univ
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 :
  ∀ (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})
⊢ ∀ (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) }))

Tactic:
refine fun a b h => (typein_lt_typein r).1 ?_

Premises used: Ordinal.typein_lt_typein, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Univ
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
mpr :
  LT.lt.{u + 1} (α := Ordinal.{u}) ((f : (a : β) → Ordinal.{u}) a : Ordinal.{u})
    ((f : (a : β) → Ordinal.{u}) b : Ordinal.{u})
⊢ 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})

Tactic:
rw [typein_enum, typein_enum]

Premises used: Ordinal.typein_enum
-- Module: Mathlib.SetTheory.Ordinal.Univ
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.{u + 1} (α := Ordinal.{u}) ((f : (a : β) → Ordinal.{u}) a : Ordinal.{u})
    ((f : (a : β) → Ordinal.{u}) b : Ordinal.{u})

Tactic:
f.map_rel_iff.2 h

Premises used: Iff.mpr, RelEmbedding.map_rel_iff
-- Module: Mathlib.SetTheory.Ordinal.Univ
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.{u + 1} (α := Ordinal.{u}) ((f : (a : β) → Ordinal.{u}) a : Ordinal.{u})
    ((f : (a : β) → Ordinal.{u}) b : Ordinal.{u})

Tactic:
exact f.map_rel_iff.2 h

Premises used: Iff.mpr, RelEmbedding.map_rel_iff
-- Module: Mathlib.SetTheory.Ordinal.Univ
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' : α
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) ⋯ :
                    { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
              ⋯ :
            (a : β) → α)
          a =
        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'

Tactic:
obtain ⟨b, e⟩ := (hf _).2 (typein_lt_type _ a')

Premises used: Iff.mpr, Ordinal.typein_lt_type
-- Module: Mathlib.SetTheory.Ordinal.Univ
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})
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) ⋯ :
                { x : Ordinal.{u} // x ∈ Set.Iio (type r) }))
          ⋯ :
        (a : β) → α)
      b =
    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'

Tactic:
exists b
-- Module: Mathlib.SetTheory.Ordinal.Univ
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})
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) ⋯ :
        { x : Ordinal.{u} // x ∈ Set.Iio (type r) }) =
    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 : β) → α)
      b =
    a'

Tactic:
simp only [RelEmbedding.ofMonotone_coe]

Premises used: RelEmbedding.ofMonotone_coe
-- Module: Mathlib.SetTheory.Ordinal.Univ
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})
⊢ (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'

Tactic:
simp [e]
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ (⇑(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}) =
    lift.{max (u + 1) v, u}

Tactic:
rfl

Premises used: Ordinal.lift, rfl
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ liftPrincipalSeg.top (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{max (u + 1) v}) ↦
      x1 < x2) =
    univ.{u, v}

Tactic:
rfl

Premises used: Ordinal.univ, Ordinal.lift, Ordinal.type, rfl
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ liftPrincipalSeg.top (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) =
    type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ univ.{u, v}.card = Cardinal.univ.{u, v}

Tactic:
rfl

Premises used: Cardinal.univ, Quotient.map, Cardinal.lift, Cardinal.map, Quotient, Quot.map, rfl, Ordinal
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ #Ordinal.{u} = univ.{u, u + 1}

Tactic:
(lift_id _).symm

Premises used: Cardinal.univ, Eq.symm, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ univ.{u, u + 1} = #Ordinal.{u}

Tactic:
lift_id _

Premises used: Cardinal.univ, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ lift.{w, max (u + 1) v} univ.{u, v} = univ.{u, max v w}

Tactic:
lift_lift _

Premises used: Cardinal.lift_lift, Cardinal.univ
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ univ.{u, max (u + 1) v} = univ.{u, v}

Tactic:
congr_fun lift_umax _

Premises used: Cardinal.univ, Cardinal.lift_umax, congr_fun
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u}
⊢ lift.{u + 1, u} c < univ.{u, u + 1}

Tactic:
simpa only [Ordinal.liftPrincipalSeg_coe, lift_ord, lift_succ, ord_le, Order.succ_le_iff] using
    le_of_lt (Ordinal.liftPrincipalSeg.{u, u + 1}.lt_top (Order.succ c).ord)

Premises used: Cardinal.lift_succ, Ordinal.liftPrincipalSeg_coe, Cardinal.lift_ord, Cardinal.ord_le, Order.succ_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u}
⊢ 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)
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u + 1} (lift.{u + 1, u} c) < lift.{max (u + 1) v, u + 1} univ.{u, u + 1}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
rw [lift_lift, lift_univ, univ_umax.{u, v}] at this

Premises used: Cardinal.lift_univ, Cardinal.lift_lift
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u} c < univ.{u, v}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
this
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u} c < univ.{u, v}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
exact this
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ ℵ₀ < univ.{u, v}

Tactic:
simpa using lift_lt_univ' ℵ₀

Premises used: Cardinal.lift_lt_univ', Cardinal.aleph0
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
n : ℕ
⊢ (↑n : Cardinal.{max (u + 1) v}) < univ.{u, v}

Tactic:
natCast_lt_aleph0.trans aleph0_lt_univ

Premises used: Cardinal.natCast_lt_aleph0, Cardinal.aleph0_lt_univ, LT.lt.trans
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ 0 < univ.{u, v}

Tactic:
aleph0_lt_univ.pos

Premises used: LT.lt.pos, Cardinal.aleph0_lt_univ
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ univ.{u, v} ≠ 0

Tactic:
univ_pos.ne'

Premises used: Cardinal.univ_pos, LT.lt.ne'
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ univ.{u, v}.ord = Ordinal.univ.{u, v}

Tactic:
le_antisymm (ord_card_le _) <| le_of_forall_lt fun o h => lt_ord.2 ?_

Premises used: Iff.mpr, le_of_forall_lt, le_antisymm, Cardinal.ord_card_le, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
refine : ∀ (o : Ordinal.{max (u + 1) v}) (h : o < Ordinal.univ.{u, v}), o.card < univ.{u, v}
⊢ univ.{u, v}.ord = Ordinal.univ.{u, v}

Tactic:
refine le_antisymm (ord_card_le _) <| le_of_forall_lt fun o h => lt_ord.2 ?_

Premises used: Iff.mpr, le_of_forall_lt, le_antisymm, Cardinal.ord_card_le, Cardinal.lt_ord