awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ (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.{v, max u v} (type s) = 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
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
h₂ : lift.{v, max u v} (type s) = 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₃ : type s = 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:
o : Ordinal.{u}
⊢ #(↑(Iio o) : Type (u + 1)) = Cardinal.lift.{u + 1, u} o.card
have rw : #(↑(Iio o) : Type (u + 1)) =
  card
    ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{u + 1}) ↦ x1 < x2) (typein LT.lt) :
        (a : Ordinal.{u}) → Ordinal.{u + 1})
      o)
Tactic: rw [lift_card, ← typein_ordinal]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
n : ℕ
⊢ card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u})
have zero : card (↑0 : Ordinal.{u}) = (↑0 : Cardinal.{u})
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
n : ℕ
zero : card (↑0 : Ordinal.{u}) = (↑0 : Cardinal.{u})
⊢ card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u})
have succ : ∀ (n : ℕ), card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u}) → card (↑(n + 1) : Ordinal.{u}) = (↑(n + 1) : Cardinal.{u})
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
n : ℕ
⊢ card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u})
have zero : card (↑0 : Ordinal.{u}) = (↑0 : Cardinal.{u})
Tactic: induction n <;> [simp; simp only [card_add, card_one, Nat.cast_succ, *]]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
n : ℕ
zero : card (↑0 : Ordinal.{u}) = (↑0 : Cardinal.{u})
⊢ card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u})
have succ : ∀ (n : ℕ), card (↑n : Ordinal.{u}) = (↑n : Cardinal.{u}) → card (↑(n + 1) : Ordinal.{u}) = (↑(n + 1) : Cardinal.{u})
Tactic: induction n <;> [simp; simp only [card_add, card_one, Nat.cast_succ, *]]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) a b →
    (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) ((fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c a)
      ((fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c b)
have refine : ∀ (α : Type u) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type u) (s : β → β → Prop) (x_1 : IsWellOrder β s)
  (γ : Type u) (t : γ → γ → Prop),
  IsWellOrder γ t →
    (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) (type r) (type s) →
      ∀ (f : r ≼i s) (a b : γ ⊕ α),
        Sum.Lex t r a b →
          Sum.Lex t s
            ((fun (x : γ ⊕ α) ↦
                (Sum.recOn (motive := fun (x : γ ⊕ α) ↦ γ ⊕ β) x Sum.inl (Sum.inr ∘ (⇑f : (a : α) → β)) : γ ⊕ β))
              a)
            ((fun (x : γ ⊕ α) ↦
                (Sum.recOn (motive := fun (x : γ ⊕ α) ↦ γ ⊕ β) x Sum.inl (Sum.inr ∘ (⇑f : (a : α) → β)) : γ ⊕ β))
              b)
Tactic: refine inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦
      (RelEmbedding.ofMonotone (Sum.recOn · Sum.inl (Sum.inr ∘ f)) ?_).ordinal_type_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) a b →
    (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2)
      (Function.swap (φ := fun (a a_2 : Ordinal.{u}) ↦ Ordinal.{u}) (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c a)
      (Function.swap (φ := fun (a a_2 : Ordinal.{u}) ↦ Ordinal.{u}) (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c b)
have refine : ∀ (α : Type u) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type u) (s : β → β → Prop) (x_1 : IsWellOrder β s)
  (γ : Type u) (t : γ → γ → Prop),
  IsWellOrder γ t →
    (fun (x1 x2 : Ordinal.{u}) ↦ x1 ≤ x2) (type r) (type s) →
      ∀ (f : r ≼i s) (a b : α ⊕ γ),
        Sum.Lex r t a b →
          Sum.Lex s t
            ((fun (x : α ⊕ γ) ↦
                (Sum.recOn (motive := fun (x : α ⊕ γ) ↦ β ⊕ γ) x (Sum.inl ∘ (⇑f : (a : α) → β)) Sum.inr : β ⊕ γ))
              a)
            ((fun (x : α ⊕ γ) ↦
                (Sum.recOn (motive := fun (x : α ⊕ γ) ↦ β ⊕ γ) x (Sum.inl ∘ (⇑f : (a : α) → β)) Sum.inr : β ⊕ γ))
              b)
Tactic: refine inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦
      (RelEmbedding.ofMonotone (Sum.recOn · (Sum.inl ∘ f) Sum.inr) ?_).ordinal_type_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ b → ∃ (c : Ordinal.{u_1}), b = a + c
have refine : ∀ (α : Type u_1) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type u_1) (s : β → β → Prop) (x_1 : IsWellOrder β s),
  type r ≤ type s → ∀ (f : r ≼i s), ∃ (c : Ordinal.{u_1}), type s = type r + c
