awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
S : Set Ordinal.{u_1}
h : ∀ (U : Set Ordinal.{u_1}), Membership.mem (γ := Filter Ordinal.{u_1}) (𝓝 0) U → ∃ y ∈ U ∩ S, y ≠ 0
x : Ordinal.{u_1}
hx : x ∈ Iio 1 ∩ S ∧ x ≠ 0
⊢ False

Tactic:
hx.2 <| lt_one_iff.mp hx.1.1

Premises used: And.right, And.left, Iff.mp, Order.lt_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
S : Set Ordinal.{u_1}
h : ∀ (U : Set Ordinal.{u_1}), Membership.mem (γ := Filter Ordinal.{u_1}) (𝓝 0) U → ∃ y ∈ U ∩ S, y ≠ 0
x : Ordinal.{u_1}
hx : x ∈ Iio 1 ∩ S ∧ x ≠ 0
⊢ False

Tactic:
exact hx.2 <| lt_one_iff.mp hx.1.1

Premises used: And.right, Iff.mp, Order.lt_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
mp : ∀ (x : Ordinal.{u_1}) (hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o), (S ∩ Ioo p o).Nonempty
⊢ (S ∩ Ioo p o).Nonempty

Tactic:
obtain ⟨x, hx⟩ := h (Ioo p (o + 1)) <| Ioo_mem_nhds plt (lt_succ o)

Premises used: Order.lt_succ, Ioo_mem_nhds, HAdd.hAdd, OfNat.ofNat, Set.Ioo
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
h₁ : x ∈ S ∩ Ioo p o
⊢ (S ∩ Ioo p o).Nonempty

Tactic:
use x
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
⊢ x ∈ S ∩ Ioo p o

Tactic:
⟨hx.1.2, ⟨hx.1.1.1, lt_of_le_of_ne ?_ hx.2⟩⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, And.intro, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
h₁ : x ≤ o
⊢ x ∈ S ∩ Ioo p o

Tactic:
refine ⟨hx.1.2, ⟨hx.1.1.1, lt_of_le_of_ne ?_ hx.2⟩⟩
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
⊢ x < o + 1

Tactic:
have := hx.1.1.2
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
this : x < o + 1
h₁ : ∀ (this : x < succ o), x ≤ o
h₂ h₃ h₄ h₅ : ∀ (this : x ≤ o), x ≤ o
⊢ x ≤ o

Tactic:
rwa [← succ_eq_add_one, lt_succ_iff] at this

Premises used: Order.succ_eq_add_one, Order.lt_succ_iff
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
mpr : (¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty) → ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
⊢ (¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty) → AccPt o (𝓟 S)

Tactic:
rw [accPt_iff_nhds]

Premises used: accPt_iff_nhds
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
mpr : ∀ (l : Ordinal.{u_1}) (hl : l < o ∧ Ioc l o ⊆ u), ∃ y ∈ u ∩ S, y ≠ o
⊢ ∃ y ∈ u ∩ S, y ≠ o

Tactic:
obtain ⟨l, hl⟩ := exists_Ioc_subset_of_mem_nhds umem ⟨0, pos_iff_ne_zero.mpr h.1⟩

Premises used: Iff.mpr, exists_Ioc_subset_of_mem_nhds, And.left, Exists.intro, OfNat.ofNat, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
mpr : ∀ (x : Ordinal.{u_1}) (hx : x ∈ S ∩ Ioo l o), ∃ y ∈ u ∩ S, y ≠ o
⊢ ∃ y ∈ u ∩ S, y ≠ o

Tactic:
obtain ⟨x, hx⟩ := h.2 l hl.1

Premises used: And.right, And.left
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
x : Ordinal.{u_1}
hx : x ∈ S ∩ Ioo l o
h₁ : x ∈ u ∩ S ∧ x ≠ o
⊢ ∃ y ∈ u ∩ S, y ≠ o

Tactic:
use x
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
x : Ordinal.{u_1}
hx : x ∈ S ∩ Ioo l o
⊢ x ∈ u ∩ S ∧ x ≠ o

Tactic:
⟨⟨hl.2 ⟨hx.2.1, hx.2.2.le⟩, hx.1⟩, hx.2.2.ne⟩

Premises used: LT.lt.le, And.right, And.left, And.intro, LT.lt.ne
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
x : Ordinal.{u_1}
hx : x ∈ S ∩ Ioo l o
⊢ x ∈ u ∩ S ∧ x ≠ o

Tactic:
exact ⟨⟨hl.2 ⟨hx.2.1, hx.2.2.le⟩, hx.1⟩, hx.2.2.ne⟩
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o.IsAcc S
⊢ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
((isAcc_iff _ _).mp h).2

Premises used: Ordinal.isAcc_iff, And.right, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o.IsAcc S
⊢ 0 < o

Tactic:
pos_iff_ne_zero.mpr ((isAcc_iff _ _).mp h).1

Premises used: Iff.mpr, Ordinal.isAcc_iff, And.left, Iff.mp, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o.IsAcc S
⊢ o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty

