awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
inst_1 : Fintype α
rw : (type r).card = (↑(Fintype.card α) : Cardinal.{u})
rw₁ : #α = (↑(Fintype.card α) : Cardinal.{u})
rw₂ rw₃ : Eq.{u + 2} (α := Cardinal.{u}) (↑(Fintype.card α) : Cardinal.{u}) (↑(Fintype.card α) : Cardinal.{u})
⊢ type r = (↑(Fintype.card α) : Ordinal.{u})

Tactic:
rw [← card_eq_nat, card_type, mk_fintype]

Premises used: Cardinal.mk_fintype, Ordinal.card_type, Ordinal.card_eq_nat
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
n : ℕ
⊢ (type fun (x1 x2 : Fin n) ↦ x1 < x2) = (↑n : Ordinal.{0})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
s : Set α
grw : ∃ (p : Set α), #(↑p : Type u) = #(↑s : Type u)
⊢ (#(↑s : Type u)).ord ≤ type r

Tactic:
grw [← ord_le_type, ord_le_ord, le_mk_iff_exists_set]

Premises used: Cardinal.le_mk_iff_exists_set, Cardinal.ord_le_ord, Cardinal.ord_le_type
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
s w : Set α
h : #(↑s : Type u) = #(↑s : Type u)
⊢ ∃ (p : Set α), #(↑p : Type u) = #(↑s : Type u)

Tactic:
use s
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
grw : #(↑s : Type u) < #(↑univ : Type u)
⊢ (#(↑s : Type u)).ord < type r

Tactic:
grw [← ord_le_type, ord_lt_ord, ← mk_univ (α := α)]

Premises used: Cardinal.mk_univ, Cardinal.ord_lt_ord, Cardinal.ord_le_type
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ #(↑s : Type u) < #(↑univ : Type u)

Tactic:
card_lt_card_of_left_finite hfin h.ssubset_univ

Premises used: Cardinal.card_lt_card_of_left_finite, Set.Nonempty.ssubset_univ
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ #(↑s : Type u) < #(↑univ : Type u)

Tactic:
exact card_lt_card_of_left_finite hfin h.ssubset_univ

Premises used: Cardinal.card_lt_card_of_left_finite, Set.Nonempty.ssubset_univ
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
grw :
  LE.le (α := Ordinal.{u})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
        (WellFounded.min (r := r) ⋯ sᶜ h) :
      Ordinal.{u})
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
        ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) (#(↑s : Type u)).ord ⋯) :
          α) :
      Ordinal.{u})
grw₁ :
  ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
      (WellFounded.min (r := r) ⋯ sᶜ h) ≤
    (#(↑s : Type u)).ord
grw₂ :
  card
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
        (WellFounded.min (r := r) ⋯ sᶜ h)) ≤
    #(↑s : Type u)
grw₃ grw₄ : #(↑s : Type u) ≤ #(↑s : Type u)
⊢ ¬r
      ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) (#(↑s : Type u)).ord ⋯))
      (WellFounded.min (r := r) ⋯ sᶜ h)

Tactic:
grw [← typein_le_typein, typein_enum, Cardinal.le_ord_iff_card_le_of_lt_aleph0 _ hfin.lt_aleph0,
    card_typein_min_le_mk]

Premises used: Ordinal.typein_le_typein, Ordinal.card_typein_min_le_mk, Ordinal.typein_enum, Set.Finite.lt_aleph0, Cardinal.le_ord_iff_card_le_of_lt_aleph0
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
l m : List α
o : Ordinal.{u}
hl : l.SortedGT
hm : m.SortedGT
hmltl : m < l
hlt :
  ∀ i ∈ l,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
⊢ Lex (fun (x1 x2 : α) ↦ x1 < x2) m l

Tactic:
replace hmltl : List.Lex (· < ·) m l := hmltl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
m : List α
o : Ordinal.{u}
hm : m.SortedGT
hl : SortedGT.{u} (α := α) []
hlt :
  ∀ (i : α),
    Membership.mem (γ := List α) [] i →
      (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
            (a : α) → Ordinal.{u})
          i <
        o
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m []
⊢ ∀ i ∈ m,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o

Tactic:
simp at hmltl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
hm : SortedGT.{u} (α := α) []
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) [] (a :: as)
i : α
hi : Membership.mem (γ := List α) [] i
⊢ (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
        (a : α) → Ordinal.{u})
      i <
    o

Tactic:
simp at hi
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
⊢ (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
        (a : α) → Ordinal.{u})
      i <
    o

Tactic:
lt_of_le_of_lt ?_ (hlt a mem_cons_self)

