awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
b : Ordinal.{u_1}
hb_1 : b ∈ Iio (g o)
hb : ∃ a' < o, b < g a'
⊢ ∃ (y : (↑(Iio (g o)) : Type (u_1 + 1))),
    Membership.mem (γ := Set (↑(Iio (g o)) : Type (u_1 + 1)))
        (range fun (i : (↑(Iio a) : Type (u_1 + 1))) ↦
          Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) (g (↑(f i) : Ordinal.{u_1})) ⋯)
        y ∧
      Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) b hb_1 ≤ y
have obtain : ∀ (c : Ordinal.{u_1}) (hc : c < o) (hc' : b < g c),
  ∃ (y : (↑(Iio (g o)) : Type (u_1 + 1))),
    Membership.mem (γ := Set (↑(Iio (g o)) : Type (u_1 + 1)))
        (range fun (i : (↑(Iio a) : Type (u_1 + 1))) ↦
          Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) (g (↑(f i) : Ordinal.{u_1})) sorry)
        y ∧
      Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) b hb_1 ≤ y
Tactic: obtain ⟨c, hc, hc'⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
b : Ordinal.{u_1}
hb : b ∈ Iio (g o)
c : Ordinal.{u_1}
hc : c < o
hc' : b < g c
⊢ ∃ (y : (↑(Iio (g o)) : Type (u_1 + 1))),
    Membership.mem (γ := Set (↑(Iio (g o)) : Type (u_1 + 1)))
        (range fun (i : (↑(Iio a) : Type (u_1 + 1))) ↦
          Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) (g (↑(f i) : Ordinal.{u_1})) ⋯)
        y ∧
      Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) b hb ≤ y
have obtain : ∀ (d : (↑(Iio a) : Type (u_1 + 1))) (hd : Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) c hc ≤ f d),
  ∃ (y : (↑(Iio (g o)) : Type (u_1 + 1))),
    Membership.mem (γ := Set (↑(Iio (g o)) : Type (u_1 + 1)))
        (range fun (i : (↑(Iio a) : Type (u_1 + 1))) ↦
          Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) (g (↑(f i) : Ordinal.{u_1})) sorry)
        y ∧
      Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) b hb ≤ y
Tactic: obtain ⟨_, ⟨d, rfl⟩, hd⟩ := hf.isCofinal_range ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
b : Ordinal.{u_1}
hb : b ∈ Iio (g o)
c : Ordinal.{u_1}
hc : c < o
hc' : b < g c
d : (↑(Iio a) : Type (u_1 + 1))
hd : Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio o) c hc ≤ f d
⊢ ∃ (y : (↑(Iio (g o)) : Type (u_1 + 1))),
    Membership.mem (γ := Set (↑(Iio (g o)) : Type (u_1 + 1)))
        (range fun (i : (↑(Iio a) : Type (u_1 + 1))) ↦
          Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) (g (↑(f i) : Ordinal.{u_1})) ⋯)
        y ∧
      Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) b hb ≤ y
have refine : Membership.mem (γ := Set (↑(Iio (g o)) : Type (u_1 + 1)))
  (range fun (i : (↑(Iio a) : Type (u_1 + 1))) ↦
    Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) (g (↑(f i) : Ordinal.{u_1})) sorry)
  (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) (g (↑(f d) : Ordinal.{u_1})) sorry)
Tactic: refine ⟨⟨_, hg.strictMono (f d).2⟩, ?_, hc'.le.trans (hg.monotone hd)⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u_1}
ha : o.cof.ord = a
⊢ ∃ (f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))), IsFundamentalSeq f
have subst : ∃ (f : (↑(Iio o.cof.ord) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))), IsFundamentalSeq f
Tactic: subst ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
o : Ordinal.{u_1}
⊢ ∃ (f : (↑(Iio o.cof.ord) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))), IsFundamentalSeq f
have obtain : ∀ (s : Set o.ToType) (hs : IsCofinal s)
  (hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof o.ToType).ord),
  ∃ (f : (↑(Iio o.cof.ord) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))), IsFundamentalSeq f
