awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
refine_1 : succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))
⊢ derivFamily f o < derivFamily f (succ o)

Tactic:
rw [derivFamily_succ, ← succ_le_iff]

Premises used: Ordinal.derivFamily_succ, Order.succ_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))

Tactic:
le_nfpFamily _ _

Premises used: Ordinal.le_nfpFamily
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))

Tactic:
exact le_nfpFamily _ _

Premises used: Ordinal.le_nfpFamily
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
refine_2 :
  IsLUB.{u + 1} (α := Ordinal.{u})
    (Set.range fun (x : (↑(Set.Iio o) : Type (u + 1))) ↦ derivFamily f (↑x : Ordinal.{u}))
    (⨆ (b : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑b : Ordinal.{u}))
⊢ IsLUB (derivFamily f '' Set.Iio o) (derivFamily f o)

Tactic:
rw [derivFamily_limit _ h, Set.image_eq_range]

Premises used: Set.image_eq_range, Ordinal.derivFamily_limit
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
⊢ Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))

Tactic:
have := h.nonempty_Iio.to_subtype
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
this : Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))
⊢ IsLUB.{u + 1} (α := Ordinal.{u})
    (Set.range fun (x : (↑(Set.Iio o) : Type (u + 1))) ↦ derivFamily f (↑x : Ordinal.{u}))
    (⨆ (b : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑b : Ordinal.{u}))

Tactic:
isLUB_ciSup bddAbove_of_small

Premises used: isLUB_ciSup, Ordinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
this : Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))
⊢ IsLUB.{u + 1} (α := Ordinal.{u})
    (Set.range fun (x : (↑(Set.Iio o) : Type (u + 1))) ↦ derivFamily f (↑x : Ordinal.{u}))
    (⨆ (b : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑b : Ordinal.{u}))

Tactic:
exact isLUB_ciSup bddAbove_of_small

Premises used: isLUB_ciSup, Ordinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
⊢ StrictMono (derivFamily f)

Tactic:
(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} ι
i : ι
H : IsNormal (f i)
zero : f i (nfpFamily f 0) = nfpFamily f 0
⊢ f i (derivFamily f 0) = derivFamily f 0

Tactic:
rw [derivFamily_zero]

Premises used: Ordinal.derivFamily_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
⊢ f i (nfpFamily f 0) = nfpFamily f 0

Tactic:
nfpFamily_fp H 0

Premises used: OfNat.ofNat, Ordinal.nfpFamily_fp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
⊢ f i (nfpFamily f 0) = nfpFamily f 0

Tactic:
exact nfpFamily_fp H 0

Premises used: OfNat.ofNat, Ordinal.nfpFamily_fp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
h : f i (derivFamily f o) = derivFamily f o
add_one : f i (nfpFamily f (derivFamily f o + 1)) = nfpFamily f (derivFamily f o + 1)
⊢ f i (derivFamily f (o + 1)) = derivFamily f (o + 1)

Tactic:
rw [derivFamily_add_one]

Premises used: Ordinal.derivFamily_add_one
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
h : f i (derivFamily f o) = derivFamily f o
⊢ f i (nfpFamily f (derivFamily f o + 1)) = nfpFamily f (derivFamily f o + 1)

Tactic:
nfpFamily_fp H _

Premises used: Ordinal.nfpFamily_fp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
h : f i (derivFamily f o) = derivFamily f o
⊢ f i (nfpFamily f (derivFamily f o + 1)) = nfpFamily f (derivFamily f o + 1)

Tactic:
exact nfpFamily_fp H _

Premises used: Ordinal.nfpFamily_fp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
⊢ Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))

Tactic:
have := l.nonempty_Iio.to_subtype
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))
limit :
  Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i_1 : (↑(Set.Iio o) : Type (u + 1))), f i (derivFamily f (↑i_1 : Ordinal.{u})))
    (⨆ (b : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑b : Ordinal.{u}))
⊢ f i (derivFamily f o) = derivFamily f o

Tactic:
rw [derivFamily_limit _ l, H.map_iSup bddAbove_of_small]

