awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
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})) ⋯)
          y ∧
        Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) b hb ≤ y
⊢ ∃ (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

Tactic:
obtain ⟨_, ⟨d, rfl⟩, hd⟩ := hf.isCofinal_range ⟨c, hc⟩

Premises used: Subtype.mk, Ordinal.IsFundamentalSeq.isCofinal_range, rfl
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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

Tactic:
⟨⟨_, hg.strictMono (f d).2⟩, ?_, hc'.le.trans (hg.monotone hd)⟩

Premises used: Order.IsNormal.monotone, LT.lt.le, Subtype.mk, And.intro, Exists.intro, LE.le.trans, Order.IsNormal.strictMono, Subtype.property
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
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})) ⋯)
    (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) (g (↑(f d) : Ordinal.{u_1})) ⋯)
⊢ ∃ (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

Tactic:
refine ⟨⟨_, hg.strictMono (f d).2⟩, ?_, hc'.le.trans (hg.monotone hd)⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
⊢ 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})) ⋯)
    (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) (g (↑(f d) : Ordinal.{u_1})) ⋯)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
ha : o.cof.ord = a
subst : ∃ (f : (↑(Iio o.cof.ord) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))), IsFundamentalSeq f
⊢ ∃ (f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))), IsFundamentalSeq f

Tactic:
subst ha
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o : Ordinal.{u_1}
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
⊢ ∃ (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

Premises used: Ordinal.exists_ord_cof_eq, Ordinal.ToType
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
⊢ (type fun (x1 x2 : (↑s : Type u_1)) ↦ x1 < x2) = o.cof.ord

Tactic:
rw [cof_toType] at hs'

Premises used: Ordinal.cof_toType
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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))
x : (↑(Iio o.cof.ord) : Type (u_1 + 1))
⊢ ∀ ⦃b : (↑(Iio o.cof.ord) : Type (u_1 + 1))⦄,
    x < b →
      LT.lt.{u_1 + 1} (α := (↑(Iio o) : Type (u_1 + 1)))
        (ToType.toOrd (↑((g : (a : (↑(Iio o.cof.ord) : Type (u_1 + 1))) → (↑s : Type u_1)) x) : o.ToType))
        (ToType.toOrd (↑((g : (a : (↑(Iio o.cof.ord) : Type (u_1 + 1))) → (↑s : Type u_1)) b) : o.ToType))

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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))
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))
⊢ ∃ (f : (↑(Iio o.cof.ord) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))), IsFundamentalSeq f

Tactic:
refine ⟨fun i ↦ g i, le_rfl, fun _ ↦ by simp, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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))
rw :
  IsCofinal.{u_1} (α := o.ToType)
    (image (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : o.ToType) ↦ x ∈ s)) Set.univ)
⊢ 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:
rw [range_comp', OrderIso.map_isCofinal_iff, range_comp', g.range_eq]

Premises used: OrderIso.range_eq, OrderIso.map_isCofinal_iff, Set.range_comp'
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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} (α := o.ToType)
    (image (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : o.ToType) ↦ x ∈ s)) Set.univ)

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
rw : (o.blsub f).cof.ord ≤ o
⊢ a.cof.ord ≤ o

Tactic:
rw [← hf.2.2]

Premises used: And.right
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ (o.blsub f).cof.ord ≤ o

Tactic:
(ord_le_ord.2 (cof_blsub_le f)).trans (ord_card_le o)

Premises used: Iff.mpr, Ordinal.cof_blsub_le, Cardinal.ord_le_ord, LE.le.trans, Cardinal.ord_card_le
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ (o.blsub f).cof.ord ≤ o

Tactic:
exact (ord_le_ord.2 (cof_blsub_le f)).trans (ord_card_le o)

Premises used: Iff.mpr, Ordinal.cof_blsub_le, Cardinal.ord_le_ord, LE.le.trans, Cardinal.ord_card_le
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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), i < j → f i hi < f j hj

