awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c + 1 = c
have rw : ω ≤ c.ord
Tactic: rw [add_comm, ← card_ord c, ← card_one, ← card_add, one_add_of_omega0_le]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ω ≤ c.ord
have rwa : ℵ₀.ord ≤ c.ord
Tactic: rwa [← ord_aleph0, ord_le_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccLimit c.ord
have left : ¬IsMin c.ord
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
left : ¬IsMin c.ord
⊢ IsSuccLimit c.ord
have right : IsSuccPrelimit c.ord
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord
have right : ∀ (a : Ordinal.{u_1}), a.card < c → a.card + 1 < c
Tactic: simp_rw [isSuccPrelimit_iff_succ_lt, succ_eq_add_one, lt_ord, card_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : a.card < c
⊢ a.card + 1 < c
have right : ∀ (ha : c ≤ a.card + 1), c ≤ a.card
Tactic: contrapose! ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ c ≤ a.card
have right : ℵ₀ ≤ a.card
Tactic: rwa [add_one_of_aleph0_le] at ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ a.card
have right : ℵ₀ ≤ a.card + 1
Tactic: rw [← ord_le, ← IsSuccLimit.le_succ_iff, succ_eq_add_one, ord_le, card_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
right : ℵ₀ ≤ a.card + 1
⊢ ℵ₀ ≤ a.card
have right₁ : IsSuccLimit ℵ₀.ord
Tactic: rw [← ord_le, ← IsSuccLimit.le_succ_iff, succ_eq_add_one, ord_le, card_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ NoMaxOrder.{u_1} c.ord.ToType
have rw : IsSuccPrelimit c.ord
Tactic: rw [← isSuccPrelimit_type_lt_iff, type_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
⊢ type r = 0 ↔ IsEmpty α
have refine : ∀ (h : type r = 0), IsEmpty α
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ type_eq_zero_of_empty r⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
h : type r = 0
⊢ IsEmpty α
have let : ∀ (s : RelIso (β := PEmpty.{u + 1}) r emptyRelation), IsEmpty α
Tactic: let ⟨s⟩ := type_eq.1 h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
inst_1 : Nonempty α
inst_2 : Subsingleton α
⊢ type r = 1
have intro : ∀ (val : Unique α), type r = 1
Tactic: cases nonempty_unique α
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsEmpty.{u_1 + 1} o.ToType ↔ o = 0
have rw : (type fun (x1 x2 : o.ToType) ↦ x1 < x2) = 0 ↔ o = 0
Tactic: rw [← @type_eq_zero_iff_isEmpty o.ToType (· < ·), type_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
rw : (type fun (x1 x2 : o.ToType) ↦ x1 < x2) = 0 ↔ o = 0
⊢ IsEmpty.{u_1 + 1} o.ToType ↔ o = 0
have rw₁ : o = 0 ↔ o = 0
Tactic: rw [← @type_eq_zero_iff_isEmpty o.ToType (· < ·), type_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
⊢ Nonempty.{u_1 + 1} o.ToType ↔ o ≠ 0
have rw : (type fun (x1 x2 : o.ToType) ↦ x1 < x2) ≠ 0 ↔ o ≠ 0
Tactic: rw [← @type_ne_zero_iff_nonempty o.ToType (· < ·), type_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
rw : (type fun (x1 x2 : o.ToType) ↦ x1 < x2) ≠ 0 ↔ o ≠ 0
⊢ Nonempty.{u_1 + 1} o.ToType ↔ o ≠ 0
have rw₁ : o ≠ 0 ↔ o ≠ 0
Tactic: rw [← @type_ne_zero_iff_nonempty o.ToType (· < ·), type_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_2 : WellFoundedLT α] (β : Type u_1) [inst_3 : LinearOrder β]
    [inst_4 : WellFoundedLT β], ((type fun (x1 x2 : α) ↦ x1 < x2) = type fun (x1 x2 : β) ↦ x1 < x2) → f α = f β
γ : Type u_1
inst : LinearOrder γ
inst_1 : WellFoundedLT γ
⊢ (type fun (x1 x2 : γ) ↦ x1 < x2).liftOnWellOrder f c = f γ
have change : ⟦{ α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := sorry : WellOrder.{u_1} }⟧.liftOn' (fun (w : WellOrder.{u_1}) ↦ f w.α) sorry =
  f γ
Tactic: change Quotient.liftOn' ⟦_⟧ _ _ = _
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_2 : WellFoundedLT α] (β : Type u_1) [inst_3 : LinearOrder β]
    [inst_4 : WellFoundedLT β], ((type fun (x1 x2 : α) ↦ x1 < x2) = type fun (x1 x2 : β) ↦ x1 < x2) → f α = f β
γ : Type u_1
inst : LinearOrder γ
inst_1 : WellFoundedLT γ
⊢ ⟦{ α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := ⋯ : WellOrder.{u_1} }⟧.liftOn' (fun (w : WellOrder.{u_1}) ↦ f w.α)
      ⋯ =
    f γ
have rw : f { α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := sorry : WellOrder.{u_1} }.α = f γ
Tactic: rw [Quotient.liftOn'_mk]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_2 : WellFoundedLT α] (β : Type u_1) [inst_3 : LinearOrder β]
    [inst_4 : WellFoundedLT β], ((type fun (x1 x2 : α) ↦ x1 < x2) = type fun (x1 x2 : β) ↦ x1 < x2) → f α = f β
γ : Type u_1
inst : LinearOrder γ
inst_1 : WellFoundedLT γ
⊢ f { α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := ⋯ : WellOrder.{u_1} }.α = f γ
have h : linearOrderOfSTO { α := γ, r := fun (x1 x2 : γ) ↦ x1 < x2, wo := sorry }.r = inst
Tactic: congr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set α
⊢ (type fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ≤ type fun (x1 x2 : α) ↦ x1 < x2
have rw : Nonempty.{u + 1} ((fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ↪r fun (x1 x2 : α) ↦ x1 < x2)
Tactic: rw [type_le_iff']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set α
⊢ Nonempty.{u + 1} ((fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ↪r fun (x1 x2 : α) ↦ x1 < x2)
have refine : ∀ {a b : (↑s : Type u)},
  LT.lt (α := α) ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : (↑s : Type u)) → α) a : α)
      ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : (↑s : Type u)) → α) b : α) ↔
    a < b
Tactic: refine ⟨⟨Embedding.subtype _, ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
h : s ⊆ t
⊢ (type fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ≤ type fun (x1 x2 : (↑t : Type u)) ↦ x1 < x2
have rw : Nonempty.{u + 1} ((fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ↪r fun (x1 x2 : (↑t : Type u)) ↦ x1 < x2)
Tactic: rw [type_le_iff']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
h : s ⊆ t
⊢ Nonempty.{u + 1} ((fun (x1 x2 : (↑s : Type u)) ↦ x1 < x2) ↪r fun (x1 x2 : (↑t : Type u)) ↦ x1 < x2)
have refine : ∀ {a b : (↑s : Type u)},
  LT.lt (α := (↑t : Type u)) ((s.embeddingOfSubset t h : (a : (↑s : Type u)) → (↑t : Type u)) a : (↑t : Type u))
      ((s.embeddingOfSubset t h : (a : (↑s : Type u)) → (↑t : Type u)) b : (↑t : Type u)) ↔
    a < b
Tactic: refine ⟨⟨embeddingOfSubset _ _ h, ?_⟩⟩
-- 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
α β : Ordinal.{u_1}
h : α ≤ β
⊢ (fun (x1 x2 : α.ToType) ↦ x1 < x2) ≼i fun (x1 x2 : β.ToType) ↦ x1 < x2
have apply : (type fun (x1 x2 : α.ToType) ↦ x1 < x2) ≤ type fun (x1 x2 : β.ToType) ↦ x1 < x2
Tactic: apply Classical.choice (type_le_iff.mp _)
-- 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
α β : Ordinal.{u_1}
h : α ≤ β
⊢ (type fun (x1 x2 : α.ToType) ↦ x1 < x2) ≤ type fun (x1 x2 : β.ToType) ↦ x1 < x2
have rwa : α ≤ type fun (x1 x2 : β.ToType) ↦ x1 < x2
Tactic: rwa [type_toType, type_toType]
-- 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
α β : Ordinal.{u_1}
h : α < β
⊢ (fun (x1 x2 : α.ToType) ↦ x1 < x2) ≺i fun (x1 x2 : β.ToType) ↦ x1 < x2
have apply : (type fun (x1 x2 : α.ToType) ↦ x1 < x2) < type fun (x1 x2 : β.ToType) ↦ x1 < x2
Tactic: apply Classical.choice (type_lt_iff.mp _)
-- 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
α β : Ordinal.{u_1}
h : α < β
⊢ (type fun (x1 x2 : α.ToType) ↦ x1 < x2) < type fun (x1 x2 : β.ToType) ↦ x1 < x2
have rwa : α < type fun (x1 x2 : β.ToType) ↦ x1 < x2
Tactic: rwa [type_toType, type_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
⊢ r ≺i fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
have refine_1 : ∀ (a b : α) (ha : r a b) (a_1 : { x : α // r x a }),
  Membership.mem (α := α) (γ := Set α) (fun (x : α) ↦ r x b)
    (((PrincipalSeg.ofElement r a).toRelEmbedding (r := Subrel r fun (x : α) ↦ r x a) (s := r) :
          (a : { x : α // r x a }) → α)
        a_1 :
      α)
Tactic: refine ⟨RelEmbedding.ofMonotone _ fun a b ha ↦
    ((PrincipalSeg.ofElement r a).codRestrict _ ?_ ?_).ordinal_type_lt, type r, fun a ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
refine_1 :
  ∀ (a b : α) (ha : r a b) (a_1 : { x : α // r x a }),
    Membership.mem (α := α) (γ := Set α) (fun (x : α) ↦ r x b)
      (((PrincipalSeg.ofElement r a).toRelEmbedding (r := Subrel r fun (x : α) ↦ r x a) (s := r) :
            (a : { x : α // r x a }) → α)
          a_1 :
        α)
⊢ r ≺i fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
have refine_2 : ∀ (a b : α) (ha : r a b),
  Membership.mem (γ := Set α) (fun (x : α) ↦ r x b)
    ((PrincipalSeg.ofElement r a).top (r := Subrel r fun (x : α) ↦ r x a) (s := r))
Tactic: refine ⟨RelEmbedding.ofMonotone _ fun a b ha ↦
    ((PrincipalSeg.ofElement r a).codRestrict _ ?_ ?_).ordinal_type_lt, type r, fun a ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
refine_1 :
  ∀ (a b : α) (ha : r a b) (a_1 : { x : α // r x a }),
    Membership.mem (α := α) (γ := Set α) (fun (x : α) ↦ r x b)
      (((PrincipalSeg.ofElement r a).toRelEmbedding (r := Subrel r fun (x : α) ↦ r x a) (s := r) :
            (a : { x : α // r x a }) → α)
          a_1 :
        α)
refine_2 :
  ∀ (a b : α) (ha : r a b),
    Membership.mem (γ := Set α) (fun (x : α) ↦ r x b)
      ((PrincipalSeg.ofElement r a).top (r := Subrel r fun (x : α) ↦ r x a) (s := r))
⊢ r ≺i fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
have refine_3 : ∀ (a : Ordinal.{u}),
  Membership.mem (γ := Set Ordinal.{u})
      (range (ι := α)
        (⇑(RelEmbedding.ofMonotone (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (fun (a : α) ↦ type (α := { x : α // r x a }) (Subrel r fun (x : α) ↦ r x a)) sorry) :
          (a : α) → Ordinal.{u}))
      a →
    a < type r
Tactic: refine ⟨RelEmbedding.ofMonotone _ fun a b ha ↦
    ((PrincipalSeg.ofElement r a).codRestrict _ ?_ ?_).ordinal_type_lt, type r, fun a ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
refine_1 :
  ∀ (a b : α) (ha : r a b) (a_1 : { x : α // r x a }),
    Membership.mem (α := α) (γ := Set α) (fun (x : α) ↦ r x b)
      (((PrincipalSeg.ofElement r a).toRelEmbedding (r := Subrel r fun (x : α) ↦ r x a) (s := r) :
            (a : { x : α // r x a }) → α)
          a_1 :
        α)
refine_2 :
  ∀ (a b : α) (ha : r a b),
    Membership.mem (γ := Set α) (fun (x : α) ↦ r x b)
      ((PrincipalSeg.ofElement r a).top (r := Subrel r fun (x : α) ↦ r x a) (s := r))
refine_3 :
  ∀ (a : Ordinal.{u}),
    Membership.mem (γ := Set Ordinal.{u})
        (range (ι := α)
          (⇑(RelEmbedding.ofMonotone (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
                (fun (a : α) ↦ type (α := { x : α // r x a }) (Subrel r fun (x : α) ↦ r x a)) ⋯) :
            (a : α) → Ordinal.{u}))
        a →
      a < type r
⊢ r ≺i fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2
have refine_4 : ∀ a < type r,
  Membership.mem (γ := Set Ordinal.{u})
    (range (ι := α)
      (⇑(RelEmbedding.ofMonotone (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (fun (a : α) ↦ type (α := { x : α // r x a }) (Subrel r fun (x : α) ↦ r x a)) sorry) :
        (a : α) → Ordinal.{u}))
    a
Tactic: refine ⟨RelEmbedding.ofMonotone _ fun a b ha ↦
    ((PrincipalSeg.ofElement r a).codRestrict _ ?_ ?_).ordinal_type_lt, type r, fun a ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r_1 : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r →
    Membership.mem (γ := Set Ordinal.{u})
      (range (ι := α)
        (⇑(RelEmbedding.ofMonotone (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (fun (a : α) ↦ type (α := { x : α // r x a }) (Subrel r fun (x : α) ↦ r x a)) ⋯) :
          (a : α) → Ordinal.{u}))
      a
have refine_4 : ∀ (α_1 : Type u) (r_2 : α_1 → α_1 → Prop) [inst_1 : IsWellOrder α_1 r_2],
  type r_2 < type r →
    Membership.mem (γ := Set Ordinal.{u})
      (range (ι := α)
        (⇑(RelEmbedding.ofMonotone (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
              (fun (a : α) ↦ type (α := { x : α // r x a }) (Subrel r fun (x : α) ↦ r x a)) sorry) :
          (a : α) → Ordinal.{u}))
      (type r_2)
Tactic: refine inductionOn a ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
i : o.ToType
⊢ (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
          (typein fun (x1 x2 : o.ToType) ↦ x1 < x2) :
        (a : o.ToType) → Ordinal.{u_1})
      i <
    o
have simp_rw : (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦ x1 < x2)
        (typein fun (x1 x2 : o.ToType) ↦ x1 < x2) :
      (a : o.ToType) → Ordinal.{u_1})
    i <
  type fun (x1 x2 : o.ToType) ↦ x1 < x2
Tactic: simp_rw [← type_toType o]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
a b : α
⊢ LE.le (α := Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a :
        Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) b :
        Ordinal.{u}) ↔
    ¬r b a
have rw : ¬LT.lt (α := Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (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}) ↔
  ¬r b a
Tactic: rw [← not_lt, typein_lt_typein]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
a b : α
rw :
  ¬LT.lt (α := Ordinal.{u})
        (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (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}) ↔
    ¬r b a
⊢ LE.le (α := Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a :
        Ordinal.{u})
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) b :
        Ordinal.{u}) ↔
    ¬r b a
have rw₁ : ¬r b a ↔ ¬r b a
Tactic: rw [← not_lt, typein_lt_typein]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
o₁ o₂ : (↑(Iio (type r)) : Type (u + 1))
⊢ ¬r ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α) o₁)
        ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α) o₂) ↔
    o₂ ≤ o₁
have rw : ¬o₁ < o₂ ↔ o₂ ≤ o₁
Tactic: rw [enum_lt_enum (r := r), not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
o₁ o₂ : (↑(Iio (type r)) : Type (u + 1))
rw : ¬o₁ < o₂ ↔ o₂ ≤ o₁
⊢ ¬r ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α) o₁)
        ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α) o₂) ↔
    o₂ ≤ o₁
have rw₁ : o₂ ≤ o₁ ↔ o₂ ≤ o₁
Tactic: rw [enum_lt_enum (r := r), not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a : Ordinal.{u_1}
o₁ o₂ : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))
⊢ LE.le (α := a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₁ :
        a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₂ :
        a.ToType) ↔
    o₁ ≤ o₂
have rw : LE.le (α := a.ToType)
    ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
          (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
        o₁ :
      a.ToType)
    ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
          (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
        o₂ :
      a.ToType) ↔
  ¬LT.lt (α := a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₂ :
        a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₁ :
        a.ToType)
Tactic: rw [← enum_le_enum, not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a : Ordinal.{u_1}
o₁ o₂ : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))
rw :
  LE.le (α := a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₁ :
        a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₂ :
        a.ToType) ↔
    ¬LT.lt (α := a.ToType)
        ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
              (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
            o₂ :
          a.ToType)
        ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
              (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
            o₁ :
          a.ToType)
⊢ LE.le (α := a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₁ :
        a.ToType)
      ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
            (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
          o₂ :
        a.ToType) ↔
    o₁ ≤ o₂
have rw₁ : LE.le (α := a.ToType)
    ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
          (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
        o₁ :
      a.ToType)
    ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
          (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
        o₂ :
      a.ToType) ↔
  LE.le (α := a.ToType)
    ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
          (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
        o₁ :
      a.ToType)
    ((enum fun (x1 x2 : a.ToType) ↦ x1 < x2 :
          (a_1 : (↑(Iio (type fun (x1 x2 : a.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → a.ToType)
        o₂ :
      a.ToType)
Tactic: rw [← enum_le_enum, not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ ¬r a
      ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) 0 h0))
have rw : Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) 0 h0 ≤
  Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r))
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a) sorry
Tactic: rw [← enum_typein r a, enum_le_enum r]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
h0 : 0 < o
a : o.ToType
⊢ (enum fun (x1 x2 : o.ToType) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → o.ToType)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) 0 ⋯) ≤
    a
have rw : ¬a <
    (enum fun (x1 x2 : o.ToType) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) : Type (u_1 + 1))) → o.ToType)
      (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) 0 sorry)
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
⊢ ∀ (hr : o < type r) (hs : o < type s),
    Eq (α := β)
      ((f : (a : α) → β)
          ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) o hr) :
            α) :
        β)
      ((enum s : (a : (↑(Iio (type s)) : Type (u + 1))) → β)
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type s)) o hs) :
        β)
have refine : ∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst_2 : IsWellOrder α_1 r_1] (hr : type r_1 < type r)
  (hs : type r_1 < type s),
  Eq (α := β)
    ((f : (a : α) → β)
        ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → α)
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) (type r_1) hr) :
          α) :
      β)
    ((enum s : (a : (↑(Iio (type s)) : Type (u + 1))) → β)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type s)) (type r_1) hs) :
      β)
Tactic: refine inductionOn o ?_