awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
q : PrimeSpectrum S
⊢ QuasiFiniteAt R q.asIdeal ↔
    IsOpen (X :=
      (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {PrimeSpectrum.comap (algebraMap R S) q}) :
        Type u_2))
      {Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
              {PrimeSpectrum.comap (algebraMap R S) q})
            x)
          q ⋯}

Tactic:
⟨fun H ↦ ?_, .of_isOpen_singleton_fiber q⟩

Premises used: Algebra.QuasiFiniteAt.of_isOpen_singleton_fiber, Iff.intro
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
q : PrimeSpectrum S
refine :
  ∀ (H : QuasiFiniteAt R q.asIdeal),
    IsOpen (X :=
      (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {PrimeSpectrum.comap (algebraMap R S) q}) :
        Type u_2))
      {Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
              {PrimeSpectrum.comap (algebraMap R S) q})
            x)
          q ⋯}
⊢ QuasiFiniteAt R q.asIdeal ↔
    IsOpen (X :=
      (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {PrimeSpectrum.comap (algebraMap R S) q}) :
        Type u_2))
      {Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
              {PrimeSpectrum.comap (algebraMap R S) q})
            x)
          q ⋯}

Tactic:
refine ⟨fun H ↦ ?_, .of_isOpen_singleton_fiber q⟩
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
q : PrimeSpectrum S
H : QuasiFiniteAt R q.asIdeal
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) : Type u_2) ≃ₜ
  PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
rw :
  IsOpen (X := PrimeSpectrum (p.asIdeal.Fiber S))
    (singleton (α := PrimeSpectrum (p.asIdeal.Fiber S))
      ((e : (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
            Membership.mem (γ := Set (PrimeSpectrum S))
              (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                {PrimeSpectrum.comap (algebraMap R S) q})
              x)
            q ⋯) :
        PrimeSpectrum (p.asIdeal.Fiber S)))
⊢ IsOpen (X :=
    (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          {PrimeSpectrum.comap (algebraMap R S) q}) :
      Type u_2))
    {Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
        Membership.mem (γ := Set (PrimeSpectrum S))
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
            {PrimeSpectrum.comap (algebraMap R S) q})
          x)
        q ⋯}

Tactic:
rw [← e.isOpen_image, Set.image_singleton]

Premises used: Set.image_singleton, Homeomorph.isOpen_image
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
q : PrimeSpectrum S
H : QuasiFiniteAt R q.asIdeal
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) : Type u_2) ≃ₜ
  PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
suffices :
  QuasiFiniteAt p.asIdeal.ResidueField (S := p.asIdeal.Fiber S)
    (PrimeSpectrum.asIdeal
      ((e : (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x)
          q ⋯)))
⊢ IsOpen (X := PrimeSpectrum (p.asIdeal.Fiber S))
    (singleton (α := PrimeSpectrum (p.asIdeal.Fiber S))
      ((e : (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
          (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
            Membership.mem (γ := Set (PrimeSpectrum S))
              (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                {PrimeSpectrum.comap (algebraMap R S) q})
              x)
            q ⋯) :
        PrimeSpectrum (p.asIdeal.Fiber S)))

Tactic:
suffices Algebra.QuasiFiniteAt p.asIdeal.ResidueField (e ⟨q, rfl⟩).asIdeal from
    (QuasiFiniteAt.isClopen_singleton (R := p.asIdeal.ResidueField) _).isOpen
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
q : PrimeSpectrum S
H : QuasiFiniteAt R q.asIdeal
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) : Type u_2) ≃ₜ
  PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
⊢ QuasiFiniteAt p.asIdeal.ResidueField (S := p.asIdeal.Fiber S)
    (PrimeSpectrum.asIdeal
      ((e : (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x)
          q ⋯)))

Tactic:
.baseChange q.asIdeal _ congr($(e.symm_apply_apply ⟨q, rfl⟩).1.asIdeal).symm

