awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst : Small.{u, u_3} α
inst_1 : Small.{u, u_4} β
a : α
⊢ Membership.mem (γ := Set Ordinal.{u}) (range fun (i : α ⊕ β) ↦ f i) ((fun (a : α) ↦ f (Sum.inl a)) a)

Tactic:
apply mem_range_self

Premises used: Set.mem_range_self
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst : Small.{u, u_3} α
inst_1 : Small.{u, u_4} β
apply : Subset.{u + 1} (α := Set Ordinal.{u}) (range fun (b : β) ↦ f (Sum.inr b)) (range fun (i : α ⊕ β) ↦ f i)
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (b : β), f (Sum.inr b)) (⨆ (i : α ⊕ β), f i)

Tactic:
apply csSup_le_csSup' bddAbove_of_small

Premises used: csSup_le_csSup', Ordinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst : Small.{u, u_3} α
inst_1 : Small.{u, u_4} β
a : β
⊢ Membership.mem (γ := Set Ordinal.{u}) (range fun (i : α ⊕ β) ↦ f i) ((fun (b : β) ↦ f (Sum.inr b)) a)

Tactic:
apply mem_range_self

Premises used: Set.mem_range_self
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α β : Type u
r : α → α → Prop
inst : IsWellOrder α r
f : β → α
h :
  type r ≤
    ⨆ (i : β),
      ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) (f i)
⊢ Unbounded r (range f)

Tactic:
(not_bounded_iff _).1 fun ⟨x, hx⟩ =>
    h.not_gt <| lt_of_le_of_lt
      (Ordinal.iSup_le fun y => ((typein_lt_typein r).2 <| hx _ <| mem_range_self y).le)
      (typein_lt_type r x)

Premises used: Set.mem_range_self, Iff.mpr, lt_of_le_of_lt, False, Ordinal.iSup_le, Ordinal.typein_lt_type, Ordinal.typein_lt_typein, Set.not_bounded_iff, LT.lt.le, _private.0.Ordinal.unbounded_range_of_le_iSup.match_1, LE.le.not_gt, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : Ordinal.{u} → Ordinal.{v}
H : Ordinal.IsNormal f
ι : Type u_3
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst : Nonempty ι
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

Tactic:
Order.IsNormal.map_iSup H hg

Premises used: Order.IsNormal.map_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : Ordinal.{u} → Ordinal.{v}
H : Ordinal.IsNormal f
ι : Type w
g : ι → Ordinal.{u}
inst : Small.{u, w} ι
inst_1 : Nonempty ι
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

Tactic:
Order.IsNormal.map_iSup H bddAbove_of_small

Premises used: Ordinal.bddAbove_of_small, Order.IsNormal.map_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : Ordinal.{u} → Ordinal.{v}
H : Ordinal.IsNormal f
s : Set Ordinal.{u}
hs : BddAbove s
hn : s.Nonempty
⊢ f (sSup s) = sSup (f '' s)

Tactic:
Order.IsNormal.map_sSup H hn hs

Premises used: Order.IsNormal.map_sSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
s : Set Ordinal.{u}
hn : s.Nonempty
inst : Small.{u, u + 1} (↑s : Type (u + 1))
⊢ f (sSup s) = sSup (f '' s)

Tactic:
Order.IsNormal.map_sSup H hn bddAbove_of_small

Premises used: Ordinal.bddAbove_of_small, Order.IsNormal.map_sSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : Ordinal.{u} → Ordinal.{v}
H : Ordinal.IsNormal f
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ f o = ⨆ (a : (↑(Iio o) : Type (u + 1))), f (↑a : Ordinal.{u})

Tactic:
Order.IsNormal.apply_of_isSuccLimit H ho

Premises used: Order.IsNormal.apply_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Cardinal.{u_3}
inl : ord (sSup ∅) = sSup (ord '' ∅)
inr : ∀ (hn : s.Nonempty), (sSup s).ord = sSup (ord '' s)
⊢ (sSup s).ord = sSup (ord '' s)

Tactic:
obtain rfl | hn := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
⊢ ord (sSup ∅) = sSup (ord '' ∅)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Cardinal.{u_3}
hn : s.Nonempty
pos : ∀ (hs : BddAbove s), (sSup s).ord = sSup (ord '' s)
neg : ∀ (hs : ¬BddAbove s), (sSup s).ord = sSup (ord '' s)
⊢ (sSup s).ord = sSup (ord '' s)

