awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
right : Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
⊢ StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)

Tactic:
use (isNormal_derivFamily f).strictMono

Premises used: Ordinal.isNormal_derivFamily, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
right :
  (∀ (a : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) (derivFamily f a)) ∧
    ∀ (b : Ordinal.{u}),
      Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) b → ∃ (a : Ordinal.{u}), derivFamily f a = b
⊢ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)

Tactic:
rw [Set.range_eq_iff]

Premises used: Set.range_eq_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ (∀ (a : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) (derivFamily f a)) ∧
    ∀ (b : Ordinal.{u}),
      Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) b → ∃ (a : Ordinal.{u}), derivFamily f a = b

Tactic:
⟨?_, fun a ha => ?_⟩

Premises used: And.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
right : ∀ (a : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) (derivFamily f a)
right₁ :
  ∀ (a : Ordinal.{u}) (ha : Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) a),
    ∃ (a_1 : Ordinal.{u}), derivFamily f a_1 = a
⊢ (∀ (a : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) (derivFamily f a)) ∧
    ∀ (b : Ordinal.{u}),
      Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) b → ∃ (a : Ordinal.{u}), derivFamily f a = b

Tactic:
refine ⟨?_, fun a ha => ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
S : Set Ordinal.{u}
i : ι
hi : (fun (i : ι) ↦ fixedPoints (f i)) i = S
right : Membership.mem (γ := Set Ordinal.{u}) ((fun (i : ι) ↦ fixedPoints (f i)) i) (derivFamily f a)
⊢ derivFamily f a ∈ S

Tactic:
rw [← hi]
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
S : Set Ordinal.{u}
i : ι
hi : (fun (i : ι) ↦ fixedPoints (f i)) i = S
⊢ Membership.mem (γ := Set Ordinal.{u}) ((fun (i : ι) ↦ fixedPoints (f i)) i) (derivFamily f a)

Tactic:
derivFamily_fp (H i) a

Premises used: Set.Mem, setOf, Function.fixedPoints, Function.IsFixedPt, Ordinal.derivFamily_fp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
S : Set Ordinal.{u}
i : ι
hi : (fun (i : ι) ↦ fixedPoints (f i)) i = S
⊢ Membership.mem (γ := Set Ordinal.{u}) ((fun (i : ι) ↦ fixedPoints (f i)) i) (derivFamily f a)

Tactic:
exact derivFamily_fp (H i) a

Premises used: Ordinal.derivFamily_fp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) a
⊢ ∀ (i : ι), a ∈ fixedPoints (f i)

Tactic:
rw [Set.mem_iInter] at ha

Premises used: Set.mem_iInter
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
right right₁ right₂ right₃ : ∀ (i : ι), f i a = a
⊢ ∃ (a_1 : Ordinal.{u}), derivFamily f a_1 = a

Tactic:
rwa [← fp_iff_derivFamily H]

Premises used: Ordinal.fp_iff_derivFamily
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ nfp f = nfpFamily fun (x : Unit) ↦ f

Tactic:
rfl

Premises used: Ordinal.nfp, rfl
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
a₁ : ⨆ (n : ℕ), f^[n] a ≤ nfp f a
a₂ : nfp f a ≤ ⨆ (n : ℕ), f^[n] a
⊢ ⨆ (n : ℕ), f^[n] a = nfp f a

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
a₁ : ∀ (i : ℕ), f^[i] a ≤ nfp f a
⊢ ⨆ (n : ℕ), f^[n] a ≤ nfp f a

Tactic:
rw [Ordinal.iSup_le_iff]

Premises used: Ordinal.iSup_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
a₁ : List.foldr (fun (x : Unit) ↦ f) a (List.replicate n ()) ≤ nfp f a
⊢ f^[n] a ≤ nfp f a

Tactic:
rw [← List.length_replicate (n := n) (a := Unit.unit), ← List.foldr_const f a]

Premises used: List.length_replicate, List.foldr_const
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ List.foldr (fun (x : Unit) ↦ f) a (List.replicate n ()) ≤ nfp f a

Tactic:
Ordinal.le_iSup _ _

Premises used: Ordinal.nfpFamily, Ordinal.nfp, Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ List.foldr (fun (x : Unit) ↦ f) a (List.replicate n ()) ≤ nfp f a

Tactic:
exact Ordinal.le_iSup _ _