Premises used: Algebra.QuasiFiniteAt.baseChange, congrArg, id, Subtype.mk, Homeomorph.symm_apply_apply, Eq.symm, Subtype.val, PrimeSpectrum.asIdeal, rfl
-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
q : PrimeSpectrum S
H : QuasiFiniteAt R q.asIdeal
p : PrimeSpectrum R := PrimeSpectrum.comap (algebraMap R S) q
e : (↑(Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) : Type u_2) ≃ₜ
  PrimeSpectrum (p.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S p
⊢ QuasiFiniteAt p.asIdeal.ResidueField (S := p.asIdeal.Fiber S)
    (PrimeSpectrum.asIdeal
      ((e : (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p}) : Type u_2)) → PrimeSpectrum (p.asIdeal.Fiber S))
        (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x)
          q ⋯)))

Tactic:
exact .baseChange q.asIdeal _ congr($(e.symm_apply_apply ⟨q, rfl⟩).1.asIdeal).symm
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
h : o.IsInitial
⊢ o.card.ord = o

Tactic:
h

Premises used: Ordinal.IsInitial
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : o.IsInitial
c : Cardinal.{u_1}
grw : o ≤ c.ord ↔ o.card.ord ≤ c.ord
grw₁ grw₂ : o ≤ c.ord ↔ o ≤ c.ord
⊢ o ≤ c.ord ↔ o.card ≤ c

Tactic:
grw [← ord_le_ord, ho.ord_card]

Premises used: Ordinal.IsInitial.ord_card, Cardinal.ord_le_ord
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a b : Ordinal.{u_1}
ha : a.IsInitial
⊢ a.card ≤ b.card ↔ a ≤ b

Tactic:
⟨fun h ↦ ?_, Ordinal.card_le_card⟩

Premises used: Ordinal.card_le_card, Iff.intro
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a b : Ordinal.{u_1}
ha : a.IsInitial
refine : ∀ (h : a.card ≤ b.card), a ≤ b
⊢ a.card ≤ b.card ↔ a ≤ b

Tactic:
refine ⟨fun h ↦ ?_, Ordinal.card_le_card⟩
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a.card ≤ b.card
⊢ a ≤ b.card.ord

Tactic:
rw [← ha.le_ord_iff_card_le] at h

Premises used: Ordinal.IsInitial.le_ord_iff_card_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a ≤ b.card.ord
grw : b.card.ord ≤ b
grw₁ grw₂ : b ≤ b
⊢ a ≤ b

Tactic:
grw [h, ord_card_le]

Premises used: Cardinal.ord_card_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a b : Ordinal.{u_1}
hb : b.IsInitial
⊢ a.card < b.card ↔ a < b

Tactic:
lt_iff_lt_of_le_iff_le hb.card_le_card

Premises used: Ordinal.IsInitial.card_le_card, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
rw : c.ord.card.ord = c.ord
rw₁ rw₂ : c.ord = c.ord
⊢ IsInitial.{u_1} c.ord

Tactic:
rw [IsInitial, card_ord]

Premises used: Ordinal.IsInitial, Cardinal.card_ord
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
rw : (card (↑n : Ordinal.{u_1})).ord = (↑n : Ordinal.{u_1})
rw₁ : ord (↑n : Cardinal.{u_1}) = (↑n : Ordinal.{u_1})
rw₂ rw₃ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
⊢ IsInitial.{u_1} (↑n : Ordinal.{u_1})

Tactic:
rw [IsInitial, card_nat, ord_natCast]

Premises used: Ordinal.IsInitial, Cardinal.ord_natCast, Ordinal.card_nat
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ IsInitial.{u_1} 0

Tactic:
exact_mod_cast isInitial_natCast 0

Premises used: Ordinal.isInitial_natCast, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ IsInitial.{u_1} 1

Tactic:
exact_mod_cast isInitial_natCast 1

Premises used: Ordinal.isInitial_natCast, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
rw : ω.card.ord = ω
rw₁ : ℵ₀.ord = ω
rw₂ rw₃ : ω = ω
⊢ ω.IsInitial

Tactic:
rw [IsInitial, card_omega0, ord_aleph0]