Tactic:
by_cases hs : BddAbove s

Premises used: BddAbove
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : BddAbove s
⊢ (sSup s).ord = sSup (ord '' s)

Tactic:
isNormal_ord.map_sSup hn hs

Premises used: Cardinal.isNormal_ord, Order.IsNormal.map_sSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : BddAbove s
⊢ (sSup s).ord = sSup (ord '' s)

Tactic:
exact isNormal_ord.map_sSup hn hs

Premises used: Cardinal.isNormal_ord, Order.IsNormal.map_sSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : ¬BddAbove s
neg : ord (sSup ∅) = sSup ∅
⊢ (sSup s).ord = sSup (ord '' s)

Tactic:
rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (bddAbove_ord_image_iff.not.2 hs)]

Premises used: Iff.mpr, Cardinal.bddAbove_ord_image_iff, Iff.not, csSup_of_not_bddAbove
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : ¬BddAbove s
⊢ ord (sSup ∅) = sSup ∅

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Family
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)
rw₃ rw₄ : sSup (ord '' range fun (i : ι) ↦ f i) = sSup (ord '' range f)
⊢ ord (⨆ (i : ι), f i) = ⨆ (i : ι), (f i).ord

Tactic:
rw [iSup, iSup, sSup_ord, range_comp']

Premises used: iSup, Ordinal.sSup_ord, Set.range_comp'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
rw : #(↑(Iio (sInf sᶜ)) : Type (u + 1)) ≤ #(↑s : Type (u + 1))
⊢ Cardinal.lift.{u + 1, u} (sInf sᶜ).card ≤ #(↑s : Type (u + 1))

Tactic:
rw [← Cardinal.mk_Iio_ordinal]

Premises used: Cardinal.mk_Iio_ordinal
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
⊢ #(↑(Iio (sInf sᶜ)) : Type (u + 1)) ≤ #(↑s : Type (u + 1))

Tactic:
mk_le_mk_of_subset fun x (hx : x < _) ↦ ?_

Premises used: Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
refine : ∀ (x : Ordinal.{u}) (hx : x < sInf sᶜ), x ∈ s
⊢ #(↑(Iio (sInf sᶜ)) : Type (u + 1)) ≤ #(↑s : Type (u + 1))

Tactic:
refine mk_le_mk_of_subset fun x (hx : x < _) ↦ ?_

Premises used: Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
rw : ¬x ∉ s
⊢ x ∈ s

Tactic:
rw [← not_notMem]

Premises used: Set.not_notMem
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ ¬x ∉ s

Tactic:
notMem_of_lt_csInf' hx

Premises used: Set.Mem, setOf, notMem_of_lt_csInf', Not
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ ¬x ∉ s

Tactic:
exact notMem_of_lt_csInf' hx

Premises used: notMem_of_lt_csInf'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
rw : Cardinal.lift.{(max u v) + 1, max u v} (sInf (range f)ᶜ).card ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι
⊢ (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι

Tactic:
rw [← Cardinal.lift_le.{max u v + 1}, Cardinal.lift_lift]

Premises used: Cardinal.lift_lift
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
apply : #(↑(range f) : Type ((max u v) + 1)) ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι
⊢ Cardinal.lift.{(max u v) + 1, max u v} (sInf (range f)ᶜ).card ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι

Tactic:
apply (lift_card_sInf_compl_le _).trans

Premises used: Ordinal.lift_card_sInf_compl_le, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
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} #ι
⊢ #(↑(range f) : Type ((max u v) + 1)) ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι

Tactic:
rw [← Cardinal.lift_id'.{u, max u v + 1} #(range _)]
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ 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:
mk_range_le_lift

Premises used: Cardinal.mk_range_le_lift
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ 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:
exact mk_range_le_lift

Premises used: Cardinal.mk_range_le_lift
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{u}
⊢ (sInf (range f)ᶜ).card ≤ #ι

Tactic:
Cardinal.lift_id #ι ▸ card_sInf_range_compl_le_lift f

Premises used: Ordinal.card_sInf_range_compl_le_lift, Cardinal.mk, Eq.rec, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
rw : (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι
⊢ sInf (range f)ᶜ < lift.{v, u} (succ #ι).ord

Tactic:
rw [lift_ord, Cardinal.lift_succ, ← card_le_iff]

Premises used: Cardinal.lift_succ, Cardinal.card_le_iff, Cardinal.lift_ord
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι

Tactic:
card_sInf_range_compl_le_lift f

Premises used: Ordinal.card_sInf_range_compl_le_lift
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι

Tactic:
exact card_sInf_range_compl_le_lift f

Premises used: Ordinal.card_sInf_range_compl_le_lift
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{u}
⊢ sInf (range f)ᶜ < (succ #ι).ord

Tactic:
lift_id (succ #ι).ord ▸ sInf_compl_lt_lift_ord_succ f

Premises used: Ordinal.sInf_compl_lt_lift_ord_succ, Order.succ, Ordinal.lift_id, Cardinal.mk, Eq.rec, Cardinal.ord
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
mp : BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s) → BddAbove s
mpr : BddAbove s → BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
⊢ BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s) ↔ BddAbove s

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : Membership.mem (γ := Set Ordinal.{u_3}) (upperBounds ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)) a
⊢ BddAbove s

Tactic:
⟨a, fun b hb ↦ (lt_add_one _).le.trans (ha (mem_image_of_mem _ hb))⟩

Premises used: lt_add_one, LT.lt.le, BddAbove, Set.Nonempty, HAdd.hAdd, Set.mem_image_of_mem, Exists.intro, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : Membership.mem (γ := Set Ordinal.{u_3}) (upperBounds ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)) a
⊢ BddAbove s

Tactic:
exact ⟨a, fun b hb ↦ (lt_add_one _).le.trans (ha (mem_image_of_mem _ hb))⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds s
h : Membership.mem (γ := Set Ordinal.{u_3}) (upperBounds ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)) (a + 1)
⊢ BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)

