awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Basic
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 r ≤ type s

Tactic:
rw [e] at h
-- Module: Mathlib.SetTheory.Ordinal.Basic
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 r ≤ type s
⊢ #α ≤ (type s).card

Tactic:
card_le_card h

Premises used: Ordinal.card_le_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
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 r ≤ type s
⊢ #α ≤ (type s).card

Tactic:
exact card_le_card h

Premises used: Ordinal.card_le_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
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
mpr : ∀ (f : α ↪ { α := β, r := s, wo := h_1 }.α), (#α).ord ≤ type s
⊢ (#α).ord ≤ type s

Tactic:
obtain ⟨f⟩ := h
-- Module: Mathlib.SetTheory.Ordinal.Basic
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 }.α
mpr : ∀ (g : RelEmbedding (α := α) ((⇑f : (a : α) → { α := β, r := s, wo := h }.α) ⁻¹'o s) s), (#α).ord ≤ type s
⊢ (#α).ord ≤ type s

Tactic:
have g := RelEmbedding.preimage f s
-- Module: Mathlib.SetTheory.Ordinal.Basic
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
⊢ IsWellOrder α ((⇑f : (a : α) → { α := β, r := s, wo := h }.α) ⁻¹'o s)

Tactic:
have := RelEmbedding.isWellOrder g
-- Module: Mathlib.SetTheory.Ordinal.Basic
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
this : IsWellOrder α ((⇑f : (a : α) → { α := β, r := s, wo := h }.α) ⁻¹'o s)
⊢ (#α).ord ≤ type s

Tactic:
(ord_le_type _).trans g.ordinal_type_le

Premises used: RelEmbedding.ordinal_type_le, LE.le.trans, Cardinal.ord_le_type
-- Module: Mathlib.SetTheory.Ordinal.Basic
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
this : IsWellOrder α ((⇑f : (a : α) → { α := β, r := s, wo := h }.α) ⁻¹'o s)
⊢ (#α).ord ≤ type s

Tactic:
exact (ord_le_type _).trans g.ordinal_type_le

Premises used: RelEmbedding.ordinal_type_le, LE.le.trans, Cardinal.ord_le_type
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
⊢ c.ord ≤ o ↔ c ≤ o.card

Tactic:
gc_ord_card.le_iff_le

Premises used: GaloisConnection.le_iff_le, Cardinal.gc_ord_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
⊢ o < c.ord ↔ o.card < c

Tactic:
gc_ord_card.lt_iff_lt

Premises used: Cardinal.gc_ord_card, GaloisConnection.lt_iff_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ Surjective card

Tactic:
fun c ↦ ⟨_, card_ord c⟩

Premises used: Cardinal.ord, Cardinal.card_ord, Exists.intro, Function.Surjective
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
s : Set Cardinal.{u_1}
⊢ BddAbove (ord '' s) ↔ BddAbove s

Tactic:
gc_ord_card.bddAbove_l_image

Premises used: GaloisConnection.bddAbove_l_image, Cardinal.gc_ord_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ o.card.ord ≤ o

Tactic:
gc_ord_card.l_u_le _

Premises used: Cardinal.gc_ord_card, GaloisConnection.l_u_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ o < (succ o.card).ord

Tactic:
lt_ord.2 <| lt_succ _

Premises used: Iff.mpr, Order.lt_succ, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
rw : o.card ≤ c ↔ o.card < succ c
rw₁ rw₂ : o.card ≤ c ↔ o.card ≤ c
⊢ o.card ≤ c ↔ o < (succ c).ord

Tactic:
rw [lt_ord, lt_succ_iff]

Premises used: Order.lt_succ_iff, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
rw : o.card ≤ c.ord.card
⊢ o.card ≤ c

Tactic:
rw [← card_ord c]

Premises used: Cardinal.card_ord
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c.ord.card

Tactic:
Ordinal.card_le_card ho

Premises used: Ordinal.card_le_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c.ord.card

Tactic:
exact Ordinal.card_le_card ho

Premises used: Ordinal.card_le_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ StrictMono ord

Tactic:
gciOrdCard.strictMono_l

Premises used: Cardinal.gciOrdCard, GaloisCoinsertion.strictMono_l
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ Monotone ord

Tactic:
gc_ord_card.monotone_l

Premises used: Cardinal.gc_ord_card, GaloisConnection.monotone_l
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ Injective ord

Tactic:
ord_strictMono.injective

Premises used: StrictMono.injective, Cardinal.ord_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c₁ c₂ : Cardinal.{u_1}
⊢ c₁.ord ≤ c₂.ord ↔ c₁ ≤ c₂

Tactic:
gciOrdCard.l_le_l_iff

Premises used: GaloisCoinsertion.l_le_l_iff, Cardinal.gciOrdCard
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c₁ c₂ : Cardinal.{u_1}
⊢ c₁.ord < c₂.ord ↔ c₁ < c₂

Tactic:
ord_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Cardinal.ord_strictMono
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c₁ c₂ : Cardinal.{u_1}
⊢ c₁.ord = c₂.ord ↔ c₁ = c₂

Tactic:
ord_injective.eq_iff

Premises used: Function.Injective.eq_iff, Cardinal.ord_injective
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ ord 0 = 0

Tactic:
gc_ord_card.l_bot

Premises used: Cardinal.gc_ord_card, GaloisConnection.l_bot
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
n : ℕ
apply : (↑n : Ordinal.{u_1}) ≤ ord (↑n : Cardinal.{u_1})
⊢ ord (↑n : Cardinal.{u_1}) = (↑n : Ordinal.{u_1})

Tactic:
apply (ord_le.2 (card_nat n).ge).antisymm

Premises used: Iff.mpr, Eq.ge, LE.le.antisymm, Cardinal.ord_le, Ordinal.card_nat
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ (↑0 : Ordinal.{u_1}) ≤ ord (↑0 : Cardinal.{u_1})

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ (↑0 : Ordinal.{u_1}) ≤ ord (↑0 : Cardinal.{u_1})

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
n : ℕ
IH : (↑n : Ordinal.{u_1}) ≤ ord (↑n : Cardinal.{u_1})
⊢ ord (↑n : Cardinal.{u_1}) < ord (↑(n + 1) : Cardinal.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
n : ℕ
IH : (↑n : Ordinal.{u_1}) ≤ ord (↑n : Cardinal.{u_1})
⊢ (↑(n + 1) : Ordinal.{u_1}) ≤ ord (↑(n + 1) : Cardinal.{u_1})

Tactic:
exact (IH.trans_lt <| by simp).succ_le

Premises used: LT.lt.succ_le, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
n : ℕ
zero : (↑0 : Ordinal.{u_1}) ≤ ord (↑0 : Cardinal.{u_1})
succ :
  ∀ (n : ℕ) (IH : (↑n : Ordinal.{u_1}) ≤ ord (↑n : Cardinal.{u_1})),
    (↑(n + 1) : Ordinal.{u_1}) ≤ ord (↑(n + 1) : Cardinal.{u_1})
⊢ (↑n : Ordinal.{u_1}) ≤ ord (↑n : Cardinal.{u_1})

Tactic:
induction n with
  | zero => exact zero_le
  | succ n IH => exact (IH.trans_lt <| by simp).succ_le

Premises used: zero_le, Order.succ, Ordinal.zero
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ ord (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
ord_natCast n

Premises used: Cardinal.ord_natCast
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ ord 1 = 1

Tactic:
simpa using ord_natCast 1

Premises used: Cardinal.ord_natCast, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u_1}
ha : IsSuccLimit a
simp_rw : ∀ ⦃a_1 : Ordinal.{u_1}⦄, (∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x ≤ a_1.card) → a ≤ a_1.card
⊢ a.ord ∈ lowerBounds (upperBounds (ord '' Iio a))

Tactic:
simp_rw [lowerBounds, upperBounds, mem_setOf, forall_mem_image, ord_le]

Premises used: lowerBounds, upperBounds, Cardinal.ord_le, Set.mem_setOf, Set.forall_mem_image
-- Module: Mathlib.SetTheory.Ordinal.Basic
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

Tactic:
fun b H ↦ le_of_forall_lt fun c hc ↦ ?_

Premises used: le_of_forall_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u_1}
ha : IsSuccLimit a
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
⊢ ∀ ⦃a_1 : Ordinal.{u_1}⦄, (∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x ≤ a_1.card) → a ≤ a_1.card

Tactic:
refine fun b H ↦ le_of_forall_lt fun c hc ↦ ?_

Premises used: le_of_forall_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u_1}
ha : IsSuccLimit a
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:
simpa using H (ha.succ_lt hc)

Premises used: Order.IsSuccLimit.succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ ℵ₀.ord = ω

Tactic:
le_antisymm (ord_le.2 le_rfl) <| le_of_forall_lt fun o h ↦ ?_

Premises used: Iff.mpr, le_rfl, Cardinal.ord_le, le_of_forall_lt, le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
refine : ∀ (o : Ordinal.{u}) (h : o < ω), o < ℵ₀.ord
⊢ ℵ₀.ord = ω

Tactic:
refine le_antisymm (ord_le.2 le_rfl) <| le_of_forall_lt fun o h ↦ ?_

Premises used: Iff.mpr, le_rfl, Cardinal.ord_le, le_of_forall_lt, le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u}
h : o < ω
rcases :
  ∀ (o : Ordinal.{0}) (ho : o < type fun (x1 x2 : ℕ) ↦ x1 < x2) (h : Ordinal.lift.{u, 0} o < ω),
    Ordinal.lift.{u, 0} o < ℵ₀.ord
⊢ o < ℵ₀.ord

Tactic:
rcases Ordinal.lt_lift_iff.1 h with ⟨o, ho, rfl⟩

Premises used: Ordinal.lt_lift_iff, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{0}
ho : o < type fun (x1 x2 : ℕ) ↦ x1 < x2
h : Ordinal.lift.{u, 0} o < ω
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) :
          ℕ)) <
    ℵ₀
⊢ Ordinal.lift.{u, 0} o < ℵ₀.ord

Tactic:
rw [lt_ord, ← lift_card, lift_lt_aleph0, ← typein_enum _ ho]

Premises used: Ordinal.typein_enum, Cardinal.lift_lt_aleph0, Ordinal.lift_card, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{0}
ho : o < type fun (x1 x2 : ℕ) ↦ x1 < x2
h : Ordinal.lift.{u, 0} o < ω
⊢ 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:
lt_aleph0_iff_fintype.2 ⟨Set.fintypeLTNat _⟩

Premises used: Iff.mpr, Set.fintypeLTNat, Nonempty.intro, Cardinal.lt_aleph0_iff_fintype
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{0}
ho : o < type fun (x1 x2 : ℕ) ↦ x1 < x2
h : Ordinal.lift.{u, 0} o < ω
⊢ 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:
exact lt_aleph0_iff_fintype.2 ⟨Set.fintypeLTNat _⟩

Premises used: Iff.mpr, Set.fintypeLTNat, Nonempty.intro, Cardinal.lt_aleph0_iff_fintype
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c : Cardinal.{v}
⊢ Ordinal.lift.{u, v} c.ord = (lift.{u, v} c).ord

Tactic:
le_antisymm (le_of_forall_lt fun a ha => ?_) ?_

Premises used: le_of_forall_lt, le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Basic
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
refine_2 : (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord
⊢ Ordinal.lift.{u, v} c.ord = (lift.{u, v} c).ord

Tactic:
refine le_antisymm (le_of_forall_lt fun a ha => ?_) ?_

Premises used: le_of_forall_lt, le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c : Cardinal.{v}
a : Ordinal.{max v u}
ha : a < Ordinal.lift.{u, v} c.ord
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
⊢ a < (lift.{u, v} c).ord

Tactic:
rcases Ordinal.lt_lift_iff.1 ha with ⟨a, _, rfl⟩

Premises used: Ordinal.lt_lift_iff, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
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
refine_1₂ : a.card < c
refine_1₃ : a < c.ord
refine_1₄ refine_1₅ refine_1₆ refine_1₇ : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ Ordinal.lift.{u, v} a < (lift.{u, v} c).ord

Tactic:
rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]

Premises used: Ordinal.lift_lt, Cardinal.lift_lt, Ordinal.lift_card, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Ordinal.Basic
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
refine_2₂ refine_2₃ : lift.{u, v} c ≤ lift.{u, v} c
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord

Tactic:
rw [ord_le, ← lift_card, card_ord]

Premises used: Cardinal.ord_le, Cardinal.card_ord, Ordinal.lift_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c : Cardinal.{u_1}
⊢ #c.ord.ToType = c

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
x : α
h : (#α).ord = type r
rw : ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) x < type r
⊢ card (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) x) < #α

Tactic:
rw [← lt_ord, h]

Premises used: Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) x < type r

Tactic:
apply typein_lt_type

Premises used: Ordinal.typein_lt_type
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
inst : LinearOrder α
inst_1 : WellFoundedLT α
i : α
h : (#α).ord = type fun (x1 x2 : α) ↦ x1 < x2
⊢ #(↑(Iio i) : Type u) < #α

Tactic:
card_typein_lt (r := LT.lt) i h

Premises used: Set.Mem, setOf, Cardinal.card_typein_lt, Set.Iio
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedGT α
i : α
h : (#α).ord = type fun (x1 x2 : αᵒᵈ) ↦ x1 < x2
⊢ #(↑(Ioi i) : Type u_1) < #α

Tactic:
mk_Iio_lt (OrderDual.toDual i) h

Premises used: OrderDual.toDual, Set.Ioi, setOf, Cardinal.mk_Iio_lt, OrderDual, DFunLike.coe
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c : Cardinal.{u_1}
i : c.ord.ToType
⊢ #(↑(Iio i) : Type u_1) < c

Tactic:
simpa using mk_Iio_lt i

Premises used: Cardinal.mk_Iio_lt
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
c : Cardinal.{u_1}
x : c.ord.ToType
⊢ card
      ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : c.ord.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_1}) ↦
            x1 < x2) (typein fun (x1 x2 : c.ord.ToType) ↦ x1 < x2) :
          (a : c.ord.ToType) → Ordinal.{u_1})
        x) <
    c