Tactic:
rw [isAcc_iff] at h

Premises used: Ordinal.isAcc_iff
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
rw : o ≠ 0 ∧ IsSuccPrelimit o
⊢ IsSuccLimit o

Tactic:
rw [isSuccLimit_iff]

Premises used: Ordinal.isSuccLimit_iff
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ o ≠ 0 ∧ IsSuccPrelimit o

Tactic:
⟨h.1, isSuccPrelimit_of_succ_ne fun x hx ↦ ?_⟩

Premises used: Order.isSuccPrelimit_of_succ_ne, And.left, And.intro
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
refine : ∀ (x : Ordinal.{u_1}) (hx : succ x = o), False
⊢ o ≠ 0 ∧ IsSuccPrelimit o

Tactic:
refine ⟨h.1, isSuccPrelimit_of_succ_ne fun x hx ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
x : Ordinal.{u_1}
hx : succ x = o
rcases : ∀ (p : Ordinal.{u_1}) (hp : p ∈ S ∩ Ioo x o), False
⊢ False

Tactic:
rcases h.2 x (lt_of_lt_of_le (lt_succ x) hx.le) with ⟨p, hp⟩

Premises used: Eq.le, Order.lt_succ, And.right, lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
x : Ordinal.{u_1}
hx : succ x = o
p : Ordinal.{u_1}
hp : p ∈ S ∩ Ioo x o
⊢ False

Tactic:
exact (hx.symm ▸ (succ_le_iff.mpr hp.2.1)).not_gt hp.2.2
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S T : Set Ordinal.{u_1}
h : S ⊆ T
ho : o.IsAcc S
rw : ∀ (ho : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty), o ≠ 0 ∧ ∀ p < o, (T ∩ Ioo p o).Nonempty
⊢ o.IsAcc T

Tactic:
rw [isAcc_iff] at *

Premises used: Ordinal.isAcc_iff
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S T : Set Ordinal.{u_1}
h : S ⊆ T
ho : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ o ≠ 0 ∧ ∀ p < o, (T ∩ Ioo p o).Nonempty

Tactic:
⟨ho.1, fun p plto ↦ (ho.2 p plto).casesOn fun s hs ↦ ⟨s, h hs.1, hs.2⟩⟩

Premises used: Exists.casesOn, And.right, And.left, And.intro
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S T : Set Ordinal.{u_1}
h : S ⊆ T
ho : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ o ≠ 0 ∧ ∀ p < o, (T ∩ Ioo p o).Nonempty

Tactic:
exact ⟨ho.1, fun p plto ↦ (ho.2 p plto).casesOn fun s hs ↦ ⟨s, h hs.1, hs.2⟩⟩
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hS : o.IsAcc S
p : Ordinal.{u_1}
hp : p < o
⊢ (S ∩ Ioo p o).Nonempty

Tactic:
hS.forall_lt p hp

Premises used: Ordinal.IsAcc.forall_lt
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
rw :
  AccPt p (𝓟 S) ↔
    AccPt (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) p hpo)
      (comap (Subtype.val (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o)) (𝓟 S))
rw₁ rw₂ : AccPt p (𝓟 S) ↔ AccPt (↑(Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) p hpo) : Ordinal.{u_1}) (𝓟 S)
⊢ AccPt p (𝓟 S) ↔ AccPt (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) p hpo) (𝓟 (Iio o ↓∩ S))

Tactic:
rw [← comap_principal, isOpen_Iio.isOpenEmbedding_subtypeVal.accPt_comap_iff]

Premises used: IsOpen.isOpenEmbedding_subtypeVal, isOpen_Iio, Topology.IsOpenEmbedding.accPt_comap_iff, Filter.comap_principal
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsClosedBelow S o ↔ ∀ p < o, p.IsAcc S → p ∈ S

Tactic:
simp [IsClosedBelow, IsAcc, isClosed_iff_accPt, ← comap_principal,
    isOpen_Iio.isOpenEmbedding_subtypeVal.accPt_comap_iff]

Premises used: Ordinal.IsAcc, IsOpen.isOpenEmbedding_subtypeVal, isOpen_Iio, isClosed_iff_accPt, Topology.IsOpenEmbedding.accPt_comap_iff, Filter.comap_principal, Ordinal.IsClosedBelow
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
rw : ∀ p < o, p.IsAcc (⋂₀ S) → p ∈ ⋂₀ S
⊢ IsClosedBelow (⋂₀ S) o

Tactic:
rw [isClosedBelow_iff]

Premises used: Ordinal.isClosedBelow_iff
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
p : Ordinal.{u_1}
plto : p < o
pAcc : p.IsAcc (⋂₀ S)
C : Set Ordinal.{u_1}
CmemS : C ∈ S
⊢ p ∈ C

Tactic:
(h C CmemS).forall_lt p plto (pAcc.mono (sInter_subset_of_mem CmemS))