Tactic:
use a + 1
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds s
⊢ Membership.mem (γ := Set Ordinal.{u_3}) (upperBounds ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)) (a + 1)

Tactic:
simpa [upperBounds]

Premises used: upperBounds
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
β : Type u_2
f : β → Ordinal.{u}
rw : BddAbove (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ x + 1) '' range f) ↔ BddAbove (range f)
rw₁ rw₂ : BddAbove (range f) ↔ BddAbove (range f)
⊢ BddAbove.{u + 1} (α := Ordinal.{u}) (range fun (i : β) ↦ f i + 1) ↔ BddAbove (range f)

Tactic:
rw [range_comp' (· + 1), bddAbove_add_one_image_iff]

Premises used: HAdd.hAdd, OfNat.ofNat, Set.range_comp', Ordinal.bddAbove_add_one_image_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
pos : ∀ (hs : BddAbove s), sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
neg : ∀ (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)

Tactic:
by_cases hs : BddAbove s

Premises used: BddAbove
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
hs : BddAbove s
⊢ BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)

Tactic:
have hs' := bddAbove_add_one_image_iff.2 hs
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
hs : BddAbove s
hs' : BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
pos : ∀ x ∈ s, x ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
⊢ sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)

Tactic:
rw [csSup_le_iff' hs]

Premises used: csSup_le_iff'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
hs : BddAbove s
hs' : BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
⊢ ∀ x ∈ s, x ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)

Tactic:
fun x hx ↦ (lt_add_one _).le.trans (le_csSup hs' (mem_image_of_mem _ hx))

Premises used: lt_add_one, LT.lt.le, HAdd.hAdd, Set.mem_image_of_mem, LE.le.trans, le_csSup, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
hs : BddAbove s
hs' : BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
⊢ ∀ x ∈ s, x ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)

Tactic:
exact fun x hx ↦ (lt_add_one _).le.trans (le_csSup hs' (mem_image_of_mem _ hx))

Premises used: lt_add_one, LT.lt.le, HAdd.hAdd, Set.mem_image_of_mem, LE.le.trans, le_csSup, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
neg : ¬BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)
⊢ sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)

Tactic:
rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := _ '' _)]

