awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (hypothesis)
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
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_2} R ↥S'
this : QuasiFinite.{u_1, u_2} R (Localization.Away r)
⊢ QuasiFiniteAt R p
have this₁ : QuasiFinite.{u_1, u_2} R (Localization.Away (↑r : S))
Tactic: have : Algebra.QuasiFinite R (Localization.Away r.1) :=
    .of_surjective_algHom (Localization.awayMapₐ S'.val r) H.2
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_2} R ↥S'
this_2 : QuasiFinite.{u_1, u_2} R (Localization.Away r)
this : QuasiFinite.{u_1, u_2} R (Localization.Away (↑r : S))
f : Localization.Away (↑r : S) →ₐ[S] Localization.AtPrime p :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers (↑r : S)) (f := ofId S (Localization.AtPrime p)) ⋯
⊢ QuasiFiniteAt R p
have refine : ∀ (x : Localization.AtPrime p),
  ∃ (s : Localization.Away (↑r : S)),
    IsUnit (M := Localization.AtPrime p)
        ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s :
          Localization.AtPrime p) ∧
      Membership.mem (γ := Subalgebra R (Localization.AtPrime p)) (AlgHom.range (AlgHom.restrictScalars R f))
        (HMul.hMul (β := Localization.AtPrime p) x
          ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s :
            Localization.AtPrime p))
Tactic: refine .of_forall_exists_mul_mem_range (f.restrictScalars R) fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
p : Ideal S
inst_4 : p.IsPrime
H_1 : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_2} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrp : (↑r : S) ∉ p
H :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_2} R ↥S'
this_2 : QuasiFinite.{u_1, u_2} R (Localization.Away r)
this : QuasiFinite.{u_1, u_2} R (Localization.Away (↑r : S))
f : Localization.Away (↑r : S) →ₐ[S] Localization.AtPrime p :=
  IsLocalization.liftAlgHom (R := S) (M := Submonoid.powers (↑r : S)) (f := ofId S (Localization.AtPrime p)) ⋯
x : Localization.AtPrime p
⊢ ∃ (s : Localization.Away (↑r : S)),
    IsUnit (M := Localization.AtPrime p)
        ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s :
          Localization.AtPrime p) ∧
      Membership.mem (γ := Subalgebra R (Localization.AtPrime p)) (AlgHom.range (AlgHom.restrictScalars R f))
        (HMul.hMul (β := Localization.AtPrime p) x
          ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s :
            Localization.AtPrime p))
have obtain : ∀ (x s : S) (hs : s ∈ p.primeCompl),
  ∃ (s_1 : Localization.Away (↑r : S)),
    IsUnit (M := Localization.AtPrime p)
        ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s_1 :
          Localization.AtPrime p) ∧
      Membership.mem (γ := Subalgebra R (Localization.AtPrime p)) (AlgHom.range (AlgHom.restrictScalars R f))
        (HMul.hMul (α := Localization.AtPrime p) (β := Localization.AtPrime p)
          (IsLocalization.mk' (Localization.AtPrime p) x (Subtype.mk (p := fun (x : S) ↦ x ∈ p.primeCompl) s hs) :
            Localization.AtPrime p)
          ((AlgHom.restrictScalars R f : (a : Localization.Away (↑r : S)) → Localization.AtPrime p) s_1 :
            Localization.AtPrime p))
Tactic: obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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 :
  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 ⋯}
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 R q.asIdeal
have 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 sorry)))
Tactic: suffices Algebra.QuasiFiniteAt p.asIdeal.ResidueField (e ⟨q, rfl⟩).asIdeal from
    .of_quasiFiniteAt_residueField _ q.asIdeal (e ⟨q, rfl⟩).asIdeal
      congr($(e.symm_apply_apply ⟨q, rfl⟩).1.asIdeal)
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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 :
  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 ⋯}
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 ⋯)))
have refine : 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)) {p}) x)
          q sorry) :
      PrimeSpectrum (p.asIdeal.Fiber S)))
Tactic: refine .of_isOpen_singleton _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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 :
  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 ⋯}
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
⊢ 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)) {p}) x)
            q ⋯) :
        PrimeSpectrum (p.asIdeal.Fiber S)))
have rwa : IsOpen (X := PrimeSpectrum (p.asIdeal.Fiber S))
  (Set.image (α :=
    { x : PrimeSpectrum S //
      Membership.mem (γ := Set (PrimeSpectrum S))
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {p}) x })
    (⇑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 sorry})
Tactic: rwa [← Set.image_singleton, e.isOpen_image]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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 ⋯}
have 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 sorry}
Tactic: refine ⟨fun H ↦ ?_, .of_isOpen_singleton_fiber q⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ 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 ⋯}
have 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 sorry) :
      PrimeSpectrum (p.asIdeal.Fiber S)))
