awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
s : Set Ordinal.{u}
inst : Small.{u, u + 1} (↑s : Type (u + 1))
hs : s.Nonempty
⊢ o + sSup s = sSup ((fun (x : Ordinal.{u}) ↦ o + x) '' s)

Tactic:
(isNormal_add_right o).map_sSup hs bddAbove_of_small

Premises used: Ordinal.bddAbove_of_small, Ordinal.isNormal_add_right, Order.IsNormal.map_sSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
inl : o * sSup ∅ = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' ∅)
inr : ∀ (hs : s.Nonempty), o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
⊢ o * sSup ∅ = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' ∅)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
inr : 0 * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ 0 * x) '' s)
inr₁ : ∀ (ho : 0 < o), o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)

Tactic:
rcases eq_zero_or_pos o with (rfl | ho)

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_1}
hs : s.Nonempty
⊢ 0 * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ 0 * x) '' s)

Tactic:
simp [hs.image_const]

Premises used: Set.Nonempty.image_const
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
pos : ∀ (bdd : BddAbove s), o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
neg : ∀ (bdd : ¬BddAbove s), o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)

Tactic:
by_cases bdd : BddAbove s

Premises used: BddAbove
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : BddAbove s
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)

Tactic:
(isNormal_mul_right ho).map_sSup hs bdd

Premises used: Ordinal.isNormal_mul_right, Order.IsNormal.map_sSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : BddAbove s
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)

Tactic:
exact (isNormal_mul_right ho).map_sSup hs bdd

Premises used: Ordinal.isNormal_mul_right, Order.IsNormal.map_sSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
neg : o * ⊥ = sSup ∅
neg₁ : ¬BddAbove (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)

Tactic:
rw [csSup_of_not_bddAbove bdd, csSup_empty, csSup_of_not_bddAbove]

Premises used: csSup_empty, csSup_of_not_bddAbove
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * ⊥ = sSup ∅

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ ¬BddAbove (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)

Tactic:
fun ⟨u, hu⟩ ↦ bdd ⟨u, fun x hx ↦ (x.le_mul_right ho).trans (hu ⟨x, hx, rfl⟩)⟩

Premises used: False, Ordinal.le_mul_right, And.intro, Exists.intro, _private.0.Ordinal.mul_sSup.match_1, LE.le.trans, Not, rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ ¬BddAbove (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)

Tactic:
exact fun ⟨u, hu⟩ ↦ bdd ⟨u, fun x hx ↦ (x.le_mul_right ho).trans (hu ⟨x, hx, rfl⟩)⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
rw : o * sSup (range fun (i : ι) ↦ f i) = ⨆ (i : ι), o * f i
rw₁ :
  Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' range fun (i : ι) ↦ f i))
    (⨆ (i : ι), o * f i)
rw₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup (range fun (x : ι) ↦ o * f x)) (⨆ (i : ι), o * f i)
rw₃ rw₄ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (x : ι), o * f x) (⨆ (i : ι), o * f i)
⊢ o * ⨆ (i : ι), f i = ⨆ (i : ι), o * f i

Tactic:
rw [← sSup_range, mul_sSup, ← Set.range_comp', sSup_range]

Premises used: Ordinal.mul_sSup, sSup_range, Set.range_comp'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
rw : ⨆ (n : ℕ), o + (↑n : Ordinal.{u_1}) = o + iSup Nat.cast
rw₁ rw₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (n : ℕ), o + (↑n : Ordinal.{u_1})) (⨆ (i : ℕ), o + (↑i : Ordinal.{u_1}))
⊢ ⨆ (n : ℕ), o + (↑n : Ordinal.{u_1}) = o + ω

Tactic:
rw [← iSup_natCast, Ordinal.add_iSup]

Premises used: Ordinal.add_iSup, Ordinal.iSup_natCast
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_1}
rw : ⨆ (n : ℕ), o * (↑n : Ordinal.{u_1}) = o * iSup Nat.cast
rw₁ rw₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (n : ℕ), o * (↑n : Ordinal.{u_1})) (⨆ (i : ℕ), o * (↑i : Ordinal.{u_1}))
⊢ ⨆ (n : ℕ), o * (↑n : Ordinal.{u_1}) = o * ω

Tactic:
rw [← iSup_natCast, Ordinal.mul_iSup]

Premises used: Ordinal.mul_iSup, Ordinal.iSup_natCast
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ nfpFamily f a

Tactic:
Ordinal.le_iSup _ _

Premises used: Ordinal.nfpFamily, Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
inst : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ a ≤ nfpFamily f a

Tactic:
foldr_le_nfpFamily f a []

Premises used: Ordinal.foldr_le_nfpFamily, List.foldr, List.nil
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
a b : Ordinal.{u}
⊢ a < nfpFamily f b ↔ ∃ (l : List ι), a < List.foldr f b l