Tactic:
mk_Iio_toType_ord_lt x

Premises used: Set.Mem, setOf, Cardinal.mk_Iio_toType_ord_lt, Set.Iio
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ a.ord = 0 ↔ a = 0

Tactic:
ord_injective.eq_iff' ord_zero

Premises used: Function.Injective.eq_iff', Cardinal.ord_zero, Cardinal.ord_injective
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ a.ord = 1 ↔ a = 1

Tactic:
ord_injective.eq_iff' ord_one

Premises used: Function.Injective.eq_iff', Cardinal.ord_one, Cardinal.ord_injective
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u_1}
rw : ord 0 < a.ord ↔ 0 < a
rw₁ rw₂ : 0 < a ↔ 0 < a
⊢ 0 < a.ord ↔ 0 < a

Tactic:
rw [← ord_zero, ord_lt_ord]

Premises used: Cardinal.ord_zero, Cardinal.ord_lt_ord
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u_1}
rw : ℵ₀.ord ≤ a.ord ↔ ℵ₀ ≤ a
rw₁ rw₂ : ℵ₀ ≤ a ↔ ℵ₀ ≤ a
⊢ ω ≤ a.ord ↔ ℵ₀ ≤ a

Tactic:
rw [← ord_aleph0, ord_le_ord]