Premises used: Ordinal.bddAbove_of_small, Ordinal.derivFamily_limit, Order.IsNormal.map_iSup
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i_1 : (↑(Set.Iio o) : Type (u + 1))), f i (derivFamily f (↑i_1 : Ordinal.{u})))
    (⨆ (b : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑b : Ordinal.{u}))

Tactic:
eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))
limit :
  ∀ (c : Ordinal.{u}),
    ⨆ (i_1 : (↑(Set.Iio o) : Type (u + 1))), f i (derivFamily f (↑i_1 : Ordinal.{u})) ≤ c ↔
      ⨆ (b : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑b : Ordinal.{u}) ≤ c
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i_1 : (↑(Set.Iio o) : Type (u + 1))), f i (derivFamily f (↑i_1 : Ordinal.{u})))
    (⨆ (b : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑b : Ordinal.{u}))

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))
c : Ordinal.{u}
limit :
  (∀ (i_1 : (↑(Set.Iio o) : Type (u + 1))), f i (derivFamily f (↑i_1 : Ordinal.{u})) ≤ c) ↔
    ∀ (i : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑i : Ordinal.{u}) ≤ c
⊢ ⨆ (i_1 : (↑(Set.Iio o) : Type (u + 1))), f i (derivFamily f (↑i_1 : Ordinal.{u})) ≤ c ↔
    ⨆ (b : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑b : Ordinal.{u}) ≤ c

Tactic:
rw [Ordinal.iSup_le_iff, Ordinal.iSup_le_iff]

Premises used: Ordinal.iSup_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))
c : Ordinal.{u}
⊢ (∀ (i_1 : (↑(Set.Iio o) : Type (u + 1))), f i (derivFamily f (↑i_1 : Ordinal.{u})) ≤ c) ↔
    ∀ (i : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑i : Ordinal.{u}) ≤ c

Tactic:
forall_congr' fun a ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))
c : Ordinal.{u}
limit :
  ∀ (a : (↑(Set.Iio o) : Type (u + 1))),
    f i (derivFamily f (↑a : Ordinal.{u})) ≤ c ↔ derivFamily f (↑a : Ordinal.{u}) ≤ c
⊢ (∀ (i_1 : (↑(Set.Iio o) : Type (u + 1))), f i (derivFamily f (↑i_1 : Ordinal.{u})) ≤ c) ↔
    ∀ (i : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑i : Ordinal.{u}) ≤ c

Tactic:
refine forall_congr' fun a ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))
c : Ordinal.{u}
a : (↑(Set.Iio o) : Type (u + 1))
limit limit₁ : derivFamily f (↑a : Ordinal.{u}) ≤ c ↔ derivFamily f (↑a : Ordinal.{u}) ≤ c
⊢ f i (derivFamily f (↑a : Ordinal.{u})) ≤ c ↔ derivFamily f (↑a : Ordinal.{u}) ≤ c

Tactic:
rw [IH _ a.2]

Premises used: Subtype.property
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
zero : f i (derivFamily f 0) = derivFamily f 0
add_one :
  ∀ (o : Ordinal.{u}), f i (derivFamily f o) = derivFamily f o → f i (derivFamily f (o + 1)) = derivFamily f (o + 1)