Tactic:
Ordinal.lt_iSup_iff

Premises used: Ordinal.nfpFamily, Ordinal.lt_iSup_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
a b : Ordinal.{u}
⊢ nfpFamily f a ≤ b ↔ ∀ (l : List ι), List.foldr f a l ≤ b

Tactic:
Ordinal.iSup_le_iff

Premises used: Ordinal.nfpFamily, Ordinal.iSup_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ (∀ (l : List ι), List.foldr f a l ≤ b) → nfpFamily f a ≤ b

Tactic:
Ordinal.iSup_le

Premises used: Ordinal.nfpFamily, Ordinal.iSup_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
hf : ∀ (i : ι), Monotone (f i)
⊢ Monotone (nfpFamily f)

Tactic:
fun _ _ h ↦ nfpFamily_le <| fun l ↦ (List.foldr_monotone hf l h).trans (foldr_le_nfpFamily _ _ l)

Premises used: Monotone, Ordinal.foldr_le_nfpFamily, List.foldr_monotone, LE.le.trans, Ordinal.nfpFamily_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 b : Ordinal.{u}
hb : b < nfpFamily f a
i : ι
⊢ f i b < nfpFamily f a

Tactic:
let ⟨l, hl⟩ := lt_nfpFamily_iff.1 hb
  lt_nfpFamily_iff.2 ⟨i::l, (H i).strictMono hl⟩

Premises used: Iff.mpr, Ordinal.nfpFamily, Ordinal.lt_nfpFamily_iff, List.cons, LT.lt, Exists.intro, Iff.mp, Order.IsNormal.strictMono, _private.0.Ordinal.apply_lt_nfpFamily.match_1
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Nonempty ι
inst_1 : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a

Tactic:
⟨fun h ↦ ?_, apply_lt_nfpFamily H⟩

Premises used: Iff.intro, Ordinal.apply_lt_nfpFamily
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Nonempty ι
inst_1 : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
refine : ∀ (h : ∀ (i : ι), f i b < nfpFamily f a), b < nfpFamily f a
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a

Tactic:
refine ⟨fun h ↦ ?_, apply_lt_nfpFamily H⟩
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Nonempty ι
inst_1 : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b < nfpFamily f a
let : ∀ (l : List ι) (hl : f (Classical.arbitrary ι) b < List.foldr f a l), b < nfpFamily f a
⊢ b < nfpFamily f a

Tactic:
let ⟨l, hl⟩ := lt_nfpFamily_iff.1 (h (Classical.arbitrary ι))
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Nonempty ι
inst_1 : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b < nfpFamily f a
l : List ι
hl : f (Classical.arbitrary ι) b < List.foldr f a l
⊢ b < nfpFamily f a

Tactic:
lt_nfpFamily_iff.2 <| ⟨l, (H _).strictMono.le_apply.trans_lt hl⟩

Premises used: StrictMono.le_apply, Iff.mpr, Ordinal.lt_nfpFamily_iff, Exists.intro, Order.IsNormal.strictMono, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Nonempty ι
inst_1 : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b < nfpFamily f a
l : List ι
hl : f (Classical.arbitrary ι) b < List.foldr f a l
⊢ b < nfpFamily f a

Tactic:
exact lt_nfpFamily_iff.2 <| ⟨l, (H _).strictMono.le_apply.trans_lt hl⟩

Premises used: Iff.mpr, Ordinal.lt_nfpFamily_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Nonempty ι
inst_1 : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
contrapose! : (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a
⊢ (∃ (i : ι), nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b

Tactic:
contrapose!
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Nonempty ι
inst_1 : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a

Tactic:
apply_lt_nfpFamily_iff H

Premises used: Ordinal.apply_lt_nfpFamily_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Nonempty ι
inst_1 : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a

Tactic:
exact apply_lt_nfpFamily_iff H

Premises used: Ordinal.apply_lt_nfpFamily_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{u}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
apply : ∀ (l : List ι), List.foldr f a l ≤ b
⊢ nfpFamily f a ≤ b

Tactic:
apply Ordinal.iSup_le fun l ↦ ?_

Premises used: Ordinal.iSup_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ b
a : Ordinal.{u}
ab : a ≤ b
⊢ List.foldr f a [] ≤ b

Tactic:
ab

Premises used: List.foldr
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ b
a : Ordinal.{u}
ab : a ≤ b
⊢ List.foldr f a [] ≤ b

Tactic:
exact ab
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ b
i : ι
l : List ι
IH : ∀ {a : Ordinal.{u}} (ab : a ≤ b), List.foldr f a l ≤ b
a : Ordinal.{u}
ab : a ≤ b
⊢ List.foldr f a (i :: l) ≤ b

Tactic:
(H i (IH ab)).trans (h i)

Premises used: LE.le.trans, List.foldr
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ b
i : ι
l : List ι
IH : ∀ {a : Ordinal.{u}} (ab : a ≤ b), List.foldr f a l ≤ b
a : Ordinal.{u}
ab : a ≤ b
⊢ List.foldr f a (i :: l) ≤ b

Tactic:
exact (H i (IH ab)).trans (h i)

Premises used: LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{u}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
l : List ι
nil : ∀ {a : Ordinal.{u}} (ab : a ≤ b), List.foldr f a [] ≤ b
cons :
  ∀ (i : ι) (l : List ι) (IH : ∀ {a : Ordinal.{u}} (ab : a ≤ b), List.foldr f a l ≤ b) {a : Ordinal.{u}} (ab : a ≤ b),
    List.foldr f a (i :: l) ≤ b
⊢ List.foldr f a l ≤ b

Tactic:
induction l generalizing a with
  | nil => exact ab
  | cons i l IH => exact (H i (IH ab)).trans (h i)
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
rw : Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i_1 : List ι), f i (List.foldr f a i_1)) (⨆ (i : List ι), List.foldr f a i)
⊢ f i (nfpFamily f a) = nfpFamily f a