Premises used: Cardinal.ord_aleph0, Ordinal.card_omega0, Ordinal.IsInitial
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
hwo : ¬o < ω
⊢ (succ o).card.ord < succ o

Tactic:
simp_all [ord_card_le]

Premises used: Cardinal.ord_card_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : Ordinal.{u_1}
ha : Membership.mem (γ := Set Ordinal.{u_1}) (upperBounds {x : Ordinal.{u_1} | x.IsInitial}) a
⊢ (succ a.card).ord ≤ a

Tactic:
have := ha (isInitial_ord (succ a.card))
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : Ordinal.{u_1}
ha : Membership.mem (γ := Set Ordinal.{u_1}) (upperBounds {x : Ordinal.{u_1} | x.IsInitial}) a
this : (succ a.card).ord ≤ a
⊢ succ a.card ≤ a.card

Tactic:
rw [ord_le] at this

Premises used: Cardinal.ord_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : Ordinal.{u_1}
ha : Membership.mem (γ := Set Ordinal.{u_1}) (upperBounds {x : Ordinal.{u_1} | x.IsInitial}) a
this : succ a.card ≤ a.card
⊢ False

Tactic:
(lt_succ _).not_ge this

Premises used: Order.lt_succ, LT.lt.not_ge
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : Ordinal.{u_1}
ha : Membership.mem (γ := Set Ordinal.{u_1}) (upperBounds {x : Ordinal.{u_1} | x.IsInitial}) a
this : succ a.card ≤ a.card
⊢ False

Tactic:
exact (lt_succ _).not_ge this

Premises used: Order.lt_succ, LT.lt.not_ge
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ (⇑preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) = enumOrd {x : Ordinal.{u_1} | x.IsInitial}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ StrictMono (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (⇑preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1})

Tactic:
preOmega.strictMono

Premises used: OrderEmbedding.strictMono, Ordinal.preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ LT.lt (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o₁ : Ordinal.{u_1})
      ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o₂ : Ordinal.{u_1}) ↔
    o₁ < o₂

Tactic:
preOmega.lt_iff_lt

Premises used: OrderEmbedding.lt_iff_lt, Ordinal.preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ LE.le (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o₁ : Ordinal.{u_1})
      ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o₂ : Ordinal.{u_1}) ↔
    o₁ ≤ o₂

Tactic:
preOmega.le_iff_le

Premises used: OrderEmbedding.le_iff_le, Ordinal.preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (max o₁ o₂) : Ordinal.{u_1})
    (max ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o₁) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o₂) :
      Ordinal.{u_1})

Tactic:
preOmega.monotone.map_max

Premises used: OrderEmbedding.monotone, Monotone.map_max, Ordinal.preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ IsInitial.{u_1} ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o)

Tactic:
enumOrd_mem not_bddAbove_isInitial o

Premises used: Set.Mem, Ordinal.not_bddAbove_isInitial, setOf, Ordinal.enumOrd_mem, Ordinal.IsInitial
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ o ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o

Tactic:
preOmega_strictMono.le_apply

Premises used: StrictMono.le_apply, Ordinal.preOmega_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
rw : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sInf {x : Ordinal.{u_1} | x.IsInitial}) 0
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0) 0

Tactic:
rw [coe_preOmega, enumOrd_zero]

Premises used: Ordinal.enumOrd_zero, Ordinal.coe_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sInf {x : Ordinal.{u_1} | x.IsInitial}) 0

Tactic:
csInf_eq_bot_of_bot_mem isInitial_zero

Premises used: csInf_eq_bot_of_bot_mem, Ordinal.isInitial_zero
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sInf {x : Ordinal.{u_1} | x.IsInitial}) 0

Tactic:
exact csInf_eq_bot_of_bot_mem isInitial_zero

Premises used: csInf_eq_bot_of_bot_mem
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑0 : Ordinal.{u_1})) (↑0 : Ordinal.{u_1})

Tactic:
preOmega_zero