Premises used: Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
a₁ : ∀ (i : List Unit), List.foldr (fun (x : Unit) ↦ f) a i ≤ ⨆ (n : ℕ), f^[n] a
⊢ nfp f a ≤ ⨆ (n : ℕ), f^[n] a

Tactic:
apply Ordinal.iSup_le

Premises used: Ordinal.iSup_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
a₁ : f^[l.length] a ≤ ⨆ (n : ℕ), f^[n] a
⊢ List.foldr (fun (x : Unit) ↦ f) a l ≤ ⨆ (n : ℕ), f^[n] a

Tactic:
rw [List.foldr_const f a l]

Premises used: List.foldr_const
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ f^[l.length] a ≤ ⨆ (n : ℕ), f^[n] a

Tactic:
Ordinal.le_iSup _ _

Premises used: Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ f^[l.length] a ≤ ⨆ (n : ℕ), f^[n] a

Tactic:
exact Ordinal.le_iSup _ _

Premises used: Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
rw : f^[n] a ≤ ⨆ (n : ℕ), f^[n] a
⊢ f^[n] a ≤ nfp f a

Tactic:
rw [← iSup_iterate_eq_nfp]

Premises used: Ordinal.iSup_iterate_eq_nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ ⨆ (n : ℕ), f^[n] a

Tactic:
Ordinal.le_iSup (fun n ↦ f^[n] a) n

Premises used: Nat.iterate, Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ ⨆ (n : ℕ), f^[n] a

Tactic:
exact Ordinal.le_iSup (fun n ↦ f^[n] a) n

Premises used: Nat.iterate, Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
⊢ a ≤ nfp f a

Tactic:
iterate_le_nfp f a 0

Premises used: Ordinal.iterate_le_nfp, Nat.iterate, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
rw : a < ⨆ (n : ℕ), f^[n] b ↔ ∃ (n : ℕ), a < f^[n] b
⊢ a < nfp f b ↔ ∃ (n : ℕ), a < f^[n] b

Tactic:
rw [← iSup_iterate_eq_nfp]

Premises used: Ordinal.iSup_iterate_eq_nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < ⨆ (n : ℕ), f^[n] b ↔ ∃ (n : ℕ), a < f^[n] b

Tactic:
Ordinal.lt_iSup_iff

Premises used: Ordinal.lt_iSup_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < ⨆ (n : ℕ), f^[n] b ↔ ∃ (n : ℕ), a < f^[n] b

Tactic:
exact Ordinal.lt_iSup_iff

Premises used: Ordinal.lt_iSup_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
rw : ⨆ (n : ℕ), f^[n] a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
⊢ nfp f a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b

Tactic:
rw [← iSup_iterate_eq_nfp]

Premises used: Ordinal.iSup_iterate_eq_nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ ⨆ (n : ℕ), f^[n] a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b

Tactic:
Ordinal.iSup_le_iff

Premises used: Ordinal.iSup_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ ⨆ (n : ℕ), f^[n] a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b

Tactic:
exact Ordinal.iSup_le_iff

Premises used: Ordinal.iSup_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ (∀ (n : ℕ), f^[n] a ≤ b) → nfp f a ≤ b

Tactic:
nfp_le_iff.2

Premises used: Iff.mpr, Ordinal.nfp_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
h : ∀ (x : Ordinal.{u_1}), nfp id x = id x
⊢ nfp id = id

Tactic:
ext
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
x : Ordinal.{u_1}
h : ⨆ (n : ℕ), id x = id x
⊢ nfp id x = id x

Tactic:
simp_rw [← iSup_iterate_eq_nfp, iterate_id]

Premises used: Function.iterate_id, Ordinal.iSup_iterate_eq_nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
x : Ordinal.{u_1}
⊢ ⨆ (n : ℕ), id x = id x

Tactic:
ciSup_const

Premises used: ciSup_const
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
x : Ordinal.{u_1}
⊢ ⨆ (n : ℕ), id x = id x

Tactic:
exact ciSup_const

Premises used: ciSup_const
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : Monotone f
⊢ Monotone (nfp f)

Tactic:
nfpFamily_monotone fun _ => hf

Premises used: Ordinal.nfp, Ordinal.nfpFamily_monotone
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
apply : f^[n] (f a) ≤ nfp f a
⊢ f^[n] a < nfp f a

Tactic:
apply (hf.iterate n h).trans_le