Tactic:
rw [nfpFamily, H.map_iSup bddAbove_of_small]

Premises used: Ordinal.nfpFamily, Ordinal.bddAbove_of_small, 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)
a : Ordinal.{u}
a₁ : LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i_1 : List ι), f i (List.foldr f a i_1)) (⨆ (i : List ι), List.foldr f a i)
a₂ : LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : List ι), List.foldr f a i) (⨆ (i_1 : List ι), f i (List.foldr f a i_1))
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i_1 : List ι), f i (List.foldr f a i_1)) (⨆ (i : List ι), List.foldr f a i)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i_1 : List ι), f i (List.foldr f a i_1)) (⨆ (i : List ι), List.foldr f a i)

Tactic:
Ordinal.iSup_le fun l => ?_

Premises used: Ordinal.iSup_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
a₁ : ∀ (l : List ι), f i (List.foldr f a l) ≤ ⨆ (i : List ι), List.foldr f a i
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i_1 : List ι), f i (List.foldr f a i_1)) (⨆ (i : List ι), List.foldr f a i)

Tactic:
refine Ordinal.iSup_le fun l => ?_

Premises used: Ordinal.iSup_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : List ι), List.foldr f a i) (⨆ (i_1 : List ι), f i (List.foldr f a i_1))

Tactic:
Ordinal.iSup_le fun l => ?_

Premises used: Ordinal.iSup_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
a₁ : ∀ (l : List ι), List.foldr f a l ≤ ⨆ (i_1 : List ι), f i (List.foldr f a i_1)
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : List ι), List.foldr f a i) (⨆ (i_1 : List ι), f i (List.foldr f a i_1))

Tactic:
refine Ordinal.iSup_le fun l => ?_

Premises used: Ordinal.iSup_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ f i (List.foldr f a l) ≤ ⨆ (i : List ι), List.foldr f a i

Tactic:
Ordinal.le_iSup _ (i::l)

Premises used: List.cons, Ordinal.le_iSup, List.foldr
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ f i (List.foldr f a l) ≤ ⨆ (i : List ι), List.foldr f a i

Tactic:
exact Ordinal.le_iSup _ (i::l)

Premises used: List.cons, Ordinal.le_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)
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ ⨆ (i_1 : List ι), f i (List.foldr f a i_1)

Tactic:
H.strictMono.le_apply.trans (Ordinal.le_iSup _ _)

Premises used: StrictMono.le_apply, Ordinal.le_iSup, LE.le.trans, 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)
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ ⨆ (i_1 : List ι), f i (List.foldr f a i_1)

