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 → Prop
s : β_1 → β_1 → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
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
⊢ 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_2 : ∀ (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 ↦ ⟨?_, ?_⟩
-- 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 → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : α → α → Prop
hr : IsWellOrder α r
⊢ Membership.mem (γ := Set Ordinal.{u})
    (range fun (r : { r : β → β → Prop // IsWellOrder β r }) ↦ type (↑r : β → β → Prop))
    ((fun (r : { r : α → α → Prop // IsWellOrder α r }) ↦ type (↑r : α → α → Prop))
      (Subtype.mk (p := fun (r : α → α → Prop) ↦ IsWellOrder α r) r hr))
have refine_1 : β ≃ α
Tactic: refine ⟨⟨_, RelIso.IsWellOrder.preimage r ?_⟩, type_preimage _ _⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
⊢ GaloisConnection ord card
have refine : ∀ (c : Cardinal.{u_1}) (o : Ordinal.{u_1}) (α β : Type u_1) (s : β → β → Prop) (x : IsWellOrder β s),
  (#α).ord ≤ type s ↔ #α ≤ (type s).card
Tactic: refine fun c o ↦ c.inductionOn fun α ↦ o.inductionOn fun β s _ ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
h : IsWellOrder β s
⊢ (#α).ord ≤ type s ↔ #α ≤ (type s).card
have let : ∀ (r : α → α → Prop) (w : IsWellOrder α r) (e : (#α).ord = type r), (#α).ord ≤ type s ↔ #α ≤ (type s).card
Tactic: let ⟨r, _, e⟩ := exists_ord_eq α
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
h : IsWellOrder β s
r : α → α → Prop
w : IsWellOrder α r
e : (#α).ord = type r
⊢ (#α).ord ≤ type s ↔ #α ≤ (type s).card
have mp : (#α).ord ≤ type s → #α ≤ (type s).card
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
h : IsWellOrder β s
r : α → α → Prop
w : IsWellOrder α r
e : (#α).ord = type r
mp : (#α).ord ≤ type s → #α ≤ (type s).card
⊢ (#α).ord ≤ type s ↔ #α ≤ (type s).card
have mpr : #α ≤ (type s).card → (#α).ord ≤ type s
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (hypothesis)
Goal:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
r : α → α → Prop
w : IsWellOrder α r
e : (#α).ord = type r
h : (#α).ord ≤ type s
⊢ #α ≤ (type s).card
have h₁ : type r ≤ type s
Tactic: rw [e] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
h_1 : IsWellOrder β s
r : α → α → Prop
w : IsWellOrder α r
e : (#α).ord = type r
h : #α ≤ (type s).card
⊢ (#α).ord ≤ type s
have mpr : ∀ (f : α ↪ { α := β, r := s, wo := h_1 }.α), (#α).ord ≤ type s
Tactic: obtain ⟨f⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
h : IsWellOrder β s
r : α → α → Prop
w : IsWellOrder α r
e : (#α).ord = type r
f : α ↪ { α := β, r := s, wo := h }.α
⊢ (#α).ord ≤ type s
have mpr : ∀ (g : RelEmbedding (α := α) ((⇑f : (a : α) → { α := β, r := s, wo := h }.α) ⁻¹'o s) s), (#α).ord ≤ type s
Tactic: have g := RelEmbedding.preimage f s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (hypothesis)
Goal:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
h : IsWellOrder β s
r : α → α → Prop
w : IsWellOrder α r
e : (#α).ord = type r
f : α ↪ { α := β, r := s, wo := h }.α
g : RelEmbedding (α := α) ((⇑f : (a : α) → { α := β, r := s, wo := h }.α) ⁻¹'o s) s
⊢ (#α).ord ≤ type s
have this : IsWellOrder α ((⇑f : (a : α) → { α := β, r := s, wo := h }.α) ⁻¹'o s)
Tactic: have := RelEmbedding.isWellOrder g
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
⊢ o.card ≤ c ↔ o < (succ c).ord
have rw : o.card ≤ c ↔ o.card < succ c
Tactic: rw [lt_ord, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
rw : o.card ≤ c ↔ o.card < succ c
⊢ o.card ≤ c ↔ o < (succ c).ord
have rw₁ : o.card ≤ c ↔ o.card ≤ c
Tactic: rw [lt_ord, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c
have rw : o.card ≤ c.ord.card
Tactic: rw [← card_ord c]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
n : ℕ
⊢ ord (↑n : Cardinal.{u_1}) = (↑n : Ordinal.{u_1})
have apply : (↑n : Ordinal.{u_1}) ≤ ord (↑n : Cardinal.{u_1})
Tactic: apply (ord_le.2 (card_nat n).ge).antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
n : ℕ
⊢ (↑n : Ordinal.{u_1}) ≤ ord (↑n : Cardinal.{u_1})
have zero : (↑0 : Ordinal.{u_1}) ≤ ord (↑0 : Cardinal.{u_1})
Tactic: induction n with
  | zero => exact zero_le
  | succ n IH => exact (IH.trans_lt <| by simp).succ_le
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
n : ℕ
zero : (↑0 : Ordinal.{u_1}) ≤ ord (↑0 : Cardinal.{u_1})
⊢ (↑n : Ordinal.{u_1}) ≤ ord (↑n : Cardinal.{u_1})
have succ : ∀ (n : ℕ) (IH : (↑n : Ordinal.{u_1}) ≤ ord (↑n : Cardinal.{u_1})),
  (↑(n + 1) : Ordinal.{u_1}) ≤ ord (↑(n + 1) : Cardinal.{u_1})
Tactic: induction n with
  | zero => exact zero_le
  | succ n IH => exact (IH.trans_lt <| by simp).succ_le
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ a.ord ∈ lowerBounds (upperBounds (ord '' Iio a))
have simp_rw : ∀ ⦃a_1 : Ordinal.{u_1}⦄, (∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x ≤ a_1.card) → a ≤ a_1.card
Tactic: simp_rw [lowerBounds, upperBounds, mem_setOf, forall_mem_image, ord_le]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ ∀ ⦃a_1 : Ordinal.{u_1}⦄, (∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x ≤ a_1.card) → a ≤ a_1.card
have refine : ∀ (b : Ordinal.{u_1}) (H : ∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x ≤ b.card) (c : Cardinal.{u_1}) (hc : c < a), c < b.card
Tactic: refine fun b H ↦ le_of_forall_lt fun c hc ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
⊢ ℵ₀.ord = ω
have refine : ∀ (o : Ordinal.{u}) (h : o < ω), o < ℵ₀.ord
Tactic: refine le_antisymm (ord_le.2 le_rfl) <| le_of_forall_lt fun o h ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u}
h : o < ω
⊢ o < ℵ₀.ord
have rcases : ∀ (o : Ordinal.{0}) (ho : o < type fun (x1 x2 : ℕ) ↦ x1 < x2) (h : Ordinal.lift.{u, 0} o < ω),
  Ordinal.lift.{u, 0} o < ℵ₀.ord
Tactic: rcases Ordinal.lt_lift_iff.1 h with ⟨o, ho, rfl⟩
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{0}
ho : o < type fun (x1 x2 : ℕ) ↦ x1 < x2
h : Ordinal.lift.{u, 0} o < ω
⊢ Ordinal.lift.{u, 0} o < ℵ₀.ord
have rw : card
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ℕ) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{0}) ↦ x1 < x2)
          (typein fun (x1 x2 : ℕ) ↦ x1 < x2) :
        (a : ℕ) → Ordinal.{0})
      ((enum fun (x1 x2 : ℕ) ↦ x1 < x2 : (a : (↑(Iio (type fun (x1 x2 : ℕ) ↦ x1 < x2)) : Type 1)) → ℕ)
          (Subtype.mk (p := fun (x : Ordinal.{0}) ↦ x ∈ Iio (type fun (x1 x2 : ℕ) ↦ x1 < x2)) o ho) :
        ℕ)) <
  ℵ₀
Tactic: rw [lt_ord, ← lift_card, lift_lt_aleph0, ← typein_enum _ ho]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{v}
⊢ Ordinal.lift.{u, v} c.ord = (lift.{u, v} c).ord
have refine_1 : ∀ (a : Ordinal.{max v u}) (ha : a < Ordinal.lift.{u, v} c.ord), a < (lift.{u, v} c).ord
Tactic: refine le_antisymm (le_of_forall_lt fun a ha => ?_) ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{v}
refine_1 : ∀ (a : Ordinal.{max v u}) (ha : a < Ordinal.lift.{u, v} c.ord), a < (lift.{u, v} c).ord
⊢ Ordinal.lift.{u, v} c.ord = (lift.{u, v} c).ord
have refine_2 : (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord
Tactic: refine le_antisymm (le_of_forall_lt fun a ha => ?_) ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{v}
a : Ordinal.{max v u}
ha : a < Ordinal.lift.{u, v} c.ord
⊢ a < (lift.{u, v} c).ord
have refine_1 : ∀ a < c.ord, ∀ (ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord), Ordinal.lift.{u, v} a < (lift.{u, v} c).ord
Tactic: rcases Ordinal.lt_lift_iff.1 ha with ⟨a, _, rfl⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{v}
a : Ordinal.{v}
left : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ Ordinal.lift.{u, v} a < (lift.{u, v} c).ord
have refine_1 : (Ordinal.lift.{u, v} a).card < lift.{u, v} c
Tactic: rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{v}
a : Ordinal.{v}
left : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
refine_1 : (Ordinal.lift.{u, v} a).card < lift.{u, v} c
⊢ Ordinal.lift.{u, v} a < (lift.{u, v} c).ord
have refine_1₁ : lift.{u, v} a.card < lift.{u, v} c
Tactic: rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{v}
a : Ordinal.{v}
left : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
refine_1 : (Ordinal.lift.{u, v} a).card < lift.{u, v} c
refine_1₁ : lift.{u, v} a.card < lift.{u, v} c
⊢ Ordinal.lift.{u, v} a < (lift.{u, v} c).ord
have refine_1₂ : a.card < c
Tactic: rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{v}
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord
have refine_2 : lift.{u, v} c ≤ (Ordinal.lift.{u, v} c.ord).card
Tactic: rw [ord_le, ← lift_card, card_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{v}
refine_2 : lift.{u, v} c ≤ (Ordinal.lift.{u, v} c.ord).card
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord
have refine_2₁ : lift.{u, v} c ≤ lift.{u, v} c.ord.card
Tactic: rw [ord_le, ← lift_card, card_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
c : Cardinal.{v}
refine_2 : lift.{u, v} c ≤ (Ordinal.lift.{u, v} c.ord).card
refine_2₁ : lift.{u, v} c ≤ lift.{u, v} c.ord.card
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord
have refine_2₂ : lift.{u, v} c ≤ lift.{u, v} c
Tactic: rw [ord_le, ← lift_card, card_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ card (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) x) < #α
have rw : ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) x < type r
Tactic: rw [← lt_ord, h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
⊢ 0 < a.ord ↔ 0 < a
have rw : ord 0 < a.ord ↔ 0 < a
Tactic: rw [← ord_zero, ord_lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
rw : ord 0 < a.ord ↔ 0 < a
⊢ 0 < a.ord ↔ 0 < a
have rw₁ : 0 < a ↔ 0 < a
Tactic: rw [← ord_zero, ord_lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
⊢ ω ≤ a.ord ↔ ℵ₀ ≤ a
have rw : ℵ₀.ord ≤ a.ord ↔ ℵ₀ ≤ a
Tactic: rw [← ord_aleph0, ord_le_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
rw : ℵ₀.ord ≤ a.ord ↔ ℵ₀ ≤ a
⊢ ω ≤ a.ord ↔ ℵ₀ ≤ a
have rw₁ : ℵ₀ ≤ a ↔ ℵ₀ ≤ a
Tactic: rw [← ord_aleph0, ord_le_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
⊢ a.ord ≤ ω ↔ a ≤ ℵ₀
have rw : a.ord ≤ ℵ₀.ord ↔ a ≤ ℵ₀
Tactic: rw [← ord_aleph0, ord_le_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
rw : a.ord ≤ ℵ₀.ord ↔ a ≤ ℵ₀
⊢ a.ord ≤ ω ↔ a ≤ ℵ₀
have rw₁ : a ≤ ℵ₀ ↔ a ≤ ℵ₀
Tactic: rw [← ord_aleph0, ord_le_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
n : ℕ
⊢ (↑n : Cardinal.{u_1}) ≤ o.card ↔ (↑n : Ordinal.{u_1}) ≤ o
have rw : ord (↑n : Cardinal.{u_1}) ≤ o ↔ (↑n : Ordinal.{u_1}) ≤ o
Tactic: rw [← Cardinal.ord_le, Cardinal.ord_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
n : ℕ
rw : ord (↑n : Cardinal.{u_1}) ≤ o ↔ (↑n : Ordinal.{u_1}) ≤ o
⊢ (↑n : Cardinal.{u_1}) ≤ o.card ↔ (↑n : Ordinal.{u_1}) ≤ o
have rw₁ : (↑n : Ordinal.{u_1}) ≤ o ↔ (↑n : Ordinal.{u_1}) ≤ o
Tactic: rw [← Cardinal.ord_le, Cardinal.ord_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.card ↔ ω ≤ o
have rw : ℵ₀.ord ≤ o ↔ ω ≤ o
Tactic: rw [← ord_le, ord_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
rw : ℵ₀.ord ≤ o ↔ ω ≤ o
⊢ ℵ₀ ≤ o.card ↔ ω ≤ o
have rw₁ : ω ≤ o ↔ ω ≤ o
Tactic: rw [← ord_le, ord_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
n : ℕ
⊢ (↑n : Cardinal.{u_1}) < o.card ↔ (↑n : Ordinal.{u_1}) < o
have rw : (↑(n + 1) : Ordinal.{u_1}) ≤ o ↔ succ (↑n : Ordinal.{u_1}) ≤ o
Tactic: rw [← natCast_add_one_le_iff, ← succ_le_iff, ← Nat.cast_add_one, nat_le_card]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ o ≤ c.ord ↔ o.card ≤ c
have rcases : ∀ (n : ℕ) (hc : (↑n : Cardinal.{u_1}) < ℵ₀), o ≤ ord (↑n : Cardinal.{u_1}) ↔ o.card ≤ (↑n : Cardinal.{u_1})
Tactic: rcases lt_aleph0.mp hc with ⟨n, rfl⟩
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (hypothesis)
Goal:
a : Cardinal.{u}
b : Ordinal.{max u v}
h : b.card ≤ Cardinal.lift.{v, u} a
⊢ b ∈ range lift.{v, u}
have h₁ : b < lift.{v, u} (succ a).ord
Tactic: rw [card_le_iff, ← lift_succ, ← lift_ord] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
inst_1 : Fintype α
⊢ type r = (↑(Fintype.card α) : Ordinal.{u})
have rw : (type r).card = (↑(Fintype.card α) : Cardinal.{u})
Tactic: rw [← card_eq_nat, card_type, mk_fintype]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
inst_1 : Fintype α
rw : (type r).card = (↑(Fintype.card α) : Cardinal.{u})
⊢ type r = (↑(Fintype.card α) : Ordinal.{u})
have rw₁ : #α = (↑(Fintype.card α) : Cardinal.{u})
Tactic: rw [← card_eq_nat, card_type, mk_fintype]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
inst_1 : Fintype α
rw : (type r).card = (↑(Fintype.card α) : Cardinal.{u})
rw₁ : #α = (↑(Fintype.card α) : Cardinal.{u})
⊢ type r = (↑(Fintype.card α) : Ordinal.{u})
have rw₂ : Eq.{u + 2} (α := Cardinal.{u}) (↑(Fintype.card α) : Cardinal.{u}) (↑(Fintype.card α) : Cardinal.{u})
Tactic: rw [← card_eq_nat, card_type, mk_fintype]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
s : Set α
⊢ (#(↑s : Type u)).ord ≤ type r
have grw : ∃ (p : Set α), #(↑p : Type u) = #(↑s : Type u)
Tactic: grw [← ord_le_type, ord_le_ord, le_mk_iff_exists_set]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
s w : Set α
⊢ ∃ (p : Set α), #(↑p : Type u) = #(↑s : Type u)
have h : #(↑s : Type u) = #(↑s : Type u)
Tactic: use s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ (#(↑s : Type u)).ord < type r
have grw : #(↑s : Type u) < #(↑univ : Type u)
Tactic: grw [← ord_le_type, ord_lt_ord, ← mk_univ (α := α)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ ¬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)
have 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) sorry 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 sorry) :
        α) :
    Ordinal.{u})
Tactic: grw [← typein_le_typein, typein_enum, Cardinal.le_ord_iff_card_le_of_lt_aleph0 _ hfin.lt_aleph0,
    card_typein_min_le_mk]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
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})
⊢ ¬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)
have grw₁ : ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
    (WellFounded.min (r := r) sorry sᶜ h) ≤
  (#(↑s : Type u)).ord
Tactic: grw [← typein_le_typein, typein_enum, Cardinal.le_ord_iff_card_le_of_lt_aleph0 _ hfin.lt_aleph0,
    card_typein_min_le_mk]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
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
⊢ ¬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)
have grw₂ : card
    (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u})
      (WellFounded.min (r := r) sorry sᶜ h)) ≤
  #(↑s : Type u)
Tactic: grw [← typein_le_typein, typein_enum, Cardinal.le_ord_iff_card_le_of_lt_aleph0 _ hfin.lt_aleph0,
    card_typein_min_le_mk]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
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)
⊢ ¬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)
have grw₃ : #(↑s : Type u) ≤ #(↑s : Type u)
Tactic: grw [← typein_le_typein, typein_enum, Cardinal.le_ord_iff_card_le_of_lt_aleph0 _ hfin.lt_aleph0,
    card_typein_min_le_mk]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (hypothesis)
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
⊢ ∀ 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
have hmltl₁ : Lex (fun (x1 x2 : α) ↦ x1 < x2) m l
Tactic: replace hmltl : List.Lex (· < ·) m l := hmltl
Cleared hypotheses: hmltl
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Basic (goal)
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
have 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})
Tactic: refine lt_of_le_of_lt ?_ (hlt a mem_cons_self)