Tactic: obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq o.ToType
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (hypothesis)
Goal:
o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = (Order.cof o.ToType).ord
⊢ ∃ (f : (↑(Iio o.cof.ord) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))), IsFundamentalSeq f
have hs'₁ : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = o.cof.ord
Tactic: rw [cof_toType] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = o.cof.ord
g : (↑(Iio o.cof.ord) : Type (u_1 + 1)) ≃o (↑s : Type u_1) :=
  OrderIso.trans (OrderIso.setCongr (Iio o.cof.ord) (Iio (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2)) ⋯)
    (OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2))
⊢ ∃ (f : (↑(Iio o.cof.ord) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))), IsFundamentalSeq f
have refine : IsCofinal.{u_1 + 1} (α := (↑(Iio o) : Type (u_1 + 1)))
  (range fun (i : (↑(Iio o.cof.ord) : Type (u_1 + 1))) ↦
    ToType.toOrd (↑((g : (a : (↑(Iio o.cof.ord) : Type (u_1 + 1))) → (↑s : Type u_1)) i) : o.ToType))
Tactic: refine ⟨fun i ↦ g i, le_rfl, fun _ ↦ by simp, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = o.cof.ord
g : (↑(Iio o.cof.ord) : Type (u_1 + 1)) ≃o (↑s : Type u_1) :=
  OrderIso.trans (OrderIso.setCongr (Iio o.cof.ord) (Iio (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2)) ⋯)
    (OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2))
⊢ IsCofinal.{u_1 + 1} (α := (↑(Iio o) : Type (u_1 + 1)))
    (range fun (i : (↑(Iio o.cof.ord) : Type (u_1 + 1))) ↦
      ToType.toOrd (↑((g : (a : (↑(Iio o.cof.ord) : Type (u_1 + 1))) → (↑s : Type u_1)) i) : o.ToType))
have rw : IsCofinal.{u_1} (α := o.ToType) (image (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : o.ToType) ↦ x ∈ s)) Set.univ)
Tactic: rw [range_comp', OrderIso.map_isCofinal_iff, range_comp', g.range_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ a.cof.ord ≤ o
have rw : (o.blsub f).cof.ord ≤ o
Tactic: rw [← hf.2.2]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a_1 : Ordinal.{?u.24777}
b : Ordinal.{?u.24780}
o_1 : Ordinal.{?u.24783}
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi : i < a.cof.ord
⊢ a.cof.ord ≤ o
have rw : o ≤ o
Tactic: rw [hf.cof_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (hypothesis)
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ a.IsFundamentalSequence a.cof.ord fun (i : Ordinal.{u}) (hi : i < a.cof.ord) ↦ f i ⋯
have H : a.cof.ord = o
Tactic: have H := hf.cof_eq
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
H : a.cof.ord = o
⊢ a.IsFundamentalSequence a.cof.ord fun (i : Ordinal.{u}) (hi : i < a.cof.ord) ↦ f i ⋯
have subst : ∀ {f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}} (hf : a.IsFundamentalSequence a.cof.ord f),
  a.IsFundamentalSequence a.cof.ord fun (i : Ordinal.{u}) (hi : i < a.cof.ord) ↦ f i sorry
Tactic: subst H
Cleared hypotheses: o, f, hf, H
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}
⊢ 0 ≤ (cof 0).ord
have rw : 0 ≤ ord 0
Tactic: rw [cof_zero, ord_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}
rw : 0 ≤ ord 0
⊢ 0 ≤ (cof 0).ord
have rw₁ : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 0
Tactic: rw [cof_zero, ord_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
o : Ordinal.{u}
⊢ IsFundamentalSequence.{u} (succ o) 1 fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o
have refine_1 : 1 ≤ (succ o).cof.ord
Tactic: refine ⟨?_, @fun i j hi hj h => ?_, blsub_const Ordinal.one_ne_zero o⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
o : Ordinal.{u}
refine_1 : 1 ≤ (succ o).cof.ord
⊢ IsFundamentalSequence.{u} (succ o) 1 fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o
have refine_2 : ∀ (i j : Ordinal.{u}) (hi : i < 1) (hj : j < 1) (h : i < j),
  LT.lt.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o) i hi)
    ((fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o) j hj)