Tactic:
hf.2.1

Premises used: And.right, And.left
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ o.blsub f = a

Tactic:
hf.2.2

Premises used: And.right
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
rw rw₁ : o ≤ o
⊢ a.cof.ord ≤ o

Tactic:
rw [hf.cof_eq]

Premises used: Ordinal.IsFundamentalSequence.cof_eq
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ a.cof.ord = o

Tactic:
have H := hf.cof_eq
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
H : a.cof.ord = o
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 ⋯
⊢ a.IsFundamentalSequence a.cof.ord fun (i : Ordinal.{u}) (hi : i < a.cof.ord) ↦ f i ⋯

Tactic:
subst H
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a : Ordinal.{u}
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 ⋯

Tactic:
hf
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a : Ordinal.{u}
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 ⋯

Tactic:
exact hf
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o : Ordinal.{u}
h : o ≤ o.cof.ord
⊢ o.IsFundamentalSequence o fun (a : Ordinal.{u}) (x : a < o) ↦ a

Tactic:
⟨h, @fun _ _ _ _ => id, blsub_id o⟩

Premises used: Ordinal.blsub_id, Ordinal.IsFundamentalSequence, id, And.intro
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}
rw : 0 ≤ ord 0
rw₁ rw₂ : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 0
⊢ 0 ≤ (cof 0).ord

Tactic:
rw [cof_zero, ord_zero]

Premises used: Ordinal.cof_zero, Cardinal.ord_zero
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o : Ordinal.{u}
⊢ IsFundamentalSequence.{u} (succ o) 1 fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o

Tactic:
⟨?_, @fun i j hi hj h => ?_, blsub_const Ordinal.one_ne_zero o⟩

Premises used: Ordinal.IsFundamentalSequence, And.intro, Ordinal.blsub_const, Ordinal.one_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o : Ordinal.{u}
refine_1 : 1 ≤ (succ o).cof.ord
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)
⊢ IsFundamentalSequence.{u} (succ o) 1 fun (x : Ordinal.{u}) (x_1 : x < 1) ↦ o

Tactic:
refine ⟨?_, @fun i j hi hj h => ?_, blsub_const Ordinal.one_ne_zero o⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o : Ordinal.{u}
refine_1 : 1 ≤ ord 1
refine_1₁ refine_1₂ : LE.le.{u + 1} (α := Ordinal.{u}) 1 1
⊢ 1 ≤ (succ o).cof.ord

Tactic:
rw [cof_succ, ord_one]

Premises used: Ordinal.cof_succ, Cardinal.ord_one
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o i j : Ordinal.{u}
hi : i < 1
hj : j < 1
h : i < j
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)
⊢ 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

Premises used: Ordinal.lt_one_iff_zero
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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}) 0 0

Tactic:
rw [hi, hj] at h
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o i j : Ordinal.{u}
hi_1 : i < 1
hi : i = 0
hj_1 : j < 1
hj : j = 0
h : LT.lt.{u + 1} (α := Ordinal.{u}) 0 0
⊢ 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)

Tactic:
h.false.elim

Premises used: False.elim, LT.lt.false
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o i j : Ordinal.{u}
hi_1 : i < 1
hi : i = 0
hj_1 : j < 1
hj : j = 0
h : LT.lt.{u + 1} (α := Ordinal.{u}) 0 0
⊢ 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)

Tactic:
exact h.false.elim

Premises used: False.elim, LT.lt.false
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
inr : ∀ (hj : i < o) (hij : i ≤ i), f i hi ≤ f i hi
⊢ f i hi ≤ f j hj

Tactic:
rcases lt_or_eq_of_le hij with (hij | rfl)

Premises used: lt_or_eq_of_le, rfl
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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_1 : i ≤ j
hij : i < j
⊢ f i hi ≤ f j hj

Tactic:
(hf.2.1 hi hj hij).le

