awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ nfpFamily f a
have refine_2 : f i b ≤ f i (nfpFamily f a)
Tactic: rw [← nfpFamily_fp (H i)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
⊢ nfpFamily f a = a
have apply : ∀ (i : List ι), List.foldr f a i ≤ a
Tactic: apply (Ordinal.iSup_le ?_).antisymm (le_nfpFamily f a)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
l : List ι
⊢ List.foldr f a l ≤ a
have rw : a ≤ a
Tactic: rw [List.foldr_fixed' h l]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ¬BddAbove.{u + 1} (α := Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i))
have rw : ∀ (x : Ordinal.{u}), ∃ (y : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) y ∧ x < y
Tactic: rw [not_bddAbove_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (x : Ordinal.{u}),
    ∃ (y : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) y ∧ x < y
have refine : ∀ (a : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) (nfpFamily f (succ a))
Tactic: refine fun a ↦ ⟨nfpFamily f (succ a), ?_, (lt_succ a).trans_le (le_nfpFamily f _)⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
⊢ IsNormal (derivFamily f)
have refine_1 : ∀ (o : Ordinal.{u}), derivFamily f o < derivFamily f (succ o)
Tactic: refine IsNormal.of_succ_lt (fun o ↦ ?_) @fun o h ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
refine_1 : ∀ (o : Ordinal.{u}), derivFamily f o < derivFamily f (succ o)
⊢ IsNormal (derivFamily f)
have refine_2 : ∀ (o : Ordinal.{u}) (h : IsSuccLimit o), IsLUB (derivFamily f '' Set.Iio o) (derivFamily f o)
Tactic: refine IsNormal.of_succ_lt (fun o ↦ ?_) @fun o h ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ derivFamily f o < derivFamily f (succ o)
have refine_1 : succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))
Tactic: rw [derivFamily_succ, ← succ_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
⊢ IsLUB (derivFamily f '' Set.Iio o) (derivFamily f o)
have 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}))
Tactic: rw [derivFamily_limit _ h, Set.image_eq_range]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
⊢ 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}))
have this : Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))
Tactic: have := h.nonempty_Iio.to_subtype
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
⊢ f i (derivFamily f 0) = derivFamily f 0
have zero : f i (nfpFamily f 0) = nfpFamily f 0
Tactic: rw [derivFamily_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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 (derivFamily f (o + 1)) = derivFamily f (o + 1)
have add_one : f i (nfpFamily f (derivFamily f o + 1)) = nfpFamily f (derivFamily f o + 1)
Tactic: rw [derivFamily_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
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'
⊢ f i (derivFamily f o) = derivFamily f o
have this : Nonempty.{u + 2} (↑(Set.Iio o) : Type (u + 1))
Tactic: have := l.nonempty_Iio.to_subtype
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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))
⊢ f i (derivFamily f o) = derivFamily f o
have 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}))
Tactic: rw [derivFamily_limit _ l, H.map_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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}))
have 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
Tactic: refine eq_of_forall_ge_iff fun c => ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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 ↔
    ⨆ (b : (↑(Set.Iio o) : Type (u + 1))), derivFamily f (↑b : Ordinal.{u}) ≤ c