Premises used: Ordinal.preOmega_zero, Nat.unaryCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑0 : Ordinal.{u_1})) (↑0 : Ordinal.{u_1})

Tactic:
exact preOmega_zero

Premises used: Ordinal.preOmega_zero
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
IH :
  Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) (↑n : Ordinal.{u_1})
succ :
  LE.le (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑(n + 1) : Ordinal.{u_1}))
    (↑(n + 1) : Ordinal.{u_1})
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑(n + 1) : Ordinal.{u_1}))
    (↑(n + 1) : Ordinal.{u_1})

Tactic:
apply (le_preOmega_self _).antisymm'

Premises used: LE.le.antisymm', Ordinal.le_preOmega_self
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
IH :
  Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) (↑n : Ordinal.{u_1})
apply : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) (↑(n + 1) : Ordinal.{u_1})
⊢ LE.le (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑(n + 1) : Ordinal.{u_1}))
    (↑(n + 1) : Ordinal.{u_1})

Tactic:
apply enumOrd_succ_le not_bddAbove_isInitial (isInitial_natCast _) (IH.trans_lt _)

Premises used: Ordinal.not_bddAbove_isInitial, Ordinal.enumOrd_succ_le, Ordinal.isInitial_natCast, Eq.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
IH :
  Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) (↑n : Ordinal.{u_1})
rw : n < n + 1
⊢ LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) (↑(n + 1) : Ordinal.{u_1})

Tactic:
rw [Nat.cast_lt]

Premises used: Nat.cast_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
IH :
  Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) (↑n : Ordinal.{u_1})
⊢ n < n + 1

Tactic:
lt_succ n

Premises used: Order.succ, Order.lt_succ
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
IH :
  Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) (↑n : Ordinal.{u_1})
⊢ n < n + 1

Tactic:
exact lt_succ n

Premises used: Order.lt_succ
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
zero :
  Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑0 : Ordinal.{u_1})) (↑0 : Ordinal.{u_1})
succ :
  ∀ (n : ℕ)
    (IH :
      Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1}))
        (↑n : Ordinal.{u_1})),
    Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑(n + 1) : Ordinal.{u_1}))
      (↑(n + 1) : Ordinal.{u_1})
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) (↑n : Ordinal.{u_1})

Tactic:
induction n with
  | zero => exact preOmega_zero
  | succ n IH =>
    apply (le_preOmega_self _).antisymm'
    apply enumOrd_succ_le not_bddAbove_isInitial (isInitial_natCast _) (IH.trans_lt _)
    rw [Nat.cast_lt]
    exact lt_succ n

Premises used: Order.succ, LE.le.antisymm', Order.lt_succ, Ordinal.preOmega_zero, Ordinal.le_preOmega_self, Ordinal.zero, Nat.cast_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (OfNat.ofNat n)) (↑n : Ordinal.{u_1})

Tactic:
preOmega_natCast n