Premises used: lt_of_le_of_lt, List.mem_cons_self
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
refine :
  LE.le (α := Ordinal.{u})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i :
      Ordinal.{u})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        a :
      Ordinal.{u})
⊢ (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
        (a : α) → Ordinal.{u})
      i <
    o

Tactic:
refine lt_of_le_of_lt ?_ (hlt a mem_cons_self)

Premises used: lt_of_le_of_lt, List.mem_cons_self
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
⊢ LE.le (α := Ordinal.{u})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i :
      Ordinal.{u})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        a :
      Ordinal.{u})

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
cons : i ≤ a
⊢ (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
        (a : α) → Ordinal.{u})
      i <
    o

Tactic:
suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
⊢ b ≤ a

Tactic:
List.head_le_of_lt hmltl

Premises used: List.head_le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
⊢ b ≤ a

Tactic:
exact List.head_le_of_lt hmltl

Premises used: List.head_le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : Mem i bs
⊢ i ≤ a

Tactic:
le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))

Premises used: List.rel_of_pairwise_cons, le_of_lt, List.SortedGT.pairwise, lt_of_lt_of_le, List.head_le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : Mem i bs
⊢ i ≤ a

Tactic:
exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))

Premises used: List.rel_of_pairwise_cons, le_of_lt, List.SortedGT.pairwise, lt_of_lt_of_le, List.head_le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
cons : b ≤ a
cons₁ : ∀ (hi : Mem i bs), i ≤ a
⊢ i ≤ a

Tactic:
cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))

Premises used: List.head, List.rel_of_pairwise_cons, le_of_lt, List.tail, List.SortedGT.pairwise, lt_of_lt_of_le, List.head_le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
m : List α
o : Ordinal.{u}
hm : m.SortedGT
a : α
as : List α
hl : (a :: as).SortedGT
hlt :
  ∀ i ∈ a :: as,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m (a :: as)
cons :
  ∀ (hm : SortedGT.{u} (α := α) []) (hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) [] (a :: as)) (i : α),
    Membership.mem (γ := List α) [] i →
      (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
            (a : α) → Ordinal.{u})
          i <
        o
cons₁ :
  ∀ (b : α) (bs : List α) (hm : (b :: bs).SortedGT) (hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) (b :: bs) (a :: as)),
    ∀ i ∈ b :: bs,
      (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
            (a : α) → Ordinal.{u})
          i <
        o
⊢ ∀ i ∈ m,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o

Tactic:
cases m with
    | nil => intro i hi; simp at hi
    | cons b bs =>
      intro i hi
      suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa
      cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))

Premises used: List.head, List.tail, List.cons, List.head_le_of_lt, List.nil
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
l m : List α
o : Ordinal.{u}
hl : l.SortedGT
hm : m.SortedGT
hlt :
  ∀ i ∈ l,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o
hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m l
nil :
  ∀ (hl : SortedGT.{u} (α := α) [])
    (hlt :
      ∀ (i : α),
        Membership.mem (γ := List α) [] i →
          (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
                  (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
                (a : α) → Ordinal.{u})
              i <
            o)
    (hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m []),
    ∀ i ∈ m,
      (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
            (a : α) → Ordinal.{u})
          i <
        o
cons :
  ∀ (a : α) (as : List α) (hl : (a :: as).SortedGT)
    (hlt :
      ∀ i ∈ a :: as,
        (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
                (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
              (a : α) → Ordinal.{u})
            i <
          o)
    (hmltl : Lex (fun (x1 x2 : α) ↦ x1 < x2) m (a :: as)),
    ∀ i ∈ m,
      (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
            (a : α) → Ordinal.{u})
          i <
        o
⊢ ∀ i ∈ m,
    (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : α) ↦ x1 < x2) :
          (a : α) → Ordinal.{u})
        i <
      o

Tactic:
cases l with
  | nil => simp at hmltl
  | cons a as =>
    cases m with
    | nil => intro i hi; simp at hi
    | cons b bs =>
      intro i hi
      suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa
      cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))

Premises used: List.head, List.tail, List.cons, List.head_le_of_lt, List.nil
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_2}
h : ¬o = 0
⊢ o % b ^ log b o < o

Tactic:
mod_opow_log_lt_self b h

Premises used: Ordinal.mod_opow_log_lt_self
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_2}
h : ¬o = 0
⊢ o % b ^ log b o < o

Tactic:
exact mod_opow_log_lt_self b h

Premises used: Ordinal.mod_opow_log_lt_self
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_2}
h : ¬o = 0
⊢ o % b ^ log b o < o

Tactic:
decreasing_by exact mod_opow_log_lt_self b h