Premises used: csSup_of_not_bddAbove
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u_3}
hs neg neg₁ neg₂ neg₃ : ¬BddAbove s
⊢ ¬BddAbove (α := Ordinal.{u_3}) ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' s)

Tactic:
rwa [bddAbove_add_one_image_iff]

Premises used: Ordinal.bddAbove_add_one_image_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
β : Type u_2
f : β → Ordinal.{u_3}
rw : LE.le (α := Ordinal.{u_3}) (sSup (range fun (i : β) ↦ f i)) (sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' range f))
⊢ LE.le.{u_3 + 1} (α := Ordinal.{u_3}) (⨆ (i : β), f i) (⨆ (i : β), f i + 1)

Tactic:
rw [iSup, iSup, range_comp' (· + 1)]

Premises used: iSup, HAdd.hAdd, OfNat.ofNat, Set.range_comp'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
β : Type u_2
f : β → Ordinal.{u_3}
⊢ LE.le (α := Ordinal.{u_3}) (sSup (range fun (i : β) ↦ f i)) (sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' range f))

Tactic:
sSup_le_sSup_add_one _

Premises used: Ordinal.sSup_le_sSup_add_one
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
β : Type u_2
f : β → Ordinal.{u_3}
⊢ LE.le (α := Ordinal.{u_3}) (sSup (range fun (i : β) ↦ f i)) (sSup ((fun (x : Ordinal.{u_3}) ↦ x + 1) '' range f))

Tactic:
exact sSup_le_sSup_add_one _

Premises used: Ordinal.sSup_le_sSup_add_one
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
apply : LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)

Tactic:
apply (iSup_le_iSup_add_one f).antisymm'

Premises used: LE.le.antisymm', Ordinal.iSup_le_iSup_add_one
-- Module: Mathlib.SetTheory.Ordinal.Family
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)
neg : ∀ (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)

Tactic:
by_cases hf' : BddAbove (range f)

Premises used: BddAbove, Set.range
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
pos : ∀ (i : β), f i + 1 ≤ ⨆ (i : β), f i
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)

Tactic:
rw [ciSup_le_iff' (bddAbove_range_add_one_iff.2 hf')]

Premises used: Iff.mpr, Ordinal.bddAbove_range_add_one_iff, ciSup_le_iff'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i : β
pos : ∀ (j : β) (hj : i < j), f i + 1 ≤ ⨆ (i : β), f i
⊢ f i + 1 ≤ ⨆ (i : β), f i

Tactic:
obtain ⟨j, hj⟩ := exists_gt i

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i j : β
hj : i < j
pos : f i + 1 ≤ f j
⊢ f i + 1 ≤ ⨆ (i : β), f i

Tactic:
apply (le_ciSup hf' j).trans'

Premises used: le_ciSup, LE.le.trans'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i j : β
hj : i < j
pos : f i < f j
⊢ f i + 1 ≤ f j

Tactic:
rw [add_one_le_iff]

Premises used: Order.add_one_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
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 < f j

Tactic:
hf hj
-- Module: Mathlib.SetTheory.Ordinal.Family
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 < f j

Tactic:
exact hf hj
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
neg : ¬BddAbove.{u + 1} (α := Ordinal.{u}) (range fun (i : β) ↦ f i + 1)
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (i : β), f i + 1) (⨆ (i : β), f i)

Tactic:
rw [ciSup_of_not_bddAbove hf', ciSup_of_not_bddAbove]

Premises used: ciSup_of_not_bddAbove
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
β : Type u_3
inst : LinearOrder β
inst_1 : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
neg neg₁ neg₂ neg₃ :
  ∀ (hf' : ¬BddAbove.{u + 1} (α := Ordinal.{u}) (range fun (i : β) ↦ f i + 1)),
    ¬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'

Premises used: Ordinal.bddAbove_range_add_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
a : Ordinal.{u}
f : (↑(Iio a) : Type (u + 1)) → Ordinal.{u}
hf : StrictMono f
ha : IsSuccPrelimit a
⊢ NoMaxOrder.{u + 1} (↑(Iio a) : Type (u + 1))

Tactic:
have := ha.noMaxOrder_Iio
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
a : Ordinal.{u}
f : (↑(Iio a) : Type (u + 1)) → Ordinal.{u}
hf : StrictMono f
ha : IsSuccPrelimit a
this : NoMaxOrder.{u + 1} (↑(Iio a) : Type (u + 1))
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i : (↑(Iio a) : Type (u + 1))), f i + 1) (⨆ (i : (↑(Iio a) : Type (u + 1))), f i)