Premises used: Ordinal.preOmega_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o a : Ordinal.{u_1}
ha : a.IsInitial
H : ∀ b < o, (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b < a
⊢ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o ≤ a

Tactic:
enumOrd_le_of_forall_lt ha H

Premises used: Ordinal.enumOrd_le_of_forall_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
rw :
  StrictMono (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (⇑preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ∧
    ∀ (o : Ordinal.{u_1}),
      IsSuccLimit o →
        ∀ (a : Ordinal.{u_1}),
          (∀ b < o, (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b ≤ a) →
            (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o ≤ a
⊢ IsNormal (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (⇑preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1})

Tactic:
rw [isNormal_iff]

Premises used: Order.isNormal_iff
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ StrictMono (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (⇑preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ∧
    ∀ (o : Ordinal.{u_1}),
      IsSuccLimit o →
        ∀ (a : Ordinal.{u_1}),
          (∀ b < o, (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b ≤ a) →
            (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o ≤ a

Tactic:
⟨preOmega_strictMono, fun o ho a ha ↦
    (preOmega_le_of_forall_lt (isInitial_ord _) fun b hb ↦ ?_).trans (ord_card_le a)⟩

Premises used: Ordinal.isInitial_ord, Ordinal.card, And.intro, Ordinal.preOmega_strictMono, Ordinal.preOmega_le_of_forall_lt, LE.le.trans, Cardinal.ord_card_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
refine :
  ∀ (o : Ordinal.{u_1}) (ho : IsSuccLimit o) (a : Ordinal.{u_1})
    (ha : ∀ b < o, (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b ≤ a) (b : Ordinal.{u_1}) (hb : b < o),
    (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b < a.card.ord
⊢ StrictMono (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (⇑preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ∧
    ∀ (o : Ordinal.{u_1}),
      IsSuccLimit o →
        ∀ (a : Ordinal.{u_1}),
          (∀ b < o, (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b ≤ a) →
            (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o ≤ a

Tactic:
refine ⟨preOmega_strictMono, fun o ho a ha ↦
    (preOmega_le_of_forall_lt (isInitial_ord _) fun b hb ↦ ?_).trans (ord_card_le a)⟩
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b ≤ a
b : Ordinal.{u_1}
hb : b < o
rw : card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b) < a.card
⊢ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b < a.card.ord

Tactic:
rw [← (isInitial_ord _).card_lt_card, card_ord]

Premises used: Ordinal.isInitial_ord, Ordinal.IsInitial.card_lt_card, Cardinal.card_ord
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b ≤ a
b : Ordinal.{u_1}
hb : b < o
apply :
  card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b) <
    card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (succ b))
⊢ card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b) < a.card

Tactic:
apply lt_of_lt_of_le _ (card_le_card <| ha _ (ho.succ_lt hb))

Premises used: Ordinal.card_le_card, Order.IsSuccLimit.succ_lt, lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b ≤ a
b : Ordinal.{u_1}
hb : b < o
rw : b < succ b
⊢ card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b) <
    card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (succ b))

Tactic:
rw [(isInitial_preOmega _).card_lt_card, preOmega_lt_preOmega]

Premises used: Ordinal.isInitial_preOmega, Ordinal.IsInitial.card_lt_card, Ordinal.preOmega_lt_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ b < succ b

Tactic:
lt_succ b

Premises used: Order.lt_succ
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ b < succ b

Tactic:
exact lt_succ b

Premises used: Order.lt_succ
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ Eq (α := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}))
    {x : Ordinal.{u_1} | x.IsInitial}

Tactic:
range_enumOrd not_bddAbove_isInitial

Premises used: Ordinal.not_bddAbove_isInitial, Ordinal.range_enumOrd
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
x : Ordinal.{u_1}
rw : Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | x.IsInitial} x ↔ x.IsInitial
rw₁ rw₂ : x.IsInitial ↔ x.IsInitial
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}))
      x ↔
    x.IsInitial

Tactic:
rw [range_preOmega, mem_setOf]

Premises used: Set.mem_setOf, Ordinal.range_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
simp_rw : ⨆ (n : ℕ), (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1}) = ω
simp_rw₁ : ⨆ (n : ℕ), (↑n : Ordinal.{u_1}) = ω
⊢ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ω = ω

Tactic:
simp_rw [← apply_omega0_of_isNormal isNormal_preOmega, preOmega_natCast, iSup_natCast]

Premises used: Ordinal.isNormal_preOmega, Ordinal.iSup_natCast, Ordinal.apply_omega0_of_isNormal, Ordinal.preOmega_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
x : Ordinal.{u_1}
rw : ω ≤ x
| ω ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x

Tactic:
rw [← preOmega_omega0, preOmega_le_preOmega]

Premises used: Ordinal.preOmega_le_preOmega, Ordinal.preOmega_omega0
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
x : Ordinal.{u_1}
conv_lhs : ω ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω ≤ x
conv_lhs₁ : ω ≤ x ↔ ω ≤ x
⊢ ω ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω ≤ x

Tactic:
conv_lhs => rw [← preOmega_omega0, preOmega_le_preOmega]

Premises used: Ordinal.preOmega_le_preOmega, Ordinal.preOmega_omega0