awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
h_1 :
  Membership.mem (γ := Set Ordinal.{max (max u v) w}) (o.brange fun (a : Ordinal.{u}) (ha : a < o) ↦ succ (f a ha)) a
b : Ordinal.{u}
hb : b < o
hb' : (fun (a : Ordinal.{u}) (ha : a < o) ↦ succ (f a ha)) b hb = a
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
⊢ Membership.mem (γ := Set Ordinal.{max (max u v) w}) (o'.brange fun (a : Ordinal.{v}) (ha : a < o') ↦ succ (g a ha)) a
have hb'₁ : succ (g c hc) = a
Tactic: simp_rw [← hc'] at hb'
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_1
β : Type u_2
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o
have rw : g a ha < o'.blsub g
Tactic: rw [← hg]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
⊢ (o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯) = o.bsup f
have a : (o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) sorry) ≤ o.bsup f
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
a : (o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯) ≤ o.bsup f
⊢ (o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯) = o.bsup f
have a₁ : o.bsup f ≤ o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) sorry
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
⊢ (o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯) ≤ o.bsup f
have a : ∀ (i : Ordinal.{max u v}) (hi : i < o'), f (g i hi) sorry ≤ o.bsup f
Tactic: refine bsup_le fun i hi => ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
⊢ o.bsup f ≤ o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯
have a : ∀ (i : Ordinal.{max u v}) (hi : i < o), f i hi ≤ o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) sorry
Tactic: refine bsup_le fun i hi => ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o
⊢ f i hi ≤ o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯
have hi₁ : ∃ (i_1 : Ordinal.{max u v}) (hi : i_1 < o'), i ≤ g i_1 hi
Tactic: rw [← hg, lt_blsub_iff] at hi
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi_1 : i < o
hi : ∃ (i_1 : Ordinal.{max u v}) (hi : i_1 < o'), i ≤ g i_1 hi
⊢ f i hi_1 ≤ o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯
have a : ∀ (j : Ordinal.{max u v}) (hj : j < o') (hj' : i ≤ g j hj),
  f i hi_1 ≤ o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) sorry
Tactic: rcases hi with ⟨j, hj, hj'⟩
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (Ordinal.bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
have rw : f (o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) ↦ x) = f o
Tactic: rw [← IsNormal.bsup.{u, u, v} H (fun x _ => x) h.ne_bot, bsup_id_limit fun _ ↦ h.succ_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
rw : f (o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) ↦ x) = f o
⊢ (Ordinal.bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
have rw₁ : f o = f o
Tactic: rw [← IsNormal.bsup.{u, u, v} H (fun x _ => x) h.ne_bot, bsup_id_limit fun _ ↦ h.succ_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
have rw : ∀ (a : Ordinal.{u}) (ha : a < o), f a < f (succ a)
Tactic: rw [← IsNormal.bsup_eq.{u, v} H h, bsup_eq_blsub_of_lt_succ_limit h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
h :
  (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)
h₂ : ∀ (o : Ordinal.{u}), IsSuccLimit o → (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
a : Ordinal.{u}
ho : IsSuccLimit a
⊢ IsLUB (f '' Iio a) (f a)
have rw : IsLUB (f '' Iio a) (bsup.{u, v} a fun (x : Ordinal.{u}) (x_1 : x < a) ↦ f x)
Tactic: rw [← h₂ _ ho]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
⊢ IsNormal f ↔
    (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧
      ∀ (o : Ordinal.{u}), IsSuccLimit o → (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
have rw : (∀ (a : Ordinal.{u}), f a < f (succ a)) →
  ((∀ (o : Ordinal.{u}), IsSuccLimit o → (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o) ↔
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o)
Tactic: rw [isNormal_iff_lt_succ_and_bsup_eq.{u, v}, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o) ↔
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
have mp : (∀ (o : Ordinal.{u}), IsSuccLimit o → (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o) →
  ∀ (o : Ordinal.{u}), IsSuccLimit o → (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
mp :
  (∀ (o : Ordinal.{u}), IsSuccLimit o → (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o) →
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o) ↔
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
have mpr : (∀ (o : Ordinal.{u}), IsSuccLimit o → (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o) →
  ∀ (o : Ordinal.{u}), IsSuccLimit o → (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
have this : (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
Tactic: have := H o ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
have this : (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
Tactic: have := H o ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
⊢ (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
have mpr : ∀ (this : (bsup.{u, v} o fun (a : Ordinal.{u}) (x : a < o) ↦ f a) = f o),
  (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
Tactic: rwa [← bsup_eq_blsub_of_lt_succ_limit ho fun a _ => h a] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
⊢ False
have obtain : ∀ (a : α) (ha : f a = ⨆ (i : α), succ (f i)), False
Tactic: obtain ⟨a, ha⟩ := h (⨆ i, succ (f i))
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
a : α
ha : f a = ⨆ (i : α), succ (f i)
⊢ False
have apply : f a < ⨆ (i : α), succ (f i)
Tactic: apply ha.not_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
a : α
ha : f a = ⨆ (i : α), succ (f i)
⊢ f a < ⨆ (i : α), succ (f i)
have rw : ∃ (i : α), f a < succ (f i)
Tactic: rw [Ordinal.lt_iSup_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
⊢ ¬BddAbove sᶜ
have rw : ¬Small.{u, u + 1} (↑sᶜ : Type (u + 1))
Tactic: rw [bddAbove_iff_small]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
h : Small.{u, u + 1} (↑sᶜ : Type (u + 1))
⊢ False
have this : Small.{u, u + 1} (↑(s ∪ sᶜ) : Type (u + 1))
Tactic: have := small_union s sᶜ
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
h : Small.{u, u + 1} (↑sᶜ : Type (u + 1))
this : Small.{u, u + 1} (↑(s ∪ sᶜ) : Type (u + 1))
⊢ False
have this₁ : Small.{u, u + 1} Ordinal.{u}
Tactic: rw [union_compl_self, small_univ_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{u} → Ordinal.{v}
hf : IsNormal f
⊢ ⨆ (n : ℕ), f (↑n : Ordinal.{u}) = f ω
have rw : ⨆ (n : ℕ), f (↑n : Ordinal.{u}) = f (iSup Nat.cast)
Tactic: rw [← iSup_natCast, hf.map_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{u} → Ordinal.{v}
hf : IsNormal f
rw : ⨆ (n : ℕ), f (↑n : Ordinal.{u}) = f (iSup Nat.cast)
⊢ ⨆ (n : ℕ), f (↑n : Ordinal.{u}) = f ω
have rw₁ : Eq.{v + 2} (α := Ordinal.{v}) (⨆ (n : ℕ), f (↑n : Ordinal.{u})) (⨆ (i : ℕ), f (↑i : Ordinal.{u}))
Tactic: rw [← iSup_natCast, hf.map_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
have inl : o * sSup ∅ = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' ∅)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
inl : o * sSup ∅ = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' ∅)
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
have inr : ∀ (hs : s.Nonempty), o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
have inr : 0 * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ 0 * x) '' s)
Tactic: rcases eq_zero_or_pos o with (rfl | ho)
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
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)
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
have inr₁ : ∀ (ho : 0 < o), o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
Tactic: rcases eq_zero_or_pos o with (rfl | ho)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
have pos : ∀ (bdd : BddAbove s), o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
Tactic: by_cases bdd : BddAbove s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
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)
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
have neg : ∀ (bdd : ¬BddAbove s), o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
Tactic: by_cases bdd : BddAbove s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
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)
have neg : o * ⊥ = sSup ∅
Tactic: rw [csSup_of_not_bddAbove bdd, csSup_empty, csSup_of_not_bddAbove]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
neg : o * ⊥ = sSup ∅
⊢ o * sSup s = sSup ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
have neg₁ : ¬BddAbove (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ o * x) '' s)
Tactic: rw [csSup_of_not_bddAbove bdd, csSup_empty, csSup_of_not_bddAbove]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ o * ⨆ (i : ι), f i = ⨆ (i : ι), o * f i
have rw : o * sSup (range fun (i : ι) ↦ f i) = ⨆ (i : ι), o * f i
Tactic: rw [← sSup_range, mul_sSup, ← Set.range_comp', sSup_range]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
rw : o * sSup (range fun (i : ι) ↦ f i) = ⨆ (i : ι), o * f i
⊢ o * ⨆ (i : ι), f i = ⨆ (i : ι), o * f i
have 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)
Tactic: rw [← sSup_range, mul_sSup, ← Set.range_comp', sSup_range]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
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)
⊢ o * ⨆ (i : ι), f i = ⨆ (i : ι), o * f i
have rw₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup (range fun (x : ι) ↦ o * f x)) (⨆ (i : ι), o * f i)
Tactic: rw [← sSup_range, mul_sSup, ← Set.range_comp', sSup_range]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
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)
⊢ o * ⨆ (i : ι), f i = ⨆ (i : ι), o * f i
have rw₃ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (x : ι), o * f x) (⨆ (i : ι), o * f i)
Tactic: rw [← sSup_range, mul_sSup, ← Set.range_comp', sSup_range]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_1}
⊢ ⨆ (n : ℕ), o + (↑n : Ordinal.{u_1}) = o + ω
have rw : ⨆ (n : ℕ), o + (↑n : Ordinal.{u_1}) = o + iSup Nat.cast
Tactic: rw [← iSup_natCast, Ordinal.add_iSup]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_1}
rw : ⨆ (n : ℕ), o + (↑n : Ordinal.{u_1}) = o + iSup Nat.cast
⊢ ⨆ (n : ℕ), o + (↑n : Ordinal.{u_1}) = o + ω
have rw₁ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (n : ℕ), o + (↑n : Ordinal.{u_1})) (⨆ (i : ℕ), o + (↑i : Ordinal.{u_1}))
Tactic: rw [← iSup_natCast, Ordinal.add_iSup]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_1}
⊢ ⨆ (n : ℕ), o * (↑n : Ordinal.{u_1}) = o * ω
have rw : ⨆ (n : ℕ), o * (↑n : Ordinal.{u_1}) = o * iSup Nat.cast
Tactic: rw [← iSup_natCast, Ordinal.mul_iSup]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_1}
rw : ⨆ (n : ℕ), o * (↑n : Ordinal.{u_1}) = o * iSup Nat.cast
⊢ ⨆ (n : ℕ), o * (↑n : Ordinal.{u_1}) = o * ω
have rw₁ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (n : ℕ), o * (↑n : Ordinal.{u_1})) (⨆ (i : ℕ), o * (↑i : Ordinal.{u_1}))
Tactic: rw [← iSup_natCast, Ordinal.mul_iSup]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
have refine : ∀ (h : ∀ (i : ι), f i b < nfpFamily f a), b < nfpFamily f a
Tactic: refine ⟨fun h ↦ ?_, apply_lt_nfpFamily H⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ b < nfpFamily f a
have let : ∀ (l : List ι) (hl : f (Classical.arbitrary ι) b < List.foldr f a l), b < nfpFamily f a
Tactic: let ⟨l, hl⟩ := lt_nfpFamily_iff.1 (h (Classical.arbitrary ι))
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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 : ι), nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b
have contrapose! : (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ nfpFamily f a ≤ b
have apply : ∀ (l : List ι), List.foldr f a l ≤ b
Tactic: apply Ordinal.iSup_le fun l ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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 ι
⊢ List.foldr f a l ≤ b
have nil : ∀ {a : Ordinal.{u}} (ab : a ≤ b), List.foldr f a [] ≤ b
Tactic: induction l generalizing a with
  | nil => exact ab
  | cons i l IH => exact (H i (IH ab)).trans (h i)
Cleared hypotheses: a, ab, l
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ List.foldr f a l ≤ b
have 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
Tactic: induction l generalizing a with
  | nil => exact ab
  | cons i l IH => exact (H i (IH ab)).trans (h i)
Cleared hypotheses: a, ab, 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} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ f i (nfpFamily f a) = nfpFamily f a
have rw : Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i_1 : List ι), f i (List.foldr f a i_1)) (⨆ (i : List ι), List.foldr f a i)
Tactic: rw [nfpFamily, 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)
a : Ordinal.{u}
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i_1 : List ι), f i (List.foldr f a i_1)) (⨆ (i : List ι), List.foldr f a i)
have 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)
Tactic: apply le_antisymm
-- 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)
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)
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i_1 : List ι), f i (List.foldr f a i_1)) (⨆ (i : List ι), List.foldr f a i)
have 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))
Tactic: apply le_antisymm
-- 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)
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)
have a₁ : ∀ (l : List ι), f i (List.foldr f a l) ≤ ⨆ (i : List ι), List.foldr f a i
Tactic: refine Ordinal.iSup_le fun 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} ι
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))
have a₁ : ∀ (l : List ι), List.foldr f a l ≤ ⨆ (i_1 : List ι), f i (List.foldr f a i_1)
Tactic: refine Ordinal.iSup_le fun 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ι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a
have refine_1 : ∀ (h : ∀ (i : ι), f i b ≤ nfpFamily f a), b ≤ nfpFamily f a
Tactic: refine ⟨fun h => ?_, fun 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} ι
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
⊢ (∀ (i : ι), f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a
have refine_2 : ∀ (h : b ≤ nfpFamily f a) (i : ι), f i b ≤ nfpFamily f a
Tactic: refine ⟨fun h => ?_, fun 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} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
⊢ b ≤ nfpFamily f a
have refine_1 : ∀ (i : ι), b ≤ nfpFamily f a
Tactic: obtain ⟨i⟩ := hι
Cleared hypotheses: hι