awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h_lfp : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), (lfp : (a : α →o α) → α) f = (↑y : α)
y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
h_y : (lfp : (a : α →o α) → α) f = (↑y : α)
⊢ lfpApprox f ⊥ (succ #α).ord ≤ (↑y : α)

Tactic:
lfpApprox_le_of_mem_fixedPoints f y.2 bot_le (ord <| succ #α)

Premises used: Order.succ, Cardinal.mk, OrdinalApprox.lfpApprox_le_of_mem_fixedPoints, Cardinal.ord, bot_le, Subtype.property
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h_lfp : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), (lfp : (a : α →o α) → α) f = (↑y : α)
y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
h_y : (lfp : (a : α →o α) → α) f = (↑y : α)
⊢ lfpApprox f ⊥ (succ #α).ord ≤ (↑y : α)

Tactic:
exact lfpApprox_le_of_mem_fixedPoints f y.2 bot_le (ord <| succ #α)

Premises used: Order.succ, Cardinal.mk, OrdinalApprox.lfpApprox_le_of_mem_fixedPoints, Cardinal.ord, bot_le, Subtype.property
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), lfpApprox f ⊥ (succ #α).ord = (↑y : α)

Tactic:
simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
        lfpApprox_ord_mem_fixedPoint f bot_le

Premises used: exists_eq_right', Subtype.exists, OrdinalApprox.lfpApprox_ord_mem_fixedPoint, exists_prop, Function.mem_fixedPoints, bot_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), lfpApprox f ⊥ (succ #α).ord = (↑y : α)

Tactic:
have h_fix : ∃ y : fixedPoints f, lfpApprox f ⊥ (ord <| succ #α) = y := by
      simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
        lfpApprox_ord_mem_fixedPoint f bot_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h_fix : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), lfpApprox f ⊥ (succ #α).ord = (↑y : α)
a :
  ∀ (x : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)) (h_x : lfpApprox f ⊥ (succ #α).ord = (↑x : α)),
    (lfp : (a : α →o α) → α) f ≤ lfpApprox f ⊥ (succ #α).ord
⊢ (lfp : (a : α →o α) → α) f ≤ lfpApprox f ⊥ (succ #α).ord

Tactic:
let ⟨x, h_x⟩ := h_fix
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h_fix : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), lfpApprox f ⊥ (succ #α).ord = (↑y : α)
x : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
h_x : lfpApprox f ⊥ (succ #α).ord = (↑x : α)
a : (lfp : (a : α →o α) → α) f ≤ (↑x : α)
⊢ (lfp : (a : α →o α) → α) f ≤ lfpApprox f ⊥ (succ #α).ord

Tactic:
rw [h_x]
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h_fix : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), lfpApprox f ⊥ (succ #α).ord = (↑y : α)
x : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
h_x : lfpApprox f ⊥ (succ #α).ord = (↑x : α)
⊢ (lfp : (a : α →o α) → α) f ≤ (↑x : α)

Tactic:
lfp_le_fixed f x.prop

Premises used: Subtype.prop, OrderHom.lfp_le_fixed
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h_fix : ∃ (y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)), lfpApprox f ⊥ (succ #α).ord = (↑y : α)
x : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
h_x : lfpApprox f ⊥ (succ #α).ord = (↑x : α)
⊢ (lfp : (a : α →o α) → α) f ≤ (↑x : α)

Tactic:
exact lfp_le_fixed f x.prop

Premises used: Subtype.prop, OrderHom.lfp_le_fixed
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : lfpApprox f ⊥ (succ #α).ord = (lfp : (a : α →o α) → α) f
⊢ Membership.mem (α := α) (Set.range (lfpApprox f ⊥)) ((lfp : (a : α →o α) → α) f : α)

Tactic:
use ord <| succ #α

Premises used: Order.succ, Cardinal.mk, Cardinal.ord
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord = (lfp : (a : α →o α) → α) f

Tactic:
lfpApprox_ord_eq_lfp f

Premises used: OrdinalApprox.lfpApprox_ord_eq_lfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord = (lfp : (a : α →o α) → α) f

Tactic:
exact lfpApprox_ord_eq_lfp f

Premises used: OrdinalApprox.lfpApprox_ord_eq_lfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
⊢ gfpApprox f x 0 = x

Tactic:
lfpApprox_zero f.dual

Premises used: iInf, OrdinalApprox.lfpApprox_zero, OrderDual, OrderHom.dual, DFunLike.coe, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
⊢ gfpApprox f x 0 = x

Tactic:
exact lfpApprox_zero f.dual

Premises used: OrdinalApprox.lfpApprox_zero, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
⊢ Antitone (gfpApprox f x)

Tactic:
lfpApprox_mono_right f.dual

Premises used: iInf, Antitone, OrdinalApprox.lfpApprox_mono_right, OrderDual, OrderHom.dual, DFunLike.coe, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
⊢ gfpApprox f x a ≤ x

Tactic:
le_lfpApprox f.dual

Premises used: iInf, OrderDual, OrdinalApprox.le_lfpApprox, OrderHom.dual, DFunLike.coe, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : (f : (a : α) → α) x ≤ x
a : Ordinal.{u}
⊢ gfpApprox f x (a + 1) = (f : (a : α) → α) (gfpApprox f x a)

Tactic:
lfpApprox_add_one f.dual hx a

Premises used: iInf, OrdinalApprox.lfpApprox_add_one, OrdinalApprox.lfpApprox, OrderDual, WellFounded.fixF, OrderHom.dual, DFunLike.coe, WellFounded.fix, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a < b
⊢ gfpApprox f x b ≤ (f : (a : α) → α) (gfpApprox f x a)

Tactic:
apply_lfpApprox_le_lfpApprox_of_lt f.dual h

Premises used: iInf, OrdinalApprox.lfpApprox, OrdinalApprox.apply_lfpApprox_le_lfpApprox_of_lt, OrderDual, WellFounded.fixF, OrderHom.dual, DFunLike.coe, WellFounded.fix, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ gfpApprox f x a = ⨅ (b : (↑(Set.Iio a) : Type (u + 1))), gfpApprox f x (↑b : Ordinal.{u})

Tactic:
lfpApprox_of_isSuccLimit f.dual ha

Premises used: iInf, OrderDual, OrdinalApprox.lfpApprox_of_isSuccLimit, OrderHom.dual, DFunLike.coe, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f g : α →o α
h : f ≤ g
⊢ LE.le (α := αᵒᵈ →o αᵒᵈ) ((OrderHom.dual : (a : α →o α) → αᵒᵈ →o αᵒᵈ) g : αᵒᵈ →o αᵒᵈ)
    ((OrderHom.dual : (a : α →o α) → αᵒᵈ →o αᵒᵈ) f : αᵒᵈ →o αᵒᵈ)

Tactic:
have : g.dual ≤ f.dual := h
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f g : α →o α
h : f ≤ g
this :
  LE.le (α := αᵒᵈ →o αᵒᵈ) ((OrderHom.dual : (a : α →o α) → αᵒᵈ →o αᵒᵈ) g : αᵒᵈ →o αᵒᵈ)
    ((OrderHom.dual : (a : α →o α) → αᵒᵈ →o αᵒᵈ) f : αᵒᵈ →o αᵒᵈ)
⊢ gfpApprox f ≤ gfpApprox g

Tactic:
lfpApprox_mono_left this

Premises used: iInf, OrdinalApprox.lfpApprox_mono_left, OrderDual, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f g : α →o α
h : f ≤ g
this :
  LE.le (α := αᵒᵈ →o αᵒᵈ) ((OrderHom.dual : (a : α →o α) → αᵒᵈ →o αᵒᵈ) g : αᵒᵈ →o αᵒᵈ)
    ((OrderHom.dual : (a : α →o α) → αᵒᵈ →o αᵒᵈ) f : αᵒᵈ →o αᵒᵈ)
⊢ gfpApprox f ≤ gfpApprox g

Tactic:
exact lfpApprox_mono_left this

Premises used: OrdinalApprox.lfpApprox_mono_left
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ Monotone (gfpApprox f)

Tactic:
fun _ _ h => lfpApprox_mono_mid f.dual h

Premises used: OrdinalApprox.lfpApprox_mono_mid, iInf, Monotone, OrderDual, OrderHom.dual, DFunLike.coe, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h_ab : a ≤ b
h : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (gfpApprox f x a)
⊢ gfpApprox f x b = gfpApprox f x a

Tactic:
lfpApprox_eq_of_mem_fixedPoints f.dual h_ab h

Premises used: iInf, OrdinalApprox.lfpApprox_eq_of_mem_fixedPoints, OrderDual, OrderHom.dual, DFunLike.coe, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ gfpApprox f x a = gfpApprox f x b

Tactic:
exists_lfpApprox_eq_lfpApprox f.dual x

Premises used: iInf, OrdinalApprox.exists_lfpApprox_eq_lfpApprox, OrderDual, OrderHom.dual, DFunLike.coe, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : (f : (a : α) → α) x ≤ x
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (gfpApprox f x (succ #α).ord)

Tactic:
lfpApprox_ord_mem_fixedPoint f.dual hx

Premises used: iInf, Set.Mem, OrdinalApprox.lfpApprox_ord_mem_fixedPoint, OrderDual, OrderHom.dual, DFunLike.coe, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x a : α
ha : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
hax : a ≤ x
i : Ordinal.{u}
⊢ a ≤ gfpApprox f x i

Tactic:
lfpApprox_le_of_mem_fixedPoints f.dual ha hax i

Premises used: iInf, OrdinalApprox.lfpApprox_le_of_mem_fixedPoints, OrderDual, OrderHom.dual, DFunLike.coe, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ gfpApprox f ⊤ (succ #α).ord = (gfp : (a : α →o α) → α) f

Tactic:
lfpApprox_ord_eq_lfp f.dual

Premises used: iInf, setOf, OrdinalApprox.lfpApprox_ord_eq_lfp, OrderDual, OrderHom.dual, DFunLike.coe, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
⊢ Membership.mem (α := α) (Set.range (gfpApprox f ⊤)) ((gfp : (a : α →o α) → α) f : α)

Tactic:
lfp_mem_range_lfpApprox f.dual

Premises used: iInf, Set.Mem, setOf, OrdinalApprox.lfp_mem_range_lfpApprox, OrderDual, OrderHom.dual, DFunLike.coe, OrdinalApprox.gfpApprox
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
a₁ : ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 ≤ o
a₂ : o ≤ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
⊢ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 = o

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
a₁ : ∀ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) < o
⊢ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 ≤ o

Tactic:
simp_rw [Ordinal.iSup_le_iff, add_one_le_iff]

Premises used: Order.add_one_le_iff, Ordinal.iSup_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
⊢ ∀ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) < o

Tactic:
fun i ↦ (f i).2

Premises used: Set.Mem, setOf, Set.Iio, 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))
hf : IsFundamentalSeq f
⊢ ∀ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) < o

Tactic:
exact fun i ↦ (f i).2

Premises used: 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))
hf : IsFundamentalSeq f
⊢ o ≤ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1

Tactic:
le_of_forall_lt fun b hb ↦ ?_

Premises used: le_of_forall_lt
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
a₁ : ∀ (b : Ordinal.{u_1}) (hb : b < o), b < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
⊢ o ≤ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1

Tactic:
refine le_of_forall_lt fun b hb ↦ ?_

Premises used: le_of_forall_lt
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
b : Ordinal.{u_1}
hb : b < o
a₁ :
  ∀ (c : (↑(Iio a) : Type (u_1 + 1))) (hc : b ≤ (↑(f c) : Ordinal.{u_1})),
    b < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
⊢ b < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1

Tactic:
obtain ⟨_, ⟨c, rfl⟩, hc : b ≤ _⟩ := hf.isCofinal_range ⟨b, hb⟩

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))
hf : IsFundamentalSeq f
b : Ordinal.{u_1}
hb : b < o
c : (↑(Iio a) : Type (u_1 + 1))
hc : b ≤ (↑(f c) : Ordinal.{u_1})
a₁ : (↑(f c) : Ordinal.{u_1}) < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
⊢ b < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1

Tactic:
apply hc.trans_lt

Premises used: LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
b : Ordinal.{u_1}
hb : b < o
c : (↑(Iio a) : Type (u_1 + 1))
hc : b ≤ (↑(f c) : Ordinal.{u_1})
a₁ : (↑(f c) : Ordinal.{u_1}) + 1 ≤ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1
⊢ (↑(f c) : Ordinal.{u_1}) < ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1

Tactic:
rw [← add_one_le_iff]

Premises used: Order.add_one_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
b : Ordinal.{u_1}
hb : b < o
c : (↑(Iio a) : Type (u_1 + 1))
hc : b ≤ (↑(f c) : Ordinal.{u_1})
⊢ (↑(f c) : Ordinal.{u_1}) + 1 ≤ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1

Tactic:
apply Ordinal.le_iSup

Premises used: Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
apply : o.cof.ord ≤ a
⊢ o.cof.ord = a

Tactic:
apply hf.le_ord_cof.antisymm'

Premises used: LE.le.antisymm', Ordinal.IsFundamentalSeq.le_ord_cof
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
rw : a.cof.ord ≤ a
⊢ o.cof.ord ≤ a

Tactic:
rw [← hf.iSup_add_one_eq, cof_iSup_Iio_add_one hf.strictMono]

Premises used: Ordinal.IsFundamentalSeq.strictMono, Ordinal.cof_iSup_Iio_add_one, Ordinal.IsFundamentalSeq.iSup_add_one_eq
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
⊢ a.cof.ord ≤ a

Tactic:
ord_cof_le a

Premises used: Ordinal.ord_cof_le
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
⊢ a.cof.ord ≤ a

Tactic:
exact ord_cof_le a

Premises used: Ordinal.ord_cof_le
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
ha : 1 < a
rw : IsSuccPrelimit a
⊢ ⨆ (i : (↑(Iio a) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) = o

Tactic:
rw [← iSup_Iio_add_one hf.strictMono, hf.iSup_add_one_eq]

Premises used: Ordinal.IsFundamentalSeq.strictMono, Ordinal.iSup_Iio_add_one, Ordinal.IsFundamentalSeq.iSup_add_one_eq
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
ha : 1 < a
rw : IsSuccPrelimit o.cof.ord
⊢ IsSuccPrelimit a

Tactic:
rw [← hf.ord_cof]

Premises used: Ordinal.IsFundamentalSeq.ord_cof
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
ha : 1 < a
apply : ℵ₀ ≤ o.cof
⊢ IsSuccPrelimit o.cof.ord

Tactic:
apply (isSuccLimit_ord _).isSuccPrelimit

Premises used: Cardinal.isSuccLimit_ord, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
hf : IsFundamentalSeq f
ha : 1 < a
rwa : 1 < o.cof
rwa₁ : ord 1 < o.cof.ord
rwa₂ : ord 1 < a
rwa₃ rwa₄ rwa₅ rwa₆ : 1 < a
⊢ ℵ₀ ≤ o.cof

Tactic:
rwa [aleph0_le_cof_iff, ← ord_lt_ord, hf.ord_cof, ord_one]

Premises used: Ordinal.aleph0_le_cof_iff, Ordinal.IsFundamentalSeq.ord_cof, Cardinal.ord_one, Cardinal.ord_lt_ord
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o : Ordinal.{u_1}
ho : o ≤ o.cof.ord
⊢ IsCofinal.{u_1 + 1} (α := (↑(Iio o) : Type (u_1 + 1))) (range id)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
f : (↑(Iio 0) : Type (u_1 + 1)) → (↑(Iio 0) : Type (u_1 + 1))
⊢ 0 ≤ (cof 0).ord

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
f : (↑(Iio 0) : Type (u_1 + 1)) → (↑(Iio 0) : Type (u_1 + 1))
x : (↑(Iio 0) : Type (u_1 + 1))
⊢ ∀ ⦃b : (↑(Iio 0) : Type (u_1 + 1))⦄, x < b → f x < f b

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o : Ordinal.{u_1}
⊢ 1 ≤ (o + 1).cof.ord

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o : Ordinal.{u_1}
x : (↑(Iio 1) : Type (u_1 + 1))
⊢ ∀ ⦃b : (↑(Iio 1) : Type (u_1 + 1))⦄,
    x < b →
      LT.lt.{u_1 + 1} (α := (↑(Iio (o + 1)) : Type (u_1 + 1)))
        ((fun (x : (↑(Iio 1) : Type (u_1 + 1))) ↦
            (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (o + 1)) o ⋯ :
              { x : Ordinal.{u_1} // x ∈ Iio (o + 1) }))
          x)
        ((fun (x : (↑(Iio 1) : Type (u_1 + 1))) ↦
            (Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (o + 1)) o ⋯ :
              { x : Ordinal.{u_1} // x ∈ Iio (o + 1) }))
          b)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
o : Ordinal.{u_1}
⊢ IsCofinal.{u_1 + 1} (α := (↑(Iio (o + 1)) : Type (u_1 + 1)))
    (range fun (x : (↑(Iio 1) : Type (u_1 + 1))) ↦ Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (o + 1)) o ⋯)

Tactic:
simp [IsTop]

Premises used: IsTop
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a b o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : (↑(Iio b) : Type (u_1 + 1)) → (↑(Iio a) : Type (u_1 + 1))
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
rw : a.cof.ord ≤ a
⊢ b ≤ o.cof.ord

Tactic:
rw [hf.ord_cof, ← hg.ord_cof]

Premises used: Ordinal.IsFundamentalSeq.ord_cof
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a b o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : (↑(Iio b) : Type (u_1 + 1)) → (↑(Iio a) : Type (u_1 + 1))
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ a.cof.ord ≤ a

Tactic:
a.ord_cof_le

Premises used: Ordinal.ord_cof_le
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a b o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : (↑(Iio b) : Type (u_1 + 1)) → (↑(Iio a) : Type (u_1 + 1))
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ a.cof.ord ≤ a

Tactic:
exact a.ord_cof_le

Premises used: Ordinal.ord_cof_le
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a b o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : (↑(Iio b) : Type (u_1 + 1)) → (↑(Iio a) : Type (u_1 + 1))
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
rw : IsCofinal (f '' range g)
⊢ IsCofinal (range (f ∘ g))

Tactic:
rw [range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a b o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : (↑(Iio b) : Type (u_1 + 1)) → (↑(Iio a) : Type (u_1 + 1))
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ IsCofinal (f '' range g)

Tactic:
hg.isCofinal_range.image hf.strictMono.monotone hf.isCofinal_range

Premises used: StrictMono.monotone, Ordinal.IsFundamentalSeq.strictMono, IsCofinal.image, Ordinal.IsFundamentalSeq.isCofinal_range
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a b o : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → (↑(Iio o) : Type (u_1 + 1))
g : (↑(Iio b) : Type (u_1 + 1)) → (↑(Iio a) : Type (u_1 + 1))
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ IsCofinal (f '' range g)

Tactic:
exact hg.isCofinal_range.image hf.strictMono.monotone hf.isCofinal_range

Premises used: StrictMono.monotone, Ordinal.IsFundamentalSeq.strictMono, IsCofinal.image, Ordinal.IsFundamentalSeq.isCofinal_range
-- 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
rw : a ≤ o.cof.ord
rw₁ rw₂ : a ≤ a
⊢ a ≤ (g o).cof.ord

Tactic:
rw [cof_map_of_isNormal hg ho, hf.ord_cof]

Premises used: Ordinal.cof_map_of_isNormal, Ordinal.IsFundamentalSeq.ord_cof
-- 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)
⊢ ∃ a' < o, b < g a'

Tactic:
rw [mem_Iio, hg.lt_iff_exists_lt ho] at hb

Premises used: Set.mem_Iio, Order.IsNormal.lt_iff_exists_lt
-- 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_1 : b ∈ Iio (g o)
hb : ∃ a' < o, b < g a'
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})) ⋯)
          y ∧
        Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio (g o)) b hb_1 ≤ 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_1 ≤ y

Tactic:
obtain ⟨c, hc, hc'⟩ := hb