have 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
Tactic: rw [Ordinal.iSup_le_iff, Ordinal.iSup_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
have limit : ∀ (a : (↑(Set.Iio o) : Type (u + 1))), f i (derivFamily f (↑a : Ordinal.{u})) ≤ c ↔ derivFamily f (↑a : Ordinal.{u}) ≤ c
Tactic: refine forall_congr' fun a ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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))
⊢ f i (derivFamily f (↑a : Ordinal.{u})) ≤ c ↔ derivFamily f (↑a : Ordinal.{u}) ≤ c
have limit : derivFamily f (↑a : Ordinal.{u}) ≤ c ↔ derivFamily f (↑a : Ordinal.{u}) ≤ c
Tactic: rw [IH _ a.2]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
⊢ f i (derivFamily f o) = derivFamily f o
have zero : f i (derivFamily f 0) = derivFamily f 0
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]
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ f i (derivFamily f o) = derivFamily f o
have add_one : ∀ (o : Ordinal.{u}), f i (derivFamily f o) = derivFamily f o → f i (derivFamily f (o + 1)) = derivFamily f (o + 1)
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]
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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)
⊢ f i (derivFamily f o) = derivFamily f o
have 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
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]
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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}), derivFamily f o = a
have suffices : ∀ (o : Ordinal.{u}), a ≤ derivFamily f o → ∃ (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
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
have zero : derivFamily f 0 ≤ a
Tactic: refine ⟨0, le_antisymm ?_ h₁⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ derivFamily f 0 ≤ a
have zero : nfpFamily f 0 ≤ a
Tactic: rw [derivFamily_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a
have add_one₁ : ∀ (h : derivFamily f o < a), ∃ (o : Ordinal.{u}), derivFamily f o = a
Tactic: rcases le_or_gt a (derivFamily f o) with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
have add_one : derivFamily f (o + 1) ≤ a
Tactic: refine ⟨o + 1, le_antisymm ?_ h₁⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ derivFamily f (o + 1) ≤ a
have add_one : nfpFamily f (derivFamily f o + 1) ≤ a
Tactic: rw [derivFamily_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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 : Ordinal.{u}), derivFamily f o = a
have limit : ∀ (h : a = derivFamily f o), ∃ (o : Ordinal.{u}), derivFamily f o = a
Tactic: rcases eq_or_lt_of_le h₁ with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a
have limit₁ : ∀ (h : a < derivFamily f o), ∃ (o : Ordinal.{u}), derivFamily f o = a
Tactic: rcases eq_or_lt_of_le h₁ with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
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
have h₂ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ ∃ (o : Ordinal.{u}), derivFamily f o = a
have limit : ∀ (o' : (↑(Set.Iio o) : Type (u + 1))) (h : ¬derivFamily f (↑o' : Ordinal.{u}) ≤ a),
  ∃ (o : Ordinal.{u}), derivFamily f o = a
Tactic: obtain ⟨o', h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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}
⊢ a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
have zero : a ≤ derivFamily f 0 → ∃ (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)
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
have 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
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)
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ a ≤ derivFamily f o → ∃ (o : Ordinal.{u}), derivFamily f o = a
have 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
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)
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ derivFamily f = enumOrd (⋂ (i : ι), fixedPoints (f i))
have rw : StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
Tactic: rw [eq_comm, eq_enumOrd _ (not_bddAbove_fp_family H)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
have right : Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
Tactic: use (isNormal_derivFamily f).strictMono
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ Set.range (derivFamily f) = ⋂ (i : ι), fixedPoints (f i)
have 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
Tactic: rw [Set.range_eq_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
have right : ∀ (a : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) (derivFamily f a)
Tactic: refine ⟨?_, fun a ha => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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)
⊢ (∀ (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
have right₁ : ∀ (a : Ordinal.{u}) (ha : Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) a),
  ∃ (a_1 : Ordinal.{u}), derivFamily f a_1 = a
Tactic: refine ⟨?_, fun a ha => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ derivFamily f a ∈ S
have right : Membership.mem (γ := Set Ordinal.{u}) ((fun (i : ι) ↦ fixedPoints (f i)) i) (derivFamily f a)
Tactic: rw [← hi]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
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
⊢ ∃ (a_1 : Ordinal.{u}), derivFamily f a_1 = a
have ha₁ : ∀ (i : ι), a ∈ fixedPoints (f i)
Tactic: rw [Set.mem_iInter] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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)
⊢ ∃ (a_1 : Ordinal.{u}), derivFamily f a_1 = a
have right : ∀ (i : ι), f i a = a
Tactic: rwa [← fp_iff_derivFamily H]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ⨆ (n : ℕ), f^[n] a = nfp f a
have a₁ : ⨆ (n : ℕ), f^[n] a ≤ nfp f a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
a₁ : ⨆ (n : ℕ), f^[n] a ≤ nfp f a
⊢ ⨆ (n : ℕ), f^[n] a = nfp f a
have a₂ : nfp f a ≤ ⨆ (n : ℕ), f^[n] a
Tactic: apply le_antisymm