Tactic: refine inductionOn₂ a b fun α r _ β s _ ⟨f⟩ ↦ ?_
-- 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 b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
h_2 : type r ≤ type s
f : r ≼i s
⊢ ∃ (c : Ordinal.{u_1}), type s = type r + c
have obtain : ∀ (γ : Type u_1) (t : γ → γ → Prop),
  IsWellOrder γ t → ∀ (g : Sum.Lex r t ≃r s), ∃ (c : Ordinal.{u_1}), type s = type r + c
Tactic: obtain ⟨γ, t, _, ⟨g⟩⟩ := f.exists_sum_relIso
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a + 1 ≤ b ↔ a < b
have refine_1 : ∀ (α : Type u_1) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type u_1) (s : β → β → Prop) (x_1 : IsWellOrder β s),
  type r + 1 ≤ type s → type r < type s
Tactic: refine inductionOn₂ a b fun α r _ β s _ ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a b : Ordinal.{u_1}
refine_1 :
  ∀ (α : Type u_1) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type u_1) (s : β → β → Prop) (x_1 : IsWellOrder β s),
    type r + 1 ≤ type s → type r < type s
⊢ a + 1 ≤ b ↔ a < b
have refine_2 : ∀ (α : Type u_1) (r : α → α → Prop) (x : IsWellOrder α r) (β : Type u_1) (s : β → β → Prop) (x_1 : IsWellOrder β s),
  type r < type s → type r + 1 ≤ type s
Tactic: refine inductionOn₂ a b fun α r _ β s _ ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
f : InitialSeg (α := α ⊕ PUnit.{u_1 + 1}) (Sum.Lex r emptyRelation) s
⊢ type r < type s
have refine_1 : ∀
  (h :
    Surjective (α := α) (β := β)
      (⇑(InitialSeg.trans (r := r) (s := Sum.Lex r emptyRelation) (t := s) (InitialSeg.leAdd r emptyRelation) f) :
        (a : α) → β)),
  False
Tactic: refine ⟨((InitialSeg.leAdd _ _).trans f).toPrincipalSeg fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
f : r ≺i s
⊢ type r + 1 ≤ type s
have apply : ∀ (a b : α ⊕ PUnit.{u_1 + 1}),
  Sum.Lex r emptyRelation a b →
    s
      ((fun (x : α ⊕ PUnit.{u_1 + 1}) ↦
          (Sum.recOn (motive := fun (x : α ⊕ PUnit.{u_1 + 1}) ↦ β) x
              (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β) fun (x : PUnit.{u_1 + 1}) ↦
              f.top (r := r) (s := s) :
            β))
        a)
      ((fun (x : α ⊕ PUnit.{u_1 + 1}) ↦
          (Sum.recOn (motive := fun (x : α ⊕ PUnit.{u_1 + 1}) ↦ β) x
              (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β) fun (x : PUnit.{u_1 + 1}) ↦
              f.top (r := r) (s := s) :
            β))
        b)
Tactic: apply (RelEmbedding.ofMonotone (Sum.recOn · f fun _ ↦ f.top) ?_).ordinal_type_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ a =
    (enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) 0
        uniqueToTypeOne._proof_1)
have rw : Eq (α := ToType 1)
  ((enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2))
        ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦
              x1 < x2) (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
            (a : ToType 1) → Ordinal.{u_1})
          a)
        sorry) :
    ToType 1)
  ((enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) 0
        uniqueToTypeOne._proof_1) :
    ToType 1)
Tactic: rw [← enum_typein (α := ToType 1) (· < ·) a]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ Eq (α := ToType 1)
    ((enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
          (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
        (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2))
          ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦
                x1 < x2) (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
              (a : ToType 1) → Ordinal.{u_1})
            a)
          ⋯) :
      ToType 1)
    ((enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
          (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
        (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) 0
          uniqueToTypeOne._proof_1) :
      ToType 1)
have h : Eq (α := Ordinal.{u_1})
  ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
          (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
        (a : ToType 1) → Ordinal.{u_1})
      a :
    Ordinal.{u_1})
  (0 : Ordinal.{u_1})