Tactic:
exact H.strictMono.le_apply.trans (Ordinal.le_iSup _ _)
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
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}
⊢ (∀ (i : ι), f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a

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

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
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}
refine_1 : ∀ (h : ∀ (i : ι), f i b ≤ nfpFamily f a), b ≤ nfpFamily f a
refine_2 : ∀ (h : b ≤ nfpFamily f a) (i : ι), f i b ≤ nfpFamily f a
⊢ (∀ (i : ι), f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a

Tactic:
refine ⟨fun h => ?_, fun h i => ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
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 : ∀ (i : ι), f i b ≤ nfpFamily f a
refine_1 : ∀ (i : ι), b ≤ nfpFamily f a
⊢ b ≤ nfpFamily f a

Tactic:
obtain ⟨i⟩ := 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 b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
i : ι
⊢ b ≤ nfpFamily f a

Tactic:
(H i).strictMono.le_apply.trans (h i)

Premises used: StrictMono.le_apply, LE.le.trans, 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 b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
i : ι
⊢ b ≤ nfpFamily f a

Tactic:
exact (H i).strictMono.le_apply.trans (h i)

Premises used: StrictMono.le_apply, LE.le.trans, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
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 : ι
refine_2 : f i b ≤ f i (nfpFamily f a)
⊢ f i b ≤ nfpFamily f a

Tactic:
rw [← nfpFamily_fp (H i)]

Premises used: Ordinal.nfpFamily_fp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
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 ≤ f i (nfpFamily f a)

Tactic:
(H i).monotone h

Premises used: Order.IsNormal.monotone
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
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 ≤ f i (nfpFamily f a)

Tactic:
exact (H i).monotone h

Premises used: Order.IsNormal.monotone
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
apply : ∀ (i : List ι), List.foldr f a i ≤ a
⊢ nfpFamily f a = a

Tactic:
apply (Ordinal.iSup_le ?_).antisymm (le_nfpFamily f a)

Premises used: Ordinal.iSup_le, LE.le.antisymm, Ordinal.le_nfpFamily
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
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 ι
rw rw₁ : a ≤ a
⊢ List.foldr f a l ≤ a

Tactic:
rw [List.foldr_fixed' h l]

Premises used: List.foldr_fixed'
-- 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 :
  ∀ (x : Ordinal.{u}),
    ∃ (y : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) y ∧ x < y
⊢ ¬BddAbove.{u + 1} (α := Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i))

Tactic:
rw [not_bddAbove_iff]

Premises used: not_bddAbove_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)
⊢ ∀ (x : Ordinal.{u}),
    ∃ (y : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) y ∧ x < y

Tactic:
fun a ↦ ⟨nfpFamily f (succ a), ?_, (lt_succ a).trans_le (le_nfpFamily f _)⟩

Premises used: Ordinal.nfpFamily, Order.succ, Order.lt_succ, LT.lt.trans_le, And.intro, Exists.intro, Ordinal.le_nfpFamily
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
refine :
  ∀ (a : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) (nfpFamily f (succ a))
⊢ ∀ (x : Ordinal.{u}),
    ∃ (y : Ordinal.{u}), Membership.mem (γ := Set Ordinal.{u}) (⋂ (i : ι), fixedPoints (f i)) y ∧ x < y

Tactic:
refine fun a ↦ ⟨nfpFamily f (succ a), ?_, (lt_succ a).trans_le (le_nfpFamily f _)⟩
-- 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 : ι
⊢ Membership.mem (γ := Set Ordinal.{u}) ((fun (i : ι) ↦ fixedPoints (f i)) i) (nfpFamily f (succ a))

Tactic:
nfpFamily_fp (H i) _

Premises used: Set.Mem, setOf, Function.fixedPoints, Function.IsFixedPt, 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}
i : ι
⊢ Membership.mem (γ := Set Ordinal.{u}) ((fun (i : ι) ↦ fixedPoints (f i)) i) (nfpFamily f (succ a))

Tactic:
exact nfpFamily_fp (H i) _

Premises used: Ordinal.nfpFamily_fp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u_2} → Ordinal.{u_2}
⊢ derivFamily f 0 = nfpFamily f 0

Tactic:
limitRecOn_zero ..

Premises used: Ordinal.limitRecOn_zero, Ordinal.derivFamily
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u_2} → Ordinal.{u_2}
o : Ordinal.{u_2}
⊢ derivFamily f (o + 1) = nfpFamily f (derivFamily f o + 1)

Tactic:
limitRecOn_add_one ..

Premises used: Order.succ, Ordinal.limitRecOn_add_one, Ordinal.derivFamily
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u_2} → Ordinal.{u_2}
o : Ordinal.{u_2}
⊢ derivFamily f (succ o) = nfpFamily f (succ (derivFamily f o))

Tactic:
derivFamily_add_one f o

Premises used: Order.succ, Ordinal.derivFamily_add_one
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
ι : Type u_1
f : ι → Ordinal.{u_2} → Ordinal.{u_2}
o : Ordinal.{u_2}
⊢ IsSuccLimit o → derivFamily f o = ⨆ (b : (↑(Set.Iio o) : Type (u_2 + 1))), derivFamily f (↑b : Ordinal.{u_2})

Tactic:
limitRecOn_limit _ _ _ _

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

Tactic:
IsNormal.of_succ_lt (fun o ↦ ?_) @fun o h ↦ ?_

Premises used: Order.IsNormal.of_succ_lt
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
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)
refine_2 : ∀ (o : Ordinal.{u}) (h : IsSuccLimit o), IsLUB (derivFamily f '' Set.Iio o) (derivFamily f o)
⊢ IsNormal (derivFamily f)

Tactic:
refine IsNormal.of_succ_lt (fun o ↦ ?_) @fun o h ↦ ?_

Premises used: Order.IsNormal.of_succ_lt