Premises used: StrictMono.iterate, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
rw : f^[n.succ] a ≤ nfp f a
⊢ f^[n] (f a) ≤ nfp f a

Tactic:
rw [← iterate_succ_apply]

Premises used: Function.iterate_succ_apply
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
⊢ f^[n.succ] a ≤ nfp f a

Tactic:
iterate_le_nfp ..

Premises used: Ordinal.iterate_le_nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
⊢ f^[n.succ] a ≤ nfp f a

Tactic:
exact iterate_le_nfp ..

Premises used: Ordinal.iterate_le_nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
unfold : f b < nfpFamily (fun (x : Unit) ↦ f) a ↔ b < nfpFamily (fun (x : Unit) ↦ f) a
⊢ f b < nfp f a ↔ b < nfp f a

Tactic:
unfold nfp

Premises used: Ordinal.nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
rw : f b < nfpFamily (fun (x : Unit) ↦ f) a ↔ ∀ (i : Unit), f b < nfpFamily (fun (x : Unit) ↦ f) a
⊢ f b < nfpFamily (fun (x : Unit) ↦ f) a ↔ b < nfpFamily (fun (x : Unit) ↦ f) a

Tactic:
rw [← @apply_lt_nfpFamily_iff Unit (fun _ => f) _ _ (fun _ => H) a b]

Premises used: Ordinal.apply_lt_nfpFamily_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfpFamily (fun (x : Unit) ↦ f) a ↔ ∀ (i : Unit), f b < nfpFamily (fun (x : Unit) ↦ f) a

Tactic:
⟨fun h _ => h, fun h => h Unit.unit⟩

Premises used: Unit.unit, Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfpFamily (fun (x : Unit) ↦ f) a ↔ ∀ (i : Unit), f b < nfpFamily (fun (x : Unit) ↦ f) a

Tactic:
exact ⟨fun h _ => h, fun h => h Unit.unit⟩
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ nfp f a ≤ f b ↔ nfp f a ≤ b

Tactic:
le_iff_le_iff_lt_iff_lt.2 (apply_lt_nfp H)

Premises used: Iff.mpr, le_iff_le_iff_lt_iff_lt, Ordinal.apply_lt_nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : Monotone f
a b : Ordinal.{u}
ab : a ≤ b
h : f b ≤ b
⊢ nfp f a ≤ b

Tactic:
nfpFamily_le_fp (fun _ => H) ab fun _ => h

Premises used: Ordinal.nfpFamily_le_fp, Ordinal.nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ ∀ (a : Ordinal.{u}), f (nfp f a) = nfp f a

Tactic:
@nfpFamily_fp Unit (fun _ => f) _ () H

Premises used: Ordinal.nfp, Ordinal.nfpFamily_fp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
h : b ≤ nfp f a
⊢ f b ≤ nfp f a

Tactic:
simpa only [nfp_fp H] using H.monotone h

Premises used: Ordinal.nfp_fp, Order.IsNormal.monotone
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
h : f a = a
⊢ nfp f a = a

Tactic:
nfpFamily_eq_self fun _ => h

Premises used: Ordinal.nfpFamily_eq_self, Ordinal.nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ ¬BddAbove.{u + 1} (α := Ordinal.{u}) (⋂ (i : Unit), fixedPoints f)

Tactic:
not_bddAbove_fp_family fun _ : Unit => H

Premises used: Ordinal.not_bddAbove_fp_family
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
h : fixedPoints f = ⋂ (i : Unit), fixedPoints f
⊢ ¬BddAbove (fixedPoints f)

Tactic:
convert! not_bddAbove_fp_family fun _ : Unit => H

Premises used: Ordinal.not_bddAbove_fp_family
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ (i : Unit), fixedPoints f

Tactic:
(Set.iInter_const _).symm

Premises used: Set.iInter_const, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ (i : Unit), fixedPoints f

Tactic:
exact (Set.iInter_const _).symm

Premises used: Set.iInter_const, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ deriv f = derivFamily fun (x : Unit) ↦ f

Tactic:
rfl

Premises used: Ordinal.deriv, rfl
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ deriv f 0 = nfp f 0

Tactic:
derivFamily_zero _

Premises used: Ordinal.nfp, Ordinal.deriv, Ordinal.derivFamily_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ deriv f (o + 1) = nfp f (deriv f o + 1)