Tactic: congr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ Eq (α := Ordinal.{u_1})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
            (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
          (a : ToType 1) → Ordinal.{u_1})
        a :
      Ordinal.{u_1})
    (0 : Ordinal.{u_1})
have h : LT.lt (α := Ordinal.{u_1})
  ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
          (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
        (a : ToType 1) → Ordinal.{u_1})
      a :
    Ordinal.{u_1})
  (1 : Ordinal.{u_1})
Tactic: rw [← lt_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
⊢ Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2) ↔ ∃ (x : α), IsMax x
have simp_rw : Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2) ↔ ∃ (x : α), IsTop x
Tactic: simp_rw [← isTop_iff_isMax]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
⊢ Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2) ↔ ∃ (x : α), IsTop x
have mp : Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2) → ∃ (x : α), IsTop x
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
mp : Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2) → ∃ (x : α), IsTop x
⊢ Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2) ↔ ∃ (x : α), IsTop x
have mpr : (∃ (x : α), IsTop x) → Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
⊢ ∃ (x : α), IsTop x
have mp : a ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)
Tactic: refine ⟨enum (α := α) (· < ·) ⟨a, ?_⟩, fun b ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
mp : a ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)
⊢ ∃ (x : α), IsTop x
have mp₁ : ∀ (b : α),
  b ≤
    (enum fun (x1 x2 : α) ↦ x1 < x2 : (a : (↑(Iio (type fun (x1 x2 : α) ↦ x1 < x2)) : Type (u + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)) a sorry)
Tactic: refine ⟨enum (α := α) (· < ·) ⟨a, ?_⟩, fun b ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
⊢ a ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)
have mp : a < type fun (x1 x2 : α) ↦ x1 < x2
Tactic: rw [mem_Iio, ← ha, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
mp : a < type fun (x1 x2 : α) ↦ x1 < x2
⊢ a ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)
have mp₁ : a < succ a
Tactic: rw [mem_Iio, ← ha, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
mp : a < type fun (x1 x2 : α) ↦ x1 < x2
mp₁ : a < succ a
⊢ a ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)
have mp₂ : a ≤ a
Tactic: rw [mem_Iio, ← ha, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = type fun (x1 x2 : α) ↦ x1 < x2
b : α
⊢ b ≤
    (enum fun (x1 x2 : α) ↦ x1 < x2 : (a : (↑(Iio (type fun (x1 x2 : α) ↦ x1 < x2)) : Type (u + 1))) → α)
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)) a ⋯)
have mp : (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
        (typein fun (x1 x2 : α) ↦ x1 < x2) :
      (a : α) → Ordinal.{u})
    b <
  type fun (x1 x2 : α) ↦ x1 < x2
Tactic: rw [← enum_typein (α := α) (· < ·) b, ← not_lt, enum_le_enum (r := (· < ·)),
        Subtype.mk_le_mk, ← lt_succ_iff, ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : IsTop a
⊢ Membership.mem (γ := Set Ordinal.{u}) (range succ) (type fun (x1 x2 : α) ↦ x1 < x2)
have mpr : ∀ (o : Ordinal.{u}),
  o <
      succ
        ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (typein fun (x1 x2 : α) ↦ x1 < x2) :
            (a : α) → Ordinal.{u})
          a) ↔
    o < type fun (x1 x2 : α) ↦ x1 < x2
Tactic: refine ⟨typein (α := α) (· < ·) a, eq_of_forall_lt_iff fun o ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
⊢ o <
      succ
        ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (typein fun (x1 x2 : α) ↦ x1 < x2) :
            (a : α) → Ordinal.{u})
          a) ↔
    o < type fun (x1 x2 : α) ↦ x1 < x2
have mpr : o ≤
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (typein fun (x1 x2 : α) ↦ x1 < x2) :
        (a : α) → Ordinal.{u})
      a ↔
  o < type fun (x1 x2 : α) ↦ x1 < x2