Premises used: Ordinal.IsClosedBelow.forall_lt, Set.sInter_subset_of_mem, Ordinal.IsAcc.mono
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
p : Ordinal.{u_1}
plto : p < o
pAcc : p.IsAcc (⋂₀ S)
C : Set Ordinal.{u_1}
CmemS : C ∈ S
⊢ p ∈ C

Tactic:
exact (h C CmemS).forall_lt p plto (pAcc.mono (sInter_subset_of_mem CmemS))

Premises used: Ordinal.IsClosedBelow.forall_lt, Set.sInter_subset_of_mem, Ordinal.IsAcc.mono
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
ι : Type u
f : ι → Set Ordinal.{u_1}
o : Ordinal.{u_1}
h : ∀ (i : ι), IsClosedBelow (f i) o
⊢ IsClosedBelow (⋂ (i : ι), f i) o

Tactic:
IsClosedBelow.sInter fun _ ⟨i, hi⟩ ↦ hi ▸ (h i)

Premises used: iInf, Set.iInter, Eq.rec, Ordinal.IsClosedBelow.sInter, Ordinal.IsClosedBelow, _private.0.Ordinal.IsClosedBelow.iInter.match_1
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) = univ.{u, u + 1}

Tactic:
(lift_id _).symm

Premises used: Ordinal.lift_id, Ordinal.univ, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ univ.{u, u + 1} = type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2

Tactic:
lift_id _

Premises used: Ordinal.lift_id, Ordinal.univ
-- 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: Ordinal.lift_lift, Ordinal.univ
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ univ.{u, max (u + 1) v} = univ.{u, v}

Tactic:
congr_fun lift_umax _

Premises used: Ordinal.univ, congr_fun, Ordinal.lift_umax
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
⊢ ∀ (b : Ordinal.{max (u + 1) v}),
    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}))
        b ↔
      b < univ.{u, v}

Tactic:
fun b => inductionOn b ?_

Premises used: Ordinal.inductionOn
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
refine :
  ∀ (b : Ordinal.{max (u + 1) v}) (α : Type (max (u + 1) v)) (r : α → α → Prop) [inst : IsWellOrder α r],
    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}))
        (type r) ↔
      type r < univ.{u, v}
⊢ ∀ (b : Ordinal.{max (u + 1) v}),
    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}))
        b ↔
      b < univ.{u, v}

Tactic:
refine fun b => inductionOn b ?_
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
_ :
  ∀ [inst : IsWellOrder β 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}))
        (type s) ↔
      type s < univ.{u, v}
⊢ ∀ [inst : IsWellOrder β 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}))
        (type s) ↔
      type s < univ.{u, v}

Tactic:
_
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
rw :
  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}))
      (type s) ↔
    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}))
      (type s) ↔
    type s < univ.{u, v}

Tactic:
rw [univ, ← lift_umax]

Premises used: Ordinal.univ, Ordinal.lift_umax
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
mp :
  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}))
      (type s) →
    type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
mpr :
  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}))
      (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}))
      (type s) ↔
    type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  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}))
    (type s)
mp :
  ∀ (a : Ordinal.{u})
    (e :
      (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 =
        type s),
    type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
⊢ type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)

Tactic:
obtain ⟨a, e⟩ := h
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
a : Ordinal.{u}
e :
  (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 =
    type s
mp :
  (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, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
⊢ type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)

Tactic:
rw [← e]
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
a : Ordinal.{u}
e :
  (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 =
    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, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)

Tactic:
inductionOn a ?_

Premises used: Ordinal.inductionOn
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
a : Ordinal.{u}
e :
  (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 =
    type s
mp :
  ∀ (α : Type u) (r : α → α → Prop) [inst : IsWellOrder α 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, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
⊢ (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, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)

Tactic:
refine inductionOn a ?_
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
a : Ordinal.{u}
e :
  (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 =
    type s
α : Type u
r : α → α → Prop
mp :
  ∀ [inst : IsWellOrder α 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, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
⊢ ∀ [inst : IsWellOrder α 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, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)

Tactic:
_
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
a : Ordinal.{u}
e :
  (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 =
    type s
α : Type u
r : α → α → Prop
inst_1 : IsWellOrder α 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, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)

Tactic:
lift_type_lt.{u, u + 1, max (u + 1) v}.2 ⟨typein r⟩

Premises used: Iff.mpr, Ordinal.lift_type_lt, Nonempty.intro, Order.Preimage, Ordinal.typein
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
a : Ordinal.{u}
e :
  (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 =
    type s
α : Type u
r : α → α → Prop
inst_1 : IsWellOrder α 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, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)

Tactic:
exact lift_type_lt.{u, u + 1, max (u + 1) v}.2 ⟨typein r⟩
-- Module: Mathlib.SetTheory.Ordinal.Univ
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h : type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
mpr :
  ∀
    (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))
⊢ 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}))
    (type s)

Tactic:
rw [← lift_id (type s)] at h ⊢

Premises used: Ordinal.lift_id, Ordinal.type