Tactic: refine ⟨?_, @fun i j hi hj h => ?_, blsub_const Ordinal.one_ne_zero o⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
o : Ordinal.{u}
⊢ 1 ≤ (succ o).cof.ord
have refine_1 : 1 ≤ ord 1
Tactic: rw [cof_succ, ord_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
o : Ordinal.{u}
refine_1 : 1 ≤ ord 1
⊢ 1 ≤ (succ o).cof.ord
have refine_1₁ : LE.le.{u + 1} (α := Ordinal.{u}) 1 1
Tactic: rw [cof_succ, ord_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
o i j : Ordinal.{u}
hi : i < 1
hj : j < 1
h : i < j
⊢ LT.lt.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o) i hi)
    ((fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o) j hj)
have refine_2 : ∀ (hi_1 : i = 0) (hj : j < 1) (hj_1 : j = 0) (h : i < j),
  LT.lt.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o) i hi)
    ((fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o) j hj)
Tactic: rw [lt_one_iff_zero] at hi hj
Cleared hypotheses: hj, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (hypothesis)
Goal:
o i j : Ordinal.{u}
hi_1 : i < 1
hi : i = 0
hj_1 : j < 1
hj : j = 0
h : i < j
⊢ LT.lt.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o) i hi_1)
    ((fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o) j hj_1)
have h₁ : LT.lt.{u + 1} (α := Ordinal.{u}) 0 0
Tactic: rw [hi, hj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i j : Ordinal.{u}
hi : i < o
hj : j < o
hij : i ≤ j
⊢ f i hi ≤ f j hj
have inl : ∀ (hij : i < j), f i hi ≤ f j hj
Tactic: rcases lt_or_eq_of_le hij with (hij | rfl)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i j : Ordinal.{u}
hi : i < o
hj : j < o
hij : i ≤ j
inl : ∀ (hij : i < j), f i hi ≤ f j hj
⊢ f i hi ≤ f j hj
have inr : ∀ (hj : i < o) (hij : i ≤ i), f i hi ≤ f i hi
Tactic: rcases lt_or_eq_of_le hij with (hij | rfl)
Cleared hypotheses: j, hj, hij
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a_1 : Ordinal.{?u.26140}
b : Ordinal.{?u.26143}
o_1 : Ordinal.{?u.26146}
a_2 o_2 : Ordinal.{u}
f_1 : (b : Ordinal.{u}) → b < o_2 → Ordinal.{u}
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
i : Ordinal.{u}
hi : i < o'
⊢ g i hi < o
have rw : g i hi < o'.blsub g
Tactic: rw [← hg.2.2]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ a.IsFundamentalSequence o' fun (i : Ordinal.{u}) (hi : i < o') ↦ f (g i hi) ⋯
have refine_1 : o' ≤ a.cof.ord
Tactic: refine ⟨?_, @fun i j _ _ h => hf.2.1 _ _ (hg.2.1 _ _ h), ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
refine_1 : o' ≤ a.cof.ord
⊢ a.IsFundamentalSequence o' fun (i : Ordinal.{u}) (hi : i < o') ↦ f (g i hi) ⋯
have refine_2 : (o'.blsub fun (i : Ordinal.{u}) (hi : i < o') ↦ f (g i hi) sorry) = a
Tactic: refine ⟨?_, @fun i j _ _ h => hf.2.1 _ _ (hg.2.1 _ _ h), ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o' ≤ a.cof.ord
have refine_1 : o' ≤ o
Tactic: rw [hf.cof_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ (o'.blsub fun (i : Ordinal.{u}) (hi : i < o') ↦ f (g i hi) ⋯) = a
have refine_2 : o.blsub f = a
Tactic: rw [@blsub_comp.{u, u, u} o _ f (@IsFundamentalSequence.monotone _ _ f hf)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
refine_2 : o.blsub f = a
⊢ (o'.blsub fun (i : Ordinal.{u}) (hi : i < o') ↦ f (g i hi) ⋯) = a
have refine_2₁ : o'.blsub g = o
Tactic: rw [@blsub_comp.{u, u, u} o _ f (@IsFundamentalSequence.monotone _ _ f hf)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
h : ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f
⊢ ∃ (f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}), a.IsFundamentalSequence a.cof.ord f
have rcases : ∀ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}) (hf : a.IsFundamentalSequence o f),
  ∃ (f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}), a.IsFundamentalSequence a.cof.ord f