Tactic: rw [lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
⊢ o ≤
      (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        a ↔
    o < type fun (x1 x2 : α) ↦ x1 < x2
have mpr : ∀ (h : o < type fun (x1 x2 : α) ↦ x1 < x2),
  o ≤
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (typein fun (x1 x2 : α) ↦ x1 < x2) :
        (a : α) → Ordinal.{u})
      a
Tactic: refine ⟨fun h ↦ h.trans_lt (typein_lt_type _ _), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < type fun (x1 x2 : α) ↦ x1 < x2
⊢ o ≤
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (typein fun (x1 x2 : α) ↦ x1 < x2) :
        (a : α) → Ordinal.{u})
      a
have mpr : (enum fun (x1 x2 : α) ↦ x1 < x2 : (a : (↑(Iio (type fun (x1 x2 : α) ↦ x1 < x2)) : Type (u + 1))) → α)
    (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type fun (x1 x2 : α) ↦ x1 < x2)) o h) ≤
  a
Tactic: rw [← typein_enum _ h, typein_le_typein, not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
⊢ IsSuccPrelimit (type fun (x1 x2 : α) ↦ x1 < x2) ↔ NoMaxOrder α
have rw : (∃ (x : α), IsMax x) ↔ ¬∀ (x : α), ¬IsMax x
Tactic: rw [← not_iff_not, noMaxOrder_iff, not_isSuccPrelimit_iff_mem_range_succ,
    type_lt_mem_range_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
x : ToType 1
⊢ Eq (α := Ordinal.{u_1})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
            (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
          (a : ToType 1) → Ordinal.{u_1})
        x :
      Ordinal.{u_1})
    (0 : Ordinal.{u_1})
have rw : Eq (α := Ordinal.{u_1})
  ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
          (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
        (a : ToType 1) → Ordinal.{u_1})
      ((enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
            (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
          (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) 0
            uniqueToTypeOne._proof_1) :
        ToType 1) :
    Ordinal.{u_1})
  (0 : Ordinal.{u_1})
Tactic: rw [one_toType_eq x, typein_enum]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
x : ToType 1
rw :
  Eq (α := Ordinal.{u_1})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
            (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
          (a : ToType 1) → Ordinal.{u_1})
        ((enum fun (x1 x2 : ToType 1) ↦ x1 < x2 :
              (a : (↑(Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) : Type (u_1 + 1))) → ToType 1)
            (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : ToType 1) ↦ x1 < x2)) 0
              uniqueToTypeOne._proof_1) :
          ToType 1) :
      Ordinal.{u_1})
    (0 : Ordinal.{u_1})
⊢ Eq (α := Ordinal.{u_1})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
            (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
          (a : ToType 1) → Ordinal.{u_1})
        x :
      Ordinal.{u_1})
    (0 : Ordinal.{u_1})
have rw₁ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 0 0
Tactic: rw [one_toType_eq x, typein_enum]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
a : (succ o).ToType
⊢ a ≤
    (enum fun (x1 x2 : (succ o).ToType) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : (succ o).ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → (succ o).ToType)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : (succ o).ToType) ↦ x1 < x2)) o ⋯)
have rw : (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (succ o).ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
        (typein fun (x1 x2 : (succ o).ToType) ↦ x1 < x2) :
      (a : (succ o).ToType) → Ordinal.{u_1})
    a <
  succ o
Tactic: rw [← enum_typein (α := (succ o).ToType) (· < ·) a, enum_le_enum', Subtype.mk_le_mk,
    ← lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α_1 : Type u
β_1 : Type v
γ : Type w
r : α_1 → α_1 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
⊢ Eq.{u + 2} (α := Ordinal.{u})
    ((fun (α : Type u) ↦ (⨅ (r : { r : α → α → Prop // IsWellOrder α r }), type (↑r : α → α → Prop) : Ordinal.{u})) α)
    ((fun (α : Type u) ↦ (⨅ (r : { r : α → α → Prop // IsWellOrder α r }), type (↑r : α → α → Prop) : Ordinal.{u})) β)
have refine_1 : ∀ (o : Ordinal.{u}),
  Membership.mem (γ := Set Ordinal.{u})
      (range fun (r : { r : α → α → Prop // IsWellOrder α r }) ↦ type (↑r : α → α → Prop)) o →
    Membership.mem (γ := Set Ordinal.{u})
      (range fun (r : { r : β → β → Prop // IsWellOrder β r }) ↦ type (↑r : β → β → Prop)) o
Tactic: refine congr_arg sInf <| ext fun o ↦ ⟨?_, ?_⟩