Tactic:
derivFamily_succ _ _

Premises used: Order.succ, Ordinal.derivFamily_succ, Ordinal.nfp, Ordinal.deriv
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ deriv f (succ o) = nfp f (succ (deriv f o))

Tactic:
deriv_add_one ..

Premises used: Order.succ, Ordinal.deriv_add_one
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsSuccLimit o → deriv f o = ⨆ (a : { a : Ordinal.{u_1} // a < o }), deriv f (↑a : Ordinal.{u_1})

Tactic:
derivFamily_limit _

Premises used: Set.Mem, setOf, Ordinal.derivFamily_limit, Ordinal.deriv, Set.Iio
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ IsNormal (deriv f)

Tactic:
isNormal_derivFamily _

Premises used: Ordinal.isNormal_derivFamily, Ordinal.deriv
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ StrictMono (deriv f)

Tactic:
derivFamily_strictMono _

Premises used: Ordinal.derivFamily_strictMono, Ordinal.deriv
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
h : nfp f = id
⊢ deriv f ⊥ = id ⊥ ∧ ∀ (a : Ordinal.{u}), deriv f a = id a → deriv f (succ a) = id (succ a)

Tactic:
simp [h]
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ ∀ (o : Ordinal.{u}), f (deriv f o) = deriv f o

Tactic:
derivFamily_fp (i := ⟨⟩) H

Premises used: Ordinal.deriv, Ordinal.derivFamily_fp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
rw : f a ≤ a ↔ ∀ (i : Unit), f a ≤ a
⊢ f a ≤ a ↔ ∃ (o : Ordinal.{u}), derivFamily (fun (x : Unit) ↦ f) o = a

Tactic:
rw [← le_iff_derivFamily fun _ : Unit => H]

Premises used: Ordinal.le_iff_derivFamily
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∀ (i : Unit), f a ≤ a

Tactic:
⟨fun h _ => h, fun h => h Unit.unit⟩

Premises used: Unit.unit, Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∀ (i : Unit), f a ≤ a

Tactic:
exact ⟨fun h _ => h, fun h => h Unit.unit⟩
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
rw : (∃ (y : Ordinal.{u}), deriv f y = a) ↔ f a = a
rw₁ : (∃ (y : Ordinal.{u}), deriv f y = a) ↔ f a ≤ a
rw₂ rw₃ : (∃ (y : Ordinal.{u}), deriv f y = a) ↔ ∃ (o : Ordinal.{u}), deriv f o = a
⊢ a ∈ Set.range (deriv f) ↔ f a = a

Tactic:
rw [Set.mem_range, ← H.strictMono.le_apply.ge_iff_eq', le_iff_deriv H]

Premises used: StrictMono.le_apply, Set.mem_range, LE.le.ge_iff_eq', Order.IsNormal.strictMono, Ordinal.le_iff_deriv
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ (derivFamily fun (x : Unit) ↦ f) = enumOrd (⋂ (i : Unit), fixedPoints f)

Tactic:
derivFamily_eq_enumOrd fun _ : Unit => H

Premises used: Ordinal.derivFamily_eq_enumOrd
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
h : fixedPoints f = ⋂ (i : Unit), fixedPoints f
⊢ deriv f = enumOrd (fixedPoints f)

Tactic:
convert! derivFamily_eq_enumOrd fun _ : Unit => H

Premises used: Ordinal.derivFamily_eq_enumOrd
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
rw : ⨆ (n : ℕ), 0^[n] a = a
⊢ nfp 0 a = a

Tactic:
rw [← iSup_iterate_eq_nfp]

Premises used: Ordinal.iSup_iterate_eq_nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
apply : ∀ (i : ℕ), 0^[i] a ≤ 0^[0] a
⊢ ⨆ (n : ℕ), 0^[n] a = a

Tactic:
apply (Ordinal.iSup_le ?_).antisymm (Ordinal.le_iSup _ 0)

Premises used: Ordinal.iSup_le, LE.le.antisymm, Ordinal.le_iSup, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
n : ℕ
zero : 0^[0] a ≤ 0^[0] a
succ : ∀ (n : ℕ), 0^[n + 1] a ≤ 0^[0] a
⊢ 0^[n] a ≤ 0^[0] a

Tactic:
cases n
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
⊢ 0^[0] a ≤ 0^[0] a

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
n : ℕ
succ : (0 ∘ 0^[n]) a ≤ 0^[0] a
⊢ 0^[n + 1] a ≤ 0^[0] a

Tactic:
rw [Function.iterate_succ']

Premises used: Function.iterate_succ'
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
n : ℕ
⊢ (0 ∘ 0^[n]) a ≤ 0^[0] a

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
h : ∀ (x : Ordinal.{u_1}), nfp 0 x = id x
⊢ nfp 0 = id

Tactic:
ext
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
x : Ordinal.{u_1}
⊢ nfp 0 x = id x

Tactic:
nfp_zero_left _

Premises used: Ordinal.nfp_zero_left
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
x : Ordinal.{u_1}
⊢ nfp 0 x = id x

Tactic:
exact nfp_zero_left _

Premises used: Ordinal.nfp_zero_left
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
⊢ deriv 0 = id

Tactic:
deriv_eq_id_of_nfp_eq_id nfp_zero

Premises used: Ordinal.nfp_zero, Ordinal.deriv_eq_id_of_nfp_eq_id
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
rw : id a = a
rw₁ rw₂ : a = a
⊢ deriv 0 a = a

Tactic:
rw [deriv_zero, id_eq]

Premises used: Ordinal.deriv_zero, id_eq
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) 0 = a * ω

Tactic:
simp [← iSup_iterate_eq_nfp]

Premises used: Ordinal.iSup_iterate_eq_nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
apply : a * ω ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b
apply₁ : a + a * ω ≤ a * ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b = a * ω

Tactic:
apply le_antisymm (nfp_le_fp (isNormal_add_right a).monotone hba _)

Premises used: Ordinal.nfp_le_fp, Order.IsNormal.monotone, le_antisymm, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
rw : nfp (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b
⊢ a * ω ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b

Tactic:
rw [← nfp_add_zero]

Premises used: Ordinal.nfp_add_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b

Tactic:
nfp_monotone (isNormal_add_right a).monotone zero_le

Premises used: zero_le, Order.IsNormal.monotone, Ordinal.nfp_monotone, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b

Tactic:
exact nfp_monotone (isNormal_add_right a).monotone zero_le

Premises used: zero_le, Order.IsNormal.monotone, Ordinal.nfp_monotone, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
rw : a * (1 + ω) ≤ a * ω
rw₁ rw₂ : a * ω ≤ a * ω
⊢ a + a * ω ≤ a * ω

Tactic:
rw [← mul_one_add, one_add_omega0]

Premises used: Ordinal.one_add_omega0, mul_one_add
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
⊢ a + b = b ↔ a * ω ≤ b

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
refine_1 : ∀ (h : a + b = b), a * ω ≤ b
refine_2 : ∀ (h : a * ω ≤ b), a + b = b
⊢ a + b = b ↔ a * ω ≤ b

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
h : a + b = b
refine_1 : deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ b
⊢ a * ω ≤ b

Tactic:
rw [← nfp_add_zero a, ← deriv_zero_right]

Premises used: Ordinal.deriv_zero_right, Ordinal.nfp_add_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
h : a + b = b
refine_1 :
  ∀ (c : Ordinal.{u_1}) (hc : deriv (fun (x : Ordinal.{u_1}) ↦ a + x) c = b),
    deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ b
⊢ deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ b

Tactic:
obtain ⟨c, hc⟩ := (mem_range_deriv (isNormal_add_right a)).2 h

Premises used: Iff.mpr, Ordinal.mem_range_deriv, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun (x : Ordinal.{u_1}) ↦ a + x) c = b
refine_1 : deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ deriv (fun (x : Ordinal.{u_1}) ↦ a + x) c
⊢ deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ b

Tactic:
rw [← hc]
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun (x : Ordinal.{u_1}) ↦ a + x) c = b
⊢ deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ deriv (fun (x : Ordinal.{u_1}) ↦ a + x) c

Tactic:
(isNormal_deriv _).monotone zero_le

Premises used: zero_le, Order.IsNormal.monotone, Ordinal.isNormal_deriv
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun (x : Ordinal.{u_1}) ↦ a + x) c = b
⊢ deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ deriv (fun (x : Ordinal.{u_1}) ↦ a + x) c

Tactic:
exact (isNormal_deriv _).monotone zero_le

Premises used: zero_le, Order.IsNormal.monotone, Ordinal.isNormal_deriv