Tactic: rcases h with ⟨o, f, hf⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
⊢ ∃ (f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}), a.IsFundamentalSequence a.cof.ord f
have suffices : ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f
Tactic: suffices h : ∃ o f, IsFundamentalSequence a o f by
    rcases h with ⟨o, f, hf⟩
    exact ⟨_, hf.ord_cof⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
⊢ ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f
have rcases : ∀ (ι : Type u) (f : ι → Ordinal.{u}) (hf : lsub f = a) (hι : #ι = a.cof),
  ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f
Tactic: rcases exists_lsub_cof a with ⟨ι, f, hf, hι⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
⊢ ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f
have rcases : ∀ (r : ι → ι → Prop) (wo : IsWellOrder ι r) (hr : (#ι).ord = type r),
  ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f
Tactic: rcases ord_eq ι with ⟨r, wo, hr⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (hypothesis)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
⊢ ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f
have this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
Tactic: haveI := hrr'.isWellOrder
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
⊢ ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f
have refine_1 : type r ≤ a.cof.ord
Tactic: refine
    ⟨_, _, hrr'.ordinal_type_le.trans ?_, @fun i j _ h _ => (enum r' ⟨j, h⟩).prop _ ?_,
      le_antisymm (blsub_le fun i hi => lsub_le_iff.1 hf.le _) ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
refine_1 : type r ≤ a.cof.ord
⊢ ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f
have refine_2 : ∀ (i j : Ordinal.{u}) (x : i < type r') (h : j < type r'),
  i < j →
    r
      (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i x)) :
        ι)
      (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) j h)) :
        ι)
Tactic: refine
    ⟨_, _, hrr'.ordinal_type_le.trans ?_, @fun i j _ h _ => (enum r' ⟨j, h⟩).prop _ ?_,
      le_antisymm (blsub_le fun i hi => lsub_le_iff.1 hf.le _) ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
refine_1 : type r ≤ a.cof.ord
refine_2 :
  ∀ (i j : Ordinal.{u}) (x : i < type r') (h : j < type r'),
    i < j →
      r
        (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i x)) :
          ι)
        (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
              (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) j h)) :
          ι)
⊢ ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f
have refine_3 : a ≤
  (type r').blsub fun (i : Ordinal.{u}) (x : i < type r') ↦
    f
      (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i x)) :
        ι)
Tactic: refine
    ⟨_, _, hrr'.ordinal_type_le.trans ?_, @fun i j _ h _ => (enum r' ⟨j, h⟩).prop _ ?_,
      le_antisymm (blsub_le fun i hi => lsub_le_iff.1 hf.le _) ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
⊢ type r ≤ a.cof.ord
have refine_1 : type r ≤ (#ι).ord
Tactic: rw [← hι, hr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
refine_1 : type r ≤ (#ι).ord
⊢ type r ≤ a.cof.ord
have refine_1₁ : type r ≤ type r
Tactic: rw [← hι, hr]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FundamentalSequence (goal)
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i j : Ordinal.{u}
h_1 : i < type r'
h : j < type r'
h_2 : i < j
⊢ r
    (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i h_1)) :
      ι)
    (↑((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
          (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) j h)) :
      ι)
have refine_2 : r
  ((hrr'.toEmbedding (r := r') (s := r) : (a : { i : ι // ∀ (j : ι), r j i → f j < f i }) → ι)
    ((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) i h_1) :
      { i : ι // ∀ (j : ι), r j i → f j < f i }))
  ((hrr'.toEmbedding (r := r') (s := r) : (a : { i : ι // ∀ (j : ι), r j i → f j < f i }) → ι)
    ((enum r' : (a : (↑(Iio (type r')) : Type (u + 1))) → { i : ι // ∀ (j : ι), r j i → f j < f i })
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r')) j h) :
      { i : ι // ∀ (j : ι), r j i → f j < f i }))
Tactic: change r (hrr'.1 _) (hrr'.1 _)