Premises used: Ordinal.mod_opow_log_lt_self
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
rw :
  (if h : Eq.{u_2 + 2} (α := Ordinal.{u_2}) 0 0 then Eq.rec (motive := fun (x : Ordinal.{u_2}) (h : 0 = x) ↦ C x) H0 ⋯
    else H 0 h (CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H (0 % b ^ log b 0))) =
    H0
rw₁ rw₂ : Eq.rec (motive := fun (x : Ordinal.{u_2}) (h : 0 = x) ↦ C x) H0 ⋯ = H0
⊢ CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H 0 = H0

Tactic:
rw [CNF.rec, dif_pos rfl]

Premises used: dif_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
rw :
  (if h : o = 0 then Eq.rec (motive := fun (x : Ordinal.{u_2}) (h : 0 = x) ↦ C x) H0 ⋯
    else H o h (CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H (o % b ^ log b o))) =
    H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))
rw₁ :
  H o ho (CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H (o % b ^ log b o)) =
    H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))
hnc : ¬o = 0
rw₂ :
  H o ho (CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H (o % b ^ log b o)) =
    H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))
hnc₁ : ¬o = 0
⊢ CNF.rec b (C := fun (x : Ordinal.{u_2}) ↦ C x) H0 H o = H o ho (CNF.rec b (C := C) H0 H (o % b ^ log b o))

Tactic:
rw [CNF.rec, dif_neg]

Premises used: dif_neg
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b : Ordinal.{u_1}
⊢ CNF b 0 = []

Tactic:
rec_zero b _ _

Premises used: Ordinal.CNF.rec_zero, Ordinal.CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ CNF b o = (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)

Tactic:
rec_pos b ho _ _

Premises used: Ordinal.CNF.rec_pos, Ordinal.CNF
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ b ≠ ⊥

Tactic:
have hb' := hb.ne_bot
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
rw :
  (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y
rw₁ : b ^ e * x + y ≠ 0
⊢ CNF b (b ^ e * x + y) = (e, x) :: CNF b y

Tactic:
rw [CNF.ne_zero]

Premises used: Ordinal.CNF.ne_zero
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
rw :
  (e + log b x, (b ^ e * x + y) / b ^ (e + log b x)) :: CNF b ((b ^ e * x + y) % b ^ (e + log b x)) = (e, x) :: CNF b y
rw₁ : (e + 0, (b ^ e * x + y) / b ^ (e + 0)) :: CNF b ((b ^ e * x + y) % b ^ (e + 0)) = (e, x) :: CNF b y
rw₂ : (e, (b ^ e * x + y) / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₃ : (e, x + y / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₄ : (e, x + 0) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₅ : (e, x) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y
rw₆ : (e, x) :: CNF b (y % b ^ e) = (e, x) :: CNF b y
rw₇ rw₈ : (e, x) :: CNF b y = (e, x) :: CNF b y
⊢ (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y

Tactic:
rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]

Premises used: Ordinal.log_eq_zero, Ordinal.mul_add_div, Ordinal.opow_ne_zero, Ordinal.div_eq_zero_of_lt, Ordinal.log_opow_mul_add, Ordinal.mul_add_mod_self, add_zero, Ordinal.mod_eq_of_lt
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
⊢ b ^ e * x + y ≠ 0

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ CNF 0 o = [(0, o)]

Tactic:
simp [CNF.ne_zero ho]

Premises used: Ordinal.CNF.ne_zero
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ CNF 1 o = [(0, o)]

Tactic:
simp [CNF.ne_zero ho]

Premises used: Ordinal.CNF.ne_zero
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
b o : Ordinal.{u_1}
hb : b ≤ 1
ho : o ≠ 0
inl : ∀ (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1), CNF 0 o = [(0, o)]
inr : ∀ (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1), CNF 1 o = [(0, o)]
⊢ CNF b o = [(0, o)]

Tactic:
rcases Order.le_one_iff.1 hb with (rfl | rfl)

Premises used: Iff.mp, Order.le_one_iff, rfl
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
⊢ CNF 0 o = [(0, o)]

Tactic:
CNF.zero_left ho

Premises used: Ordinal.CNF.zero_left
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
⊢ CNF 1 o = [(0, o)]

Tactic:
CNF.one_left ho

Premises used: Ordinal.CNF.one_left
-- Module: Mathlib.SetTheory.Ordinal.CantorNormalForm
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
⊢ CNF 0 o = [(0, o)]

Tactic:
exacts [CNF.zero_left ho, CNF.one_left ho]

Premises used: Ordinal.CNF.zero_left, Ordinal.CNF.one_left