Premises used: Cardinal.ord_aleph0, Cardinal.ord_le_ord
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u_1}
rw : a.ord ≤ ℵ₀.ord ↔ a ≤ ℵ₀
rw₁ rw₂ : a ≤ ℵ₀ ↔ a ≤ ℵ₀
⊢ a.ord ≤ ω ↔ a ≤ ℵ₀

Tactic:
rw [← ord_aleph0, ord_le_ord]

Premises used: Cardinal.ord_aleph0, Cardinal.ord_le_ord
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ a.ord < ω ↔ a < ℵ₀

Tactic:
le_iff_le_iff_lt_iff_lt.1 omega0_le_ord

Premises used: le_iff_le_iff_lt_iff_lt, Cardinal.omega0_le_ord, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ ω < a.ord ↔ ℵ₀ < a

Tactic:
le_iff_le_iff_lt_iff_lt.1 ord_le_omega0

Premises used: le_iff_le_iff_lt_iff_lt, Iff.mp, Cardinal.ord_le_omega0
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ a.ord = ω ↔ a = ℵ₀

Tactic:
ord_injective.eq_iff' ord_aleph0

Premises used: Cardinal.ord_aleph0, Function.Injective.eq_iff', Cardinal.ord_injective
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
⊢ (⇑orderEmbedding : (a : Cardinal.{u_1}) → Ordinal.{u_1}) = ord