Tactic: rw [← e.isOpen_image, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.ZariskisMainTheorem (goal)
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
⊢ 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)))
have 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 sorry)))
Tactic: suffices Algebra.QuasiFiniteAt p.asIdeal.ResidueField (e ⟨q, rfl⟩).asIdeal from
    (QuasiFiniteAt.isClopen_singleton (R := p.asIdeal.ResidueField) _).isOpen
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : o.IsInitial
c : Cardinal.{u_1}
⊢ o ≤ c.ord ↔ o.card ≤ c
have grw : o ≤ c.ord ↔ o.card.ord ≤ c.ord
Tactic: grw [← ord_le_ord, ho.ord_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : o.IsInitial
c : Cardinal.{u_1}
grw : o ≤ c.ord ↔ o.card.ord ≤ c.ord
⊢ o ≤ c.ord ↔ o.card ≤ c
have grw₁ : o ≤ c.ord ↔ o ≤ c.ord
Tactic: grw [← ord_le_ord, ho.ord_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a b : Ordinal.{u_1}
ha : a.IsInitial
⊢ a.card ≤ b.card ↔ a ≤ b
have refine : ∀ (h : a.card ≤ b.card), a ≤ b
Tactic: refine ⟨fun h ↦ ?_, Ordinal.card_le_card⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (hypothesis)
Goal:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a.card ≤ b.card
⊢ a ≤ b
have h₁ : a ≤ b.card.ord
Tactic: rw [← ha.le_ord_iff_card_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a ≤ b.card.ord
⊢ a ≤ b
have grw : b.card.ord ≤ b
Tactic: grw [h, ord_card_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a ≤ b.card.ord
grw : b.card.ord ≤ b
⊢ a ≤ b
have grw₁ : b ≤ b
Tactic: grw [h, ord_card_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
⊢ IsInitial.{u_1} c.ord
have rw : c.ord.card.ord = c.ord
Tactic: rw [IsInitial, card_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
rw : c.ord.card.ord = c.ord
⊢ IsInitial.{u_1} c.ord
have rw₁ : c.ord = c.ord
Tactic: rw [IsInitial, card_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
n : ℕ
⊢ IsInitial.{u_1} (↑n : Ordinal.{u_1})
have rw : (card (↑n : Ordinal.{u_1})).ord = (↑n : Ordinal.{u_1})
Tactic: rw [IsInitial, card_nat, ord_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
n : ℕ
rw : (card (↑n : Ordinal.{u_1})).ord = (↑n : Ordinal.{u_1})
⊢ IsInitial.{u_1} (↑n : Ordinal.{u_1})
have rw₁ : ord (↑n : Cardinal.{u_1}) = (↑n : Ordinal.{u_1})
Tactic: rw [IsInitial, card_nat, ord_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
n : ℕ
rw : (card (↑n : Ordinal.{u_1})).ord = (↑n : Ordinal.{u_1})
rw₁ : ord (↑n : Cardinal.{u_1}) = (↑n : Ordinal.{u_1})
⊢ IsInitial.{u_1} (↑n : Ordinal.{u_1})
have rw₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
Tactic: rw [IsInitial, card_nat, ord_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ ω.IsInitial
have rw : ω.card.ord = ω
Tactic: rw [IsInitial, card_omega0, ord_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
rw : ω.card.ord = ω
⊢ ω.IsInitial
have rw₁ : ℵ₀.ord = ω
Tactic: rw [IsInitial, card_omega0, ord_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
rw : ω.card.ord = ω
rw₁ : ℵ₀.ord = ω
⊢ ω.IsInitial
have rw₂ : ω = ω
Tactic: rw [IsInitial, card_omega0, ord_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (hypothesis)
Goal:
a : Ordinal.{u_1}
ha : Membership.mem (γ := Set Ordinal.{u_1}) (upperBounds {x : Ordinal.{u_1} | x.IsInitial}) a
⊢ False
have this : (succ a.card).ord ≤ a
Tactic: have := ha (isInitial_ord (succ a.card))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (hypothesis)
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
⊢ False
have this₁ : succ a.card ≤ a.card
Tactic: rw [ord_le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0) 0
have rw : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sInf {x : Ordinal.{u_1} | x.IsInitial}) 0
Tactic: rw [coe_preOmega, enumOrd_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
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})
have succ : 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 (le_preOmega_self _).antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
n : ℕ
IH :
  Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) (↑n : 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})
have apply : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) (↑(n + 1) : Ordinal.{u_1})
Tactic: apply enumOrd_succ_le not_bddAbove_isInitial (isInitial_natCast _) (IH.trans_lt _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
n : ℕ
IH :
  Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) (↑n : Ordinal.{u_1})
⊢ LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) (↑(n + 1) : Ordinal.{u_1})
have rw : n < n + 1
Tactic: rw [Nat.cast_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
n : ℕ
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) (↑n : Ordinal.{u_1})
have zero : Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑0 : Ordinal.{u_1})) (↑0 : 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
n : ℕ
zero :
  Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑0 : Ordinal.{u_1})) (↑0 : Ordinal.{u_1})
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) (↑n : Ordinal.{u_1})
have 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})
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ IsNormal (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (⇑preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1})
have 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
Tactic: rw [isNormal_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
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
have 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
Tactic: refine ⟨preOmega_strictMono, fun o ho a ha ↦
    (preOmega_le_of_forall_lt (isInitial_ord _) fun b hb ↦ ?_).trans (ord_card_le a)⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
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
⊢ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b < a.card.ord
have rw : card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b) < a.card
Tactic: rw [← (isInitial_ord _).card_lt_card, card_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
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
⊢ card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b) < a.card
have apply : card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b) <
  card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (succ b))
Tactic: apply lt_of_lt_of_le _ (card_le_card <| ha _ (ho.succ_lt hb))