awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst : Small.{u, u_3} α
inst_1 : Small.{u, u_4} β
apply : ∀ (i : α ⊕ β), f i ≤ max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))
⊢ iSup f = max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))
have apply₁ : LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (a : α), f (Sum.inl a)) (⨆ (i : α ⊕ β), f i)
Tactic: apply (Ordinal.iSup_le _).antisymm (max_le _ _)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst : Small.{u, u_3} α
inst_1 : Small.{u, u_4} β
apply : ∀ (i : α ⊕ β), f i ≤ max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))
apply₁ : LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (a : α), f (Sum.inl a)) (⨆ (i : α ⊕ β), f i)
⊢ iSup f = max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))
have apply₂ : LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (b : β), f (Sum.inr b)) (⨆ (i : α ⊕ β), f i)
Tactic: apply (Ordinal.iSup_le _).antisymm (max_le _ _)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst : Small.{u, u_3} α
inst_1 : Small.{u, u_4} β
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (a : α), f (Sum.inl a)) (⨆ (i : α ⊕ β), f i)
have apply : Subset.{u + 1} (α := Set Ordinal.{u}) (range fun (a : α) ↦ f (Sum.inl a)) (range fun (i : α ⊕ β) ↦ f i)
Tactic: apply csSup_le_csSup' bddAbove_of_small
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst : Small.{u, u_3} α
inst_1 : Small.{u, u_4} β
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (b : β), f (Sum.inr b)) (⨆ (i : α ⊕ β), f i)
have apply : Subset.{u + 1} (α := Set Ordinal.{u}) (range fun (b : β) ↦ f (Sum.inr b)) (range fun (i : α ⊕ β) ↦ f i)
Tactic: apply csSup_le_csSup' bddAbove_of_small
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Cardinal.{u_3}
⊢ (sSup s).ord = sSup (ord '' s)
have inl : ord (sSup ∅) = sSup (ord '' ∅)
Tactic: obtain rfl | hn := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Cardinal.{u_3}
inl : ord (sSup ∅) = sSup (ord '' ∅)
⊢ (sSup s).ord = sSup (ord '' s)
have inr : ∀ (hn : s.Nonempty), (sSup s).ord = sSup (ord '' s)
Tactic: obtain rfl | hn := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Cardinal.{u_3}
hn : s.Nonempty
⊢ (sSup s).ord = sSup (ord '' s)
have pos : ∀ (hs : BddAbove s), (sSup s).ord = sSup (ord '' s)
Tactic: by_cases hs : BddAbove s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Cardinal.{u_3}
hn : s.Nonempty
pos : ∀ (hs : BddAbove s), (sSup s).ord = sSup (ord '' s)
⊢ (sSup s).ord = sSup (ord '' s)
have neg : ∀ (hs : ¬BddAbove s), (sSup s).ord = sSup (ord '' s)
Tactic: by_cases hs : BddAbove s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : ¬BddAbove s
⊢ (sSup s).ord = sSup (ord '' s)
have neg : ord (sSup ∅) = sSup ∅
Tactic: rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (bddAbove_ord_image_iff.not.2 hs)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Sort u_3
f : ι → Cardinal.{u_4}
⊢ ord (⨆ (i : ι), f i) = ⨆ (i : ι), (f i).ord
have rw : ord (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), (f i).ord
Tactic: rw [iSup, iSup, sSup_ord, range_comp']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Sort u_3
f : ι → Cardinal.{u_4}
rw : ord (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), (f i).ord
⊢ ord (⨆ (i : ι), f i) = ⨆ (i : ι), (f i).ord
have rw₁ : ord (sSup (range fun (i : ι) ↦ f i)) = sSup (range fun (i : ι) ↦ (f i).ord)
Tactic: rw [iSup, iSup, sSup_ord, range_comp']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Sort u_3
f : ι → Cardinal.{u_4}
rw : ord (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), (f i).ord
rw₁ : ord (sSup (range fun (i : ι) ↦ f i)) = sSup (range fun (i : ι) ↦ (f i).ord)
⊢ ord (⨆ (i : ι), f i) = ⨆ (i : ι), (f i).ord
have rw₂ : sSup (ord '' range fun (i : ι) ↦ f i) = sSup (range fun (i : ι) ↦ (f i).ord)
Tactic: rw [iSup, iSup, sSup_ord, range_comp']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Sort u_3
f : ι → Cardinal.{u_4}
rw : ord (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), (f i).ord
rw₁ : ord (sSup (range fun (i : ι) ↦ f i)) = sSup (range fun (i : ι) ↦ (f i).ord)
rw₂ : sSup (ord '' range fun (i : ι) ↦ f i) = sSup (range fun (i : ι) ↦ (f i).ord)
⊢ ord (⨆ (i : ι), f i) = ⨆ (i : ι), (f i).ord
have rw₃ : sSup (ord '' range fun (i : ι) ↦ f i) = sSup (ord '' range f)
Tactic: rw [iSup, iSup, sSup_ord, range_comp']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u}
⊢ Cardinal.lift.{u + 1, u} (sInf sᶜ).card ≤ #(↑s : Type (u + 1))
have rw : #(↑(Iio (sInf sᶜ)) : Type (u + 1)) ≤ #(↑s : Type (u + 1))
Tactic: rw [← Cardinal.mk_Iio_ordinal]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u}
⊢ #(↑(Iio (sInf sᶜ)) : Type (u + 1)) ≤ #(↑s : Type (u + 1))
have refine : ∀ (x : Ordinal.{u}) (hx : x < sInf sᶜ), x ∈ s
Tactic: refine mk_le_mk_of_subset fun x (hx : x < _) ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ x ∈ s
have rw : ¬x ∉ s
Tactic: rw [← not_notMem]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι
have rw : Cardinal.lift.{(max u v) + 1, max u v} (sInf (range f)ᶜ).card ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι
Tactic: rw [← Cardinal.lift_le.{max u v + 1}, Cardinal.lift_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ Cardinal.lift.{(max u v) + 1, max u v} (sInf (range f)ᶜ).card ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι
have apply : #(↑(range f) : Type ((max u v) + 1)) ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι
Tactic: apply (lift_card_sInf_compl_le _).trans
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ #(↑(range f) : Type ((max u v) + 1)) ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι
have rw : Cardinal.lift.{u, max u ((max u v) + 1)} #(↑(range f) : Type (max (u + 1) (v + 1))) ≤
  Cardinal.lift.{max v (u + 1) (v + 1), u} #ι
Tactic: rw [← Cardinal.lift_id'.{u, max u v + 1} #(range _)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ sInf (range f)ᶜ < lift.{v, u} (succ #ι).ord
have rw : (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι
Tactic: rw [lift_ord, Cardinal.lift_succ, ← card_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u_3}
⊢ BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s) ↔ BddAbove s
have mp : BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s) → BddAbove s
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u_3}
mp : BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s) → BddAbove s
⊢ BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s) ↔ BddAbove s
have mpr : BddAbove s → BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds s
⊢ BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
have h : Membership.mem (γ := Set Ordinal.{u_3}) (upperBounds ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)) (a + 1)
Tactic: use a + 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_2
f : β → Ordinal.{u}
⊢ BddAbove.{u + 1} (α := Ordinal.{u}) (range fun (i : β) ↦ f i + 1) ↔ BddAbove (range f)
have rw : BddAbove (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ x + 1) '' range f) ↔ BddAbove (range f)
Tactic: rw [range_comp' (· + 1), bddAbove_add_one_image_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_2
f : β → Ordinal.{u}
rw : BddAbove (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ x + 1) '' range f) ↔ BddAbove (range f)
⊢ BddAbove.{u + 1} (α := Ordinal.{u}) (range fun (i : β) ↦ f i + 1) ↔ BddAbove (range f)
have rw₁ : BddAbove (range f) ↔ BddAbove (range f)
Tactic: rw [range_comp' (· + 1), bddAbove_add_one_image_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u_3}
⊢ sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
have pos : ∀ (hs : BddAbove s), sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
Tactic: by_cases hs : BddAbove s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u_3}
pos : ∀ (hs : BddAbove s), sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
⊢ sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
have neg : ∀ (hs : ¬BddAbove s), sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
Tactic: by_cases hs : BddAbove s
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
s : Set Ordinal.{u_3}
hs : BddAbove s
⊢ sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
have hs' : BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
Tactic: have hs' := bddAbove_add_one_image_iff.2 hs
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u_3}
hs : BddAbove s
hs' : BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
⊢ sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
have pos : ∀ x ∈ s, x ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
Tactic: rw [csSup_le_iff' hs]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
have neg : ¬BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
Tactic: rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := _ '' _)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_2
f : β → Ordinal.{u_3}
⊢ LE.le.{u_3 + 1} (α := Ordinal.{u_3}) (⨆ (i : β), f i) (⨆ (i : β), f i + 1)
have rw : LE.le (α := Ordinal.{u_3}) (sSup (range fun (i : β) ↦ f i)) (sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' range f))
Tactic: rw [iSup, iSup, range_comp' (· + 1)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)
have apply : LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)
Tactic: apply (iSup_le_iSup_add_one f).antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)
have pos : ∀ (hf' : BddAbove (range f)), LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)
Tactic: by_cases hf' : BddAbove (range f)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
pos : ∀ (hf' : BddAbove (range f)), LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)
have neg : ∀ (hf' : ¬BddAbove (range f)), LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)
Tactic: by_cases hf' : BddAbove (range f)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)
have pos : ∀ (i : β), f i + 1 ≤ ⨆ (i : β), f i
Tactic: rw [ciSup_le_iff' (bddAbove_range_add_one_iff.2 hf')]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i : β
⊢ f i + 1 ≤ ⨆ (i : β), f i
have pos : ∀ (j : β) (hj : i < j), f i + 1 ≤ ⨆ (i : β), f i
Tactic: obtain ⟨j, hj⟩ := exists_gt i
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i j : β
hj : i < j
⊢ f i + 1 ≤ ⨆ (i : β), f i
have pos : f i + 1 ≤ f j
Tactic: apply (le_ciSup hf' j).trans'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i j : β
hj : i < j
⊢ f i + 1 ≤ f j
have pos : f i < f j
Tactic: rw [add_one_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)
have neg : ¬BddAbove.{u + 1} (α := Ordinal.{u}) (range fun (i : β) ↦ f i + 1)
Tactic: rw [ciSup_of_not_bddAbove hf', ciSup_of_not_bddAbove]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
⊢ ¬BddAbove.{u + 1} (α := Ordinal.{u}) (range fun (i : β) ↦ f i + 1)
have neg : ∀ (hf' : ¬BddAbove.{u + 1} (α := Ordinal.{u}) (range fun (i : β) ↦ f i + 1)),
  ¬BddAbove.{u + 1} (α := Ordinal.{u}) (range fun (i : β) ↦ f i + 1)
Tactic: rwa [← bddAbove_range_add_one_iff] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
a : Ordinal.{u}
f : (↑(Iio a) : Type (u + 1)) → Ordinal.{u}
hf : StrictMono f
ha : IsSuccPrelimit a
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i : (↑(Iio a) : Type (u + 1))), f i + 1) (⨆ (i : (↑(Iio a) : Type (u + 1))), f i)
have this : NoMaxOrder.{u + 1} (↑(Iio a) : Type (u + 1))
Tactic: have := ha.noMaxOrder_Iio
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
⊢ sSup (o.brange f) = bsup.{u_3, u_4} o f
have e_a : o.brange f = range (o.familyOfBFamily f)
Tactic: congr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
⊢ o.brange f = range (o.familyOfBFamily f)
have e_a : o.brange f = o.brange f
Tactic: rw [range_familyOfBFamily]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
r r' : ι → ι → Prop
inst : IsWellOrder ι r
inst_1 : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ bsup.{u, v} (type r) (bfamilyOfFamily' r f) = bsup.{u, v} (type r') (bfamilyOfFamily' r' f)
have rw : iSup f = bsup.{u, v} (type r') (bfamilyOfFamily' r' f)
Tactic: rw [bsup'_eq_iSup, bsup'_eq_iSup]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
r r' : ι → ι → Prop
inst : IsWellOrder ι r
inst_1 : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
rw : iSup f = bsup.{u, v} (type r') (bfamilyOfFamily' r' f)
⊢ bsup.{u, v} (type r) (bfamilyOfFamily' r f) = bsup.{u, v} (type r') (bfamilyOfFamily' r' f)
have rw₁ : iSup f = iSup f
Tactic: rw [bsup'_eq_iSup, bsup'_eq_iSup]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ bsup.{u, v} o₁ f = bsup.{u, v} o₂ fun (a : Ordinal.{u}) (h : a < o₂) ↦ f a ⋯
have subst : bsup.{u, v} o₁ f = bsup.{u, v} o₁ fun (a : Ordinal.{u}) (h : a < o₁) ↦ f a sorry
Tactic: subst ho
Cleared hypotheses: o₂, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
h : ∀ (i : o.ToType), o.familyOfBFamily f i ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi ≤ a
have rw : o.familyOfBFamily f
    ((enum fun (x1 x2 : o.ToType) ↦ x1 < x2 :
        (a : (↑(Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) : Type (u + 1))) → o.ToType)
      (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) i sorry)) ≤
  a
Tactic: rw [← familyOfBFamily_enum o f]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (hypothesis)
Goal:
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
h_1 : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
⊢ f (Ordinal.bsup.{u_4, u_3} (type r) g) =
    Ordinal.bsup.{u_4, u_5} (type r) fun (a : Ordinal.{u_4}) (h : a < type r) ↦ f (g a h)
have this : Nonempty α
Tactic: haveI := type_ne_zero_iff_nonempty.1 h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
h_1 : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ f (Ordinal.bsup.{u_4, u_3} (type r) g) =
    Ordinal.bsup.{u_4, u_5} (type r) fun (a : Ordinal.{u_4}) (h : a < type r) ↦ f (g a h)
have rw : Eq (α := Ordinal.{max u_4 u_5}) (⨆ (i : α), f (familyOfBFamily' r sorry g i))
  (iSup (familyOfBFamily' r sorry fun (a : Ordinal.{u_4}) (h : a < type r) ↦ f (g a h)))
Tactic: rw [← iSup'_eq_bsup r, Order.IsNormal.map_iSup H bddAbove_of_small, ← iSup'_eq_bsup r]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
h_1 : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
rw :
  Eq (α := Ordinal.{max u_4 u_5}) (⨆ (i : α), f (familyOfBFamily' r ⋯ g i))
    (iSup (familyOfBFamily' r ⋯ fun (a : Ordinal.{u_4}) (h : a < type r) ↦ f (g a h)))
⊢ f (Ordinal.bsup.{u_4, u_3} (type r) g) =
    Ordinal.bsup.{u_4, u_5} (type r) fun (a : Ordinal.{u_4}) (h : a < type r) ↦ f (g a h)
have ho : type r = type r
Tactic: rw [← iSup'_eq_bsup r, Order.IsNormal.map_iSup H bddAbove_of_small, ← iSup'_eq_bsup r]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ bsup.{u, v} o f
a : Ordinal.{max u v}
⊢ a < bsup.{u, v} o f → succ a < bsup.{u, v} o f
have rw : ∀ (hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ iSup (o.familyOfBFamily f)),
  ∀ a < iSup (o.familyOfBFamily f), succ a < iSup (o.familyOfBFamily f)
Tactic: rw [← iSup_eq_bsup] at *
Cleared hypotheses: hf, a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ bsup.{u_3, u_4} o f = 0 ↔ ∀ (i : Ordinal.{u_3}) (hi : i < o), f i hi = 0
have h : ∀ (h : bsup.{u_3, u_4} o f = 0) (i : Ordinal.{u_3}) (hi : i < o), f i hi = 0
Tactic: refine
    ⟨fun h i hi => ?_, fun h =>
      le_antisymm (bsup_le fun i hi => nonpos_iff_eq_zero.2 (h i hi)) zero_le⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
h : bsup.{u_3, u_4} o f = 0
i : Ordinal.{u_3}
hi : i < o
⊢ f i hi = 0
have rw : f i hi ≤ bsup.{u_3, u_4} o f
Tactic: rw [← nonpos_iff_eq_zero, ← h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}
⊢ bsup.{u_3, u_4} 1 f = f 0 ⋯
have simp_rw : iSup (familyOfBFamily 1 f) = f 0 sorry
Tactic: simp_rw [← iSup_eq_bsup, ciSup_unique, familyOfBFamily, familyOfBFamily', typein_one_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}
simp_rw : iSup (familyOfBFamily 1 f) = f 0 ⋯
⊢ bsup.{u_3, u_4} 1 f = f 0 ⋯
have simp_rw₁ : familyOfBFamily 1 f default = f 0 sorry
Tactic: simp_rw [← iSup_eq_bsup, ciSup_unique, familyOfBFamily, familyOfBFamily', typein_one_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}
simp_rw : iSup (familyOfBFamily 1 f) = f 0 ⋯
simp_rw₁ : familyOfBFamily 1 f default = f 0 ⋯
⊢ bsup.{u_3, u_4} 1 f = f 0 ⋯
have simp_rw₂ : familyOfBFamily' (fun (x1 x2 : ToType 1) ↦ x1 < x2) sorry f default = f 0 sorry
Tactic: simp_rw [← iSup_eq_bsup, ciSup_unique, familyOfBFamily, familyOfBFamily', typein_one_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}
simp_rw : iSup (familyOfBFamily 1 f) = f 0 ⋯
simp_rw₁ : familyOfBFamily 1 f default = f 0 ⋯
simp_rw₂ : familyOfBFamily' (fun (x1 x2 : ToType 1) ↦ x1 < x2) ⋯ f default = f 0 ⋯
⊢ bsup.{u_3, u_4} 1 f = f 0 ⋯
have simp_rw₃ : f
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : ToType 1) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_3}) ↦ x1 < x2)
          (typein fun (x1 x2 : ToType 1) ↦ x1 < x2) :
        (a : ToType 1) → Ordinal.{u_3})
      default)
    sorry =
  f 0 sorry
Tactic: simp_rw [← iSup_eq_bsup, ciSup_unique, familyOfBFamily, familyOfBFamily', typein_one_toType]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
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
i : Ordinal.{u}
hi : i < o
⊢ f i hi ≤ o'.bsup g
have obtain : ∀ (j : Ordinal.{v}) (hj : j < o') (hj' : g j hj = f i hi), f i hi ≤ o'.bsup g
Tactic: obtain ⟨j, hj, hj'⟩ := h ⟨i, hi, rfl⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
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
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ f i hi ≤ o'.bsup g
have rw : g j hj ≤ o'.bsup g
Tactic: rw [← hj']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ ⨆ (a : (↑(Iio o) : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
have simp_rw : ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) sorry = bsup.{u_3, u_4} o f
Tactic: simp_rw [Iio, bsup, iSup, range_familyOfBFamily, brange, range, Subtype.exists, mem_setOf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
simp_rw : ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
⊢ ⨆ (a : (↑(Iio o) : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
have simp_rw₁ : ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) sorry = iSup (o.familyOfBFamily f)
Tactic: simp_rw [Iio, bsup, iSup, range_familyOfBFamily, brange, range, Subtype.exists, mem_setOf]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
simp_rw : ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
simp_rw₁ :
  ⨆ (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = iSup (o.familyOfBFamily f)
⊢ ⨆ (a : (↑(Iio o) : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f
have simp_rw₂ : sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) sorry) =
  sSup (range (o.familyOfBFamily f))
Tactic: simp_rw [Iio, bsup, iSup, range_familyOfBFamily, brange, range, Subtype.exists, mem_setOf]