Tactic:
rfl

Premises used: Cardinal.ord, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
rw : ord (↑n : Cardinal.{u_1}) ≤ o ↔ (↑n : Ordinal.{u_1}) ≤ o
rw₁ rw₂ : (↑n : Ordinal.{u_1}) ≤ o ↔ (↑n : Ordinal.{u_1}) ≤ o
⊢ (↑n : Cardinal.{u_1}) ≤ o.card ↔ (↑n : Ordinal.{u_1}) ≤ o

Tactic:
rw [← Cardinal.ord_le, Cardinal.ord_natCast]

Premises used: Cardinal.ord_le, Cardinal.ord_natCast
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ 1 ≤ o.card ↔ 1 ≤ o

Tactic:
simpa using nat_le_card (n := 1)

Premises used: Ordinal.nat_le_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n ≤ o.card ↔ OfNat.ofNat n ≤ o

Tactic:
nat_le_card

Premises used: Ordinal.nat_le_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
rw : ℵ₀.ord ≤ o ↔ ω ≤ o
rw₁ rw₂ : ω ≤ o ↔ ω ≤ o
⊢ ℵ₀ ≤ o.card ↔ ω ≤ o

Tactic:
rw [← ord_le, ord_aleph0]

Premises used: Cardinal.ord_aleph0, Cardinal.ord_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ o.card < ℵ₀ ↔ o < ω