Premises used: LT.lt.le, And.right, And.left
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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_1 : i ≤ j
hij : i < j
⊢ f i hi ≤ f j hj

Tactic:
exact (hf.2.1 hi hj hij).le

Premises used: LT.lt.le, And.right, And.left
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi hj : i < o
hij : i ≤ i
⊢ f i hi ≤ f i hi

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'
rw : g i hi < o'.blsub g
⊢ g i hi < o

Tactic:
rw [← hg.2.2]

Premises used: And.right
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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'.blsub g

Tactic:
apply lt_blsub

Premises used: Ordinal.lt_blsub
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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) ⋯

Tactic:
⟨?_, @fun i j _ _ h => hf.2.1 _ _ (hg.2.1 _ _ h), ?_⟩

Premises used: Ordinal.IsFundamentalSequence.trans._proof_1, Ordinal.IsFundamentalSequence, And.right, And.left, And.intro
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
refine_2 : (o'.blsub fun (i : Ordinal.{u}) (hi : i < o') ↦ f (g i hi) ⋯) = a
⊢ a.IsFundamentalSequence o' fun (i : Ordinal.{u}) (hi : i < o') ↦ f (g i hi) ⋯

Tactic:
refine ⟨?_, @fun i j _ _ h => hf.2.1 _ _ (hg.2.1 _ _ h), ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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' ≤ o
⊢ o' ≤ a.cof.ord

Tactic:
rw [hf.cof_eq]

Premises used: Ordinal.IsFundamentalSequence.cof_eq
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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' ≤ o

Tactic:
hg.1.trans (ord_cof_le o)

Premises used: Ordinal.ord_cof_le, And.left, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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' ≤ o

Tactic:
exact hg.1.trans (ord_cof_le o)

Premises used: Ordinal.ord_cof_le, And.left, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
refine_2₁ : o'.blsub g = o
⊢ (o'.blsub fun (i : Ordinal.{u}) (hi : i < o') ↦ f (g i hi) ⋯) = a

Tactic:
rw [@blsub_comp.{u, u, u} o _ f (@IsFundamentalSequence.monotone _ _ f hf)]
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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 f = a

Tactic:
hf.2.2

Premises used: And.right
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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 f = a

Tactic:
exact hf.2.2

Premises used: And.right
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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 g = o

Tactic:
hg.2.2

Premises used: And.right
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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 g = o

Tactic:
exact hg.2.2

Premises used: And.right
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
s : (p : Ordinal.{u_1}) → p < o → Ordinal.{u_1}
h : a.IsFundamentalSequence o s
p : Ordinal.{u_1}
hp : p < o
⊢ s p hp < a

Tactic:
h.blsub_eq ▸ lt_blsub s p hp

Premises used: Ordinal.IsFundamentalSequence.blsub_eq, Eq.rec, Ordinal.lt_blsub
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a : Ordinal.{u}
h : ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f
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
⊢ ∃ (f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}), a.IsFundamentalSequence a.cof.ord f

Tactic:
rcases h with ⟨o, f, hf⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a 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:
⟨_, hf.ord_cof⟩

Premises used: Ordinal.IsFundamentalSequence.ord_cof, Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a 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:
exact ⟨_, hf.ord_cof⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a : Ordinal.{u}
suffices : ∃ (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

Tactic:
suffices h : ∃ o f, IsFundamentalSequence a o f by
    rcases h with ⟨o, f, hf⟩
    exact ⟨_, hf.ord_cof⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a : Ordinal.{u}
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
⊢ ∃ (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ι⟩

Premises used: Ordinal.exists_lsub_cof
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
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
⊢ ∃ (o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}), a.IsFundamentalSequence o f

Tactic:
rcases ord_eq ι with ⟨r, wo, hr⟩

Premises used: Cardinal.ord_eq
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
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
⊢ IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'

Tactic:
haveI := hrr'.isWellOrder