Tactic:
iSup_add_one hf

Premises used: Ordinal.iSup_add_one
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
a : Ordinal.{u}
f : (↑(Iio a) : Type (u + 1)) → Ordinal.{u}
hf : StrictMono f
ha : IsSuccPrelimit a
this : NoMaxOrder.{u + 1} (↑(Iio a) : Type (u + 1))
⊢ Eq.{u + 2} (α := Ordinal.{u}) (⨆ (i : (↑(Iio a) : Type (u + 1))), f i + 1) (⨆ (i : (↑(Iio a) : Type (u + 1))), f i)

Tactic:
exact iSup_add_one hf

Premises used: Ordinal.iSup_add_one
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst : IsWellOrder ι r
inst_1 : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{u_3}
⊢ range (familyOfBFamily' r ho f) = range (familyOfBFamily' r' ho' f)

Tactic:
simp_rw [range_familyOfBFamily']

Premises used: Ordinal.range_familyOfBFamily'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
⊢ iSup (o.familyOfBFamily f) = bsup.{u_3, u_4} o f

Tactic:
rfl

Premises used: Ordinal.bsup, rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
ι : Type u_3
r : ι → ι → Prop
inst : IsWellOrder ι r
ho : type r = o
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
⊢ iSup (familyOfBFamily' r ho f) = bsup.{u_3, u_4} o f

Tactic:
iSup_eq_iSup r _ ho _ f

Premises used: Ordinal.iSup_eq_iSup, Ordinal.familyOfBFamily, Ordinal.bsup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
e_a : o.brange f = range (o.familyOfBFamily f)
⊢ sSup (o.brange f) = bsup.{u_3, u_4} o f

Tactic:
congr
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
e_a e_a₁ : o.brange f = o.brange f
⊢ o.brange f = range (o.familyOfBFamily f)

Tactic:
rw [range_familyOfBFamily]

Premises used: Ordinal.range_familyOfBFamily
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
r : ι → ι → Prop
inst : IsWellOrder ι r
f : ι → Ordinal.{max u_3 u_4}
⊢ bsup.{u_3, u_4} (type r) (bfamilyOfFamily' r f) = iSup f

Tactic:
simp +unfoldPartialApp only [← iSup'_eq_bsup r, enum_typein, familyOfBFamily', bfamilyOfFamily']

Premises used: Ordinal.bfamilyOfFamily', Ordinal.enum_typein, Ordinal.iSup'_eq_bsup, Ordinal.familyOfBFamily'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ bsup.{u_3, u_4} (type (α := ι) WellOrderingRel) (bfamilyOfFamily f) = iSup f

Tactic:
bsup'_eq_iSup _ f

Premises used: Ordinal.bfamilyOfFamily, Ordinal.bsup'_eq_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
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)
rw₁ rw₂ : iSup f = iSup f
⊢ bsup.{u, v} (type r) (bfamilyOfFamily' r f) = bsup.{u, v} (type r') (bfamilyOfFamily' r' f)

Tactic:
rw [bsup'_eq_iSup, bsup'_eq_iSup]

Premises used: Ordinal.bsup'_eq_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
subst : bsup.{u, v} o₁ f = bsup.{u, v} o₁ fun (a : Ordinal.{u}) (h : a < o₁) ↦ f a ⋯
⊢ bsup.{u, v} o₁ f = bsup.{u, v} o₂ fun (a : Ordinal.{u}) (h : a < o₂) ↦ f a ⋯

Tactic:
subst ho
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o₁ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
⊢ bsup.{u, v} o₁ f = bsup.{u, v} o₁ fun (a : Ordinal.{u}) (h : a < o₁) ↦ f a ⋯

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
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
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 ⋯)) ≤
    a
⊢ f i hi ≤ a

Tactic:
rw [← familyOfBFamily_enum o f]

Premises used: Ordinal.familyOfBFamily_enum
-- Module: Mathlib.SetTheory.Ordinal.Family
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
⊢ 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 ⋯)) ≤
    a

Tactic:
h _