awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
refine_1 :
  ∀ (h : IsNormal (enumOrd s)) {ι : Type u} (hι : Nonempty ι) (f : ι → Ordinal.{u}) (hf : ∀ (i : ι), f i ∈ s),
    ⨆ (i : ι), f i ∈ s
⊢ IsNormal (enumOrd s) ↔ IsClosed s
have refine_2 : ∀ (h : IsClosed s) (a : Ordinal.{u}) (ha : IsSuccLimit a) (o : Ordinal.{u}) (H : ∀ b < a, enumOrd s b ≤ o),
  enumOrd s a ≤ o
Tactic: refine
    ⟨fun h => isClosed_iff_iSup.2 fun {ι} hι f hf => ?_, fun h =>
      isNormal_iff.2 ⟨Hs, fun a ha o H => ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
this : enumOrd s (⨆ (i : ι), g i) = ⨆ (i : ι), f i
⊢ ⨆ (i : ι), f i ∈ s
have rw : enumOrd s (⨆ (i : ι), g i) ∈ s
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
⊢ ⨆ (i : ι), f i ∈ s
have refine_1 : enumOrd s (⨆ (i : ι), g i) = ⨆ (i : ι), f i
Tactic: suffices enumOrd s (⨆ i, g i) = ⨆ i, f i by
      rw [← this]
      exact enumOrd_mem hs _
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
⊢ enumOrd s (⨆ (i : ι), g i) = ⨆ (i : ι), f i
have refine_1 : Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i : ι), enumOrd s (g i)) (⨆ (i : ι), f i)
Tactic: rw [h.map_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i : ι), enumOrd s (g i)) (⨆ (i : ι), f i)
have refine_1 : Eq.{u + 2} (α := ι → Ordinal.{u}) (fun (i : ι) ↦ enumOrd s (g i)) fun (i : ι) ↦ f i
Tactic: congr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
⊢ Eq.{u + 2} (α := ι → Ordinal.{u}) (fun (i : ι) ↦ enumOrd s (g i)) fun (i : ι) ↦ f i
have refine_1 : ∀ (x : ι), enumOrd s (g x) = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} :=
  fun (i : ι) ↦
    ((enumOrdOrderIso s hs).symm : (a : (↑s : Type (u + 1))) → Ordinal.{u})
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f i) ⋯)
x : ι
⊢ (↑((enumOrdOrderIso s hs : (a : Ordinal.{u}) → (↑s : Type (u + 1))) (g x)) : Ordinal.{u}) = f x
have refine_1 : (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ s) (f x) sorry) : Ordinal.{u}) = f x
Tactic: rw [OrderIso.apply_symm_apply]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (hypothesis)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
⊢ enumOrd s a ≤ o
have this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
Tactic: have := csSup_mem_closure (ha.nonempty_Iio.image (enumOrd s)) bddAbove_of_small
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
⊢ enumOrd s a ≤ o
have refine_2 : enumOrd s '' Set.Iio a ⊆ s
Tactic: have := h.closure_eq ▸ closure_mono (t := s) ?_ this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
refine_2 : enumOrd s '' Set.Iio a ⊆ s
⊢ enumOrd s a ≤ o
have refine_2₁ : ∀ (this : sSup (enumOrd s '' Set.Iio a) ∈ s), enumOrd s a ≤ o
Tactic: have := h.closure_eq ▸ closure_mono (t := s) ?_ this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
⊢ enumOrd s '' Set.Iio a ⊆ s
have refine_2 : Set.range (enumOrd s) = s
Tactic: apply (Set.image_subset_range ..).trans_eq
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
⊢ Set.range (enumOrd s) = s
have refine_2 : s = s
Tactic: rw [range_enumOrd hs]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this_1 : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ enumOrd s a ≤ o
have refine_2 : sSup (enumOrd s '' Set.Iio a) ≤ o
Tactic: apply (enumOrd_le_of_forall_lt this _).trans
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this_1 : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
refine_2 : sSup (enumOrd s '' Set.Iio a) ≤ o
⊢ enumOrd s a ≤ o
have apply : ∀ b < a, enumOrd s b < sSup (enumOrd s '' Set.Iio a)
Tactic: apply (enumOrd_le_of_forall_lt this _).trans
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this_1 : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ sSup (enumOrd s '' Set.Iio a) ≤ o
have refine_2 : o ∈ upperBounds (enumOrd s '' Set.Iio a)
Tactic: apply csSup_le'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ AccPt o (𝓟 S) ↔ ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
have mp : AccPt o (𝓟 S) → ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
mp : AccPt o (𝓟 S) → ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ AccPt o (𝓟 S) ↔ ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
have mpr : (¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty) → AccPt o (𝓟 S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ AccPt o (𝓟 S) → ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
have mp : (∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o) → ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
Tactic: rw [accPt_iff_nhds]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
⊢ ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
have mp : ¬o = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
mp : ¬o = 0
⊢ ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
have mp₁ : ∀ p < o, (S ∩ Ioo p o).Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
S : Set Ordinal.{u_1}
h : ∀ (U : Set Ordinal.{u_1}), Membership.mem (γ := Filter Ordinal.{u_1}) (𝓝 0) U → ∃ y ∈ U ∩ S, y ≠ 0
⊢ False
have mp : ∀ (x : Ordinal.{u_1}) (hx : x ∈ Iio 1 ∩ S ∧ x ≠ 0), False
Tactic: obtain ⟨x, hx⟩ := h (Iio 1) (Iio_mem_nhds zero_lt_one)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
⊢ (S ∩ Ioo p o).Nonempty
have mp : ∀ (x : Ordinal.{u_1}) (hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o), (S ∩ Ioo p o).Nonempty
Tactic: obtain ⟨x, hx⟩ := h (Ioo p (o + 1)) <| Ioo_mem_nhds plt (lt_succ o)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
⊢ (S ∩ Ioo p o).Nonempty
have h₁ : x ∈ S ∩ Ioo p o
Tactic: use x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
⊢ x ∈ S ∩ Ioo p o
have h₁ : x ≤ o
Tactic: refine ⟨hx.1.2, ⟨hx.1.1.1, lt_of_le_of_ne ?_ hx.2⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (hypothesis)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
⊢ x ≤ o
have this : x < o + 1
Tactic: have := hx.1.1.2
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
this : x < o + 1
⊢ x ≤ o
have h₁ : ∀ (this : x < succ o), x ≤ o
Tactic: rwa [← succ_eq_add_one, lt_succ_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
p : Ordinal.{u_1}
plt : p < o
x : Ordinal.{u_1}
hx : x ∈ Ioo p (o + 1) ∩ S ∧ x ≠ o
this : x < o + 1
h₁ : ∀ (this : x < succ o), x ≤ o
⊢ x ≤ o
have h₂ : ∀ (this : x ≤ o), x ≤ o
Tactic: rwa [← succ_eq_add_one, lt_succ_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
⊢ (¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty) → AccPt o (𝓟 S)
have mpr : (¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty) → ∀ U ∈ 𝓝 o, ∃ y ∈ U ∩ S, y ≠ o
Tactic: rw [accPt_iff_nhds]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
⊢ ∃ y ∈ u ∩ S, y ≠ o
have mpr : ∀ (l : Ordinal.{u_1}) (hl : l < o ∧ Ioc l o ⊆ u), ∃ y ∈ u ∩ S, y ≠ o
Tactic: obtain ⟨l, hl⟩ := exists_Ioc_subset_of_mem_nhds umem ⟨0, pos_iff_ne_zero.mpr h.1⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
⊢ ∃ y ∈ u ∩ S, y ≠ o
have mpr : ∀ (x : Ordinal.{u_1}) (hx : x ∈ S ∩ Ioo l o), ∃ y ∈ u ∩ S, y ≠ o
Tactic: obtain ⟨x, hx⟩ := h.2 l hl.1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : ¬o = 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
u : Set Ordinal.{u_1}
umem : u ∈ 𝓝 o
l : Ordinal.{u_1}
hl : l < o ∧ Ioc l o ⊆ u
x : Ordinal.{u_1}
hx : x ∈ S ∩ Ioo l o
⊢ ∃ y ∈ u ∩ S, y ≠ o
have h₁ : x ∈ u ∩ S ∧ x ≠ o
Tactic: use x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (hypothesis)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o.IsAcc S
⊢ IsSuccLimit o
have h₁ : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
Tactic: rw [isAcc_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ IsSuccLimit o
have rw : o ≠ 0 ∧ IsSuccPrelimit o
Tactic: rw [isSuccLimit_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
⊢ o ≠ 0 ∧ IsSuccPrelimit o
have refine : ∀ (x : Ordinal.{u_1}) (hx : succ x = o), False
Tactic: refine ⟨h.1, isSuccPrelimit_of_succ_ne fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
h : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty
x : Ordinal.{u_1}
hx : succ x = o
⊢ False
have rcases : ∀ (p : Ordinal.{u_1}) (hp : p ∈ S ∩ Ioo x o), False
Tactic: rcases h.2 x (lt_of_lt_of_le (lt_succ x) hx.le) with ⟨p, hp⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S T : Set Ordinal.{u_1}
h : S ⊆ T
ho : o.IsAcc S
⊢ o.IsAcc T
have rw : ∀ (ho : o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty), o ≠ 0 ∧ ∀ p < o, (T ∩ Ioo p o).Nonempty
Tactic: rw [isAcc_iff] at *
Cleared hypotheses: ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
⊢ AccPt p (𝓟 S) ↔ AccPt (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) p hpo) (𝓟 (Iio o ↓∩ S))
have rw : AccPt p (𝓟 S) ↔
  AccPt (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) p hpo)
    (comap (Subtype.val (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o)) (𝓟 S))
Tactic: rw [← comap_principal, isOpen_Iio.isOpenEmbedding_subtypeVal.accPt_comap_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
rw :
  AccPt p (𝓟 S) ↔
    AccPt (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) p hpo)
      (comap (Subtype.val (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o)) (𝓟 S))
⊢ AccPt p (𝓟 S) ↔ AccPt (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) p hpo) (𝓟 (Iio o ↓∩ S))
have rw₁ : AccPt p (𝓟 S) ↔ AccPt (↑(Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) p hpo) : Ordinal.{u_1}) (𝓟 S)
Tactic: rw [← comap_principal, isOpen_Iio.isOpenEmbedding_subtypeVal.accPt_comap_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Topology (goal)
Goal:
o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
⊢ IsClosedBelow (⋂₀ S) o
have rw : ∀ p < o, p.IsAcc (⋂₀ S) → p ∈ ⋂₀ S
Tactic: rw [isClosedBelow_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
⊢ ∀ (b : Ordinal.{max (u + 1) v}),
    Membership.mem (γ := Set Ordinal.{max (u + 1) v})
        (Set.range (ι := Ordinal.{u})
          (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
                fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
            (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
        b ↔
      b < univ.{u, v}
have refine : ∀ (b : Ordinal.{max (u + 1) v}) (α : Type (max (u + 1) v)) (r : α → α → Prop) [inst : IsWellOrder α r],
  Membership.mem (γ := Set Ordinal.{max (u + 1) v})
      (Set.range (ι := Ordinal.{u})
        (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
              fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
          (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
      (type r) ↔
    type r < univ.{u, v}
Tactic: refine fun b => inductionOn b ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
⊢ Membership.mem (γ := Set Ordinal.{max (u + 1) v})
      (Set.range (ι := Ordinal.{u})
        (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
              fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
          (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
      (type s) ↔
    type s < univ.{u, v}
have rw : Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    (type s) ↔
  type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
Tactic: rw [univ, ← lift_umax]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
⊢ Membership.mem (γ := Set Ordinal.{max (u + 1) v})
      (Set.range (ι := Ordinal.{u})
        (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
              fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
          (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
      (type s) ↔
    type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
have mp : Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    (type s) →
  type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
mp :
  Membership.mem (γ := Set Ordinal.{max (u + 1) v})
      (Set.range (ι := Ordinal.{u})
        (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
              fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
          (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
      (type s) →
    type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
⊢ Membership.mem (γ := Set Ordinal.{max (u + 1) v})
      (Set.range (ι := Ordinal.{u})
        (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
              fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
          (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
      (type s) ↔
    type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
have mpr : type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) →
  Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    (type s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h :
  Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    (type s)
⊢ type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
have mp : ∀ (a : Ordinal.{u})
  (e :
    (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
          (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
        a =
      type s),
  type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
Tactic: obtain ⟨a, e⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
a : Ordinal.{u}
e :
  (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      a =
    type s
⊢ type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
have mp : (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
        fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
      (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
    a <
  lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
Tactic: rw [← e]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
a : Ordinal.{u}
e :
  (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      a =
    type s
⊢ (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      a <
    lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
have mp : ∀ (α : Type u) (r : α → α → Prop) [inst : IsWellOrder α r],
  (liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
          fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v})
      (type r) <
    lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
Tactic: refine inductionOn a ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Univ (goal)
Goal:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst : IsWellOrder β s
h : type s < lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
⊢ Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    (type s)
have mpr : ∀
  (h :
    lift.{max (u + 1) v, max (u + 1) v} (type s) <
      lift.{max (u + 1) v, u + 1} (type fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)),
  Membership.mem (γ := Set Ordinal.{max (u + 1) v})
    (Set.range (ι := Ordinal.{u})
      (⇑(liftInitialSeg.toRelEmbedding (r := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{max (max (u + 1) v) u}) ↦ x1 < x2)) :
        (a : Ordinal.{u}) → Ordinal.{max (u + 1) v}))
    (lift.{max (u + 1) v, max (u + 1) v} (type s))
Tactic: rw [← lift_id (type s)] at h ⊢
Cleared hypotheses: h