limit :
  ∀ (o : Ordinal.{u}) (l : IsSuccLimit o) (IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'),
    f i (derivFamily f o) = derivFamily f o
⊢ f i (derivFamily f o) = derivFamily f o

Tactic:
induction o using limitRecOn with
  | zero =>
    rw [derivFamily_zero]
    exact nfpFamily_fp H 0
  | add_one =>
    rw [derivFamily_add_one]
    exact nfpFamily_fp H _
  | limit o l IH =>
    have := l.nonempty_Iio.to_subtype
    rw [derivFamily_limit _ l, H.map_iSup bddAbove_of_small]
    refine eq_of_forall_ge_iff fun c => ?_
    rw [Ordinal.iSup_le_iff, Ordinal.iSup_le_iff]
    refine forall_congr' fun a ↦ ?_
    rw [IH _ a.2]

Premises used: eq_of_forall_ge_iff, Ordinal.derivFamily_add_one, Ordinal.bddAbove_of_small, Order.IsNormal.map_iSup, Ordinal.zero, Ordinal.derivFamily_zero, forall_congr', Ordinal.iSup_le_iff, OfNat.ofNat, Ordinal.nfpFamily_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 : ∀ (i : ι), f i a ≤ a
suffices : ∀ (o : Ordinal.{u}), a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
suffices ∀ (o), a ≤ derivFamily f o → ∃ o, derivFamily f o = a from
      this a (isNormal_derivFamily _).strictMono.le_apply
-- 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 : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
⟨0, le_antisymm ?_ h₁⟩

Premises used: le_antisymm, Exists.intro, OfNat.ofNat
-- 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 : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
zero : derivFamily f 0 ≤ a
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
refine ⟨0, le_antisymm ?_ h₁⟩
-- 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 : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
zero : nfpFamily f 0 ≤ a
⊢ derivFamily f 0 ≤ a

Tactic:
rw [derivFamily_zero]

Premises used: Ordinal.derivFamily_zero
-- 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 : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ nfpFamily f 0 ≤ a

Tactic:
nfpFamily_le_fp (fun i => (H i).monotone) zero_le ha

Premises used: zero_le, Order.IsNormal.monotone, Ordinal.nfpFamily_le_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 : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ nfpFamily f 0 ≤ a

Tactic:
exact nfpFamily_le_fp (fun i => (H i).monotone) zero_le ha

Premises used: zero_le, Order.IsNormal.monotone, Ordinal.nfpFamily_le_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 : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
add_one : ∀ (h : a ≤ derivFamily f o), ∃ (o : Ordinal.{u}), derivFamily f o = a
add_one₁ : ∀ (h : derivFamily f o < a), ∃ (o : Ordinal.{u}), derivFamily f o = a
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
rcases le_or_gt a (derivFamily f o) with h | h

Premises used: le_or_gt, Ordinal.derivFamily
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : a ≤ derivFamily f o
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
IH h
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : a ≤ derivFamily f o
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
exact IH h
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
⟨o + 1, le_antisymm ?_ h₁⟩

Premises used: le_antisymm, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
add_one : derivFamily f (o + 1) ≤ a
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
refine ⟨o + 1, le_antisymm ?_ h₁⟩
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
add_one : nfpFamily f (derivFamily f o + 1) ≤ a
⊢ derivFamily f (o + 1) ≤ a

Tactic:
rw [derivFamily_add_one]

Premises used: Ordinal.derivFamily_add_one
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ nfpFamily f (derivFamily f o + 1) ≤ a

Tactic:
nfpFamily_le_fp (fun i => (H i).monotone) (succ_le_of_lt h) ha

Premises used: Order.IsNormal.monotone, Ordinal.nfpFamily_le_fp, Order.succ_le_of_lt
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ nfpFamily f (derivFamily f o + 1) ≤ a

Tactic:
exact nfpFamily_le_fp (fun i => (H i).monotone) (succ_le_of_lt h) ha

Premises used: Order.IsNormal.monotone, Ordinal.nfpFamily_le_fp, Order.succ_le_of_lt
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f o
limit : ∀ (h : a = derivFamily f o), ∃ (o : Ordinal.{u}), derivFamily f o = a
limit₁ : ∀ (h : a < derivFamily f o), ∃ (o : Ordinal.{u}), derivFamily f o = a
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
rcases eq_or_lt_of_le h₁ with h | h

Premises used: eq_or_lt_of_le
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a = derivFamily f o
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
⟨_, h.symm⟩

Premises used: Exists.intro, Eq.symm
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a = derivFamily f o
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
exact ⟨_, h.symm⟩
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a < derivFamily f o
⊢ ∃ (x : (↑(Set.Iio o) : Type (u + 1))), ¬derivFamily f (↑x : Ordinal.{u}) ≤ a

Tactic:
rw [derivFamily_limit _ l, ← not_le, Ordinal.iSup_le_iff, not_forall] at h

Premises used: not_le, Ordinal.derivFamily_limit, Ordinal.iSup_le_iff, Classical.not_forall
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : ∃ (x : (↑(Set.Iio o) : Type (u + 1))), ¬derivFamily f (↑x : Ordinal.{u}) ≤ a
limit :
  ∀ (o' : (↑(Set.Iio o) : Type (u + 1))) (h : ¬derivFamily f (↑o' : Ordinal.{u}) ≤ a),
    ∃ (o : Ordinal.{u}), derivFamily f o = a
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
obtain ⟨o', h⟩ := h
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f o
o' : (↑(Set.Iio o) : Type (u + 1))
h : ¬derivFamily f (↑o' : Ordinal.{u}) ≤ a
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
IH o' o'.2 (le_of_not_ge h)

Premises used: le_of_not_ge, Subtype.val, Subtype.property
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ (o : Ordinal.{u}), derivFamily f o = a
h₁ : a ≤ derivFamily f o
o' : (↑(Set.Iio o) : Type (u + 1))
h : ¬derivFamily f (↑o' : Ordinal.{u}) ≤ a
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
exact IH o' o'.2 (le_of_not_ge h)

Premises used: le_of_not_ge, Subtype.val, Subtype.property
-- 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 : ι), f i a ≤ a
o : Ordinal.{u}
zero : a ≤ derivFamily f 0 → ∃ (o : Ordinal.{u}), derivFamily f o = a
add_one :
  ∀ (o : Ordinal.{u}) (IH : a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a),
    a ≤ derivFamily f (o + 1) → ∃ (o : Ordinal.{u}), derivFamily f o = a
limit :
  ∀ (o : Ordinal.{u}) (l : IsSuccLimit o)
    (IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ (o : Ordinal.{u}), derivFamily f o = a),
    a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
⊢ a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
induction o using limitRecOn with
    | zero =>
      intro h₁
      refine ⟨0, le_antisymm ?_ h₁⟩
      rw [derivFamily_zero]
      exact nfpFamily_le_fp (fun i => (H i).monotone) zero_le ha
    | add_one o IH =>
      intro h₁
      rcases le_or_gt a (derivFamily f o) with h | h
      · exact IH h
      refine ⟨o + 1, le_antisymm ?_ h₁⟩
      rw [derivFamily_add_one]
      exact nfpFamily_le_fp (fun i => (H i).monotone) (succ_le_of_lt h) ha
    | limit o l IH =>
      intro h₁
      rcases eq_or_lt_of_le h₁ with h | h
      · exact ⟨_, h.symm⟩
      rw [derivFamily_limit _ l, ← not_le, Ordinal.iSup_le_iff, not_forall] at h
      obtain ⟨o', h⟩ := h
      exact IH o' o'.2 (le_of_not_ge h)

Premises used: not_le, zero_le, Order.IsNormal.monotone, Ordinal.nfpFamily_le_fp, Ordinal.derivFamily_add_one, le_or_gt, Ordinal.zero, Ordinal.derivFamily_zero, Ordinal.derivFamily, Ordinal.iSup_le_iff, Classical.not_forall
-- 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}
⊢ (∀ (i : ι), f i a = a) ↔ ∃ (o : Ordinal.{u}), derivFamily f o = a

Tactic:
Iff.trans ⟨fun h i => le_of_eq (h i), fun h i => (H i).strictMono.le_apply.ge_iff_eq'.1 (h i)⟩
    (le_iff_derivFamily H)

Premises used: StrictMono.le_apply, Ordinal.le_iff_derivFamily, LE.le.ge_iff_eq', Iff.intro, Iff.mp, Iff.trans, le_of_eq, 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)
a : Ordinal.{u}
⊢ a ∈ Set.range (derivFamily f) ↔ ∀ (i : ι), f i a = a

Tactic:
(fp_iff_derivFamily H).symm

Premises used: Ordinal.fp_iff_derivFamily, Set.Mem, setOf, Set.range, Iff.symm
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
rw : StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
⊢ derivFamily f = enumOrd (⋂ (i : ι), fixedPoints (f i))

Tactic:
rw [eq_comm, eq_enumOrd _ (not_bddAbove_fp_family H)]

Premises used: Ordinal.not_bddAbove_fp_family, eq_comm, Ordinal.eq_enumOrd