Tactic:
le_iff_le_iff_lt_iff_lt.1 aleph0_le_card

Premises used: le_iff_le_iff_lt_iff_lt, Ordinal.aleph0_le_card, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
rw : (↑(n + 1) : Ordinal.{u_1}) ≤ o ↔ succ (↑n : Ordinal.{u_1}) ≤ o
⊢ (↑n : Cardinal.{u_1}) < o.card ↔ (↑n : Ordinal.{u_1}) < o

Tactic:
rw [← natCast_add_one_le_iff, ← succ_le_iff, ← Nat.cast_add_one, nat_le_card]

Premises used: Cardinal.natCast_add_one_le_iff, Ordinal.nat_le_card, Order.succ_le_iff, Nat.cast_add_one
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
⊢ (↑(n + 1) : Ordinal.{u_1}) ≤ o ↔ succ (↑n : Ordinal.{u_1}) ≤ o

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ 0 < o.card ↔ 0 < o

Tactic:
simpa using nat_lt_card (n := 0)

Premises used: Ordinal.nat_lt_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ 1 < o.card ↔ 1 < o

Tactic:
simpa using nat_lt_card (n := 1)

Premises used: Ordinal.nat_lt_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n < o.card ↔ OfNat.ofNat n < o

Tactic:
nat_lt_card

Premises used: Ordinal.nat_lt_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
⊢ o.card < (↑n : Cardinal.{u_1}) ↔ o < (↑n : Ordinal.{u_1})

Tactic:
lt_iff_lt_of_le_iff_le nat_le_card

Premises used: Ordinal.nat_le_card, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
inst : n.AtLeastTwo
⊢ o.card < OfNat.ofNat n ↔ o < OfNat.ofNat n

Tactic:
card_lt_nat

Premises used: Ordinal.card_lt_nat
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
⊢ o.card ≤ (↑n : Cardinal.{u_1}) ↔ o ≤ (↑n : Ordinal.{u_1})

Tactic:
le_iff_le_iff_lt_iff_lt.2 nat_lt_card

Premises used: Iff.mpr, le_iff_le_iff_lt_iff_lt, Ordinal.nat_lt_card
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ o.card ≤ 1 ↔ o ≤ 1

Tactic:
simpa using card_le_nat (n := 1)

Premises used: Ordinal.card_le_nat
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
inst : n.AtLeastTwo
⊢ o.card ≤ OfNat.ofNat n ↔ o ≤ OfNat.ofNat n

Tactic:
card_le_nat

Premises used: Ordinal.card_le_nat
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
⊢ o.card = (↑n : Cardinal.{u_1}) ↔ o = (↑n : Ordinal.{u_1})

Tactic:
simp only [le_antisymm_iff, card_le_nat, nat_le_card]

Premises used: Ordinal.nat_le_card, Ordinal.card_le_nat, le_antisymm_iff
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ o.card = 0 ↔ o = 0

Tactic:
simpa using card_eq_nat (n := 0)

Premises used: Ordinal.card_eq_nat
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ o.card = 1 ↔ o = 1

Tactic:
simpa using card_eq_nat (n := 1)

Premises used: Ordinal.card_eq_nat
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c < ℵ₀
rcases : ∀ (n : ℕ) (hc : (↑n : Cardinal.{u_1}) < ℵ₀), o ≤ ord (↑n : Cardinal.{u_1}) ↔ o.card ≤ (↑n : Cardinal.{u_1})
⊢ o ≤ c.ord ↔ o.card ≤ c

Tactic:
rcases lt_aleph0.mp hc with ⟨n, rfl⟩

Premises used: Iff.mp, Cardinal.lt_aleph0, rfl
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
hc : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ o ≤ ord (↑n : Cardinal.{u_1}) ↔ o.card ≤ (↑n : Cardinal.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u}
b : Ordinal.{max u v}
h : b.card ≤ Cardinal.lift.{v, u} a
⊢ b < lift.{v, u} (succ a).ord

Tactic:
rw [card_le_iff, ← lift_succ, ← lift_ord] at h

Premises used: Cardinal.lift_succ, Cardinal.card_le_iff, Cardinal.lift_ord
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < lift.{v, u} (succ a).ord
⊢ b ∈ range lift.{v, u}

Tactic:
mem_range_lift_of_le h.le

Premises used: Ordinal.mem_range_lift_of_le, Set.Mem, LT.lt.le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < lift.{v, u} (succ a).ord
⊢ b ∈ range lift.{v, u}

Tactic:
exact mem_range_lift_of_le h.le

Premises used: Ordinal.mem_range_lift_of_le, LT.lt.le
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
n : ℕ
inst : n.AtLeastTwo
⊢ o.card = OfNat.ofNat n ↔ o = OfNat.ofNat n

Tactic:
card_eq_nat

Premises used: Ordinal.card_eq_nat