awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
rw :
  (∀ (i : Ordinal.{u}) (h : i < type r), f i h < o) ↔
    ∀ (i : α),
      f (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) i) ⋯ <
        o
⊢ blsub.{u, v} (type r) f ≤ o ↔
    (lsub.{u, v} fun (a : α) ↦
        f (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a)
          ⋯) ≤
      o

Tactic:
rw [blsub_le_iff, lsub_le_iff]

Premises used: Ordinal.blsub_le_iff, Ordinal.lsub_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
H :
  ∀ (i : α),
    f (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) i) ⋯ < o
i : Ordinal.{u}
h : i < type r
⊢ f i h < o

Tactic:
simpa only [typein_enum] using H (enum r ⟨i, h⟩)

Premises used: Ordinal.typein_enum, Subtype.mk, Ordinal.enum, DFunLike.coe
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (h : i < type r), f i h < o) ↔
    ∀ (i : α),
      f (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) i) ⋯ <
        o

Tactic:
exact ⟨fun H b => H _ _, fun H i h => by simpa only [typein_enum] using H (enum r ⟨i, h⟩)⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
ho : o ≠ 0
a : Ordinal.{max u v}
⊢ (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ a) = succ a

Tactic:
bsup_const.{u, v} ho (succ a)

Premises used: Order.succ, Ordinal.bsup_const, Ordinal.blsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}
⊢ blsub.{u_3, u_4} 1 f = succ (f 0 ⋯)

Tactic:
bsup_one _

Premises used: Ordinal.bsup_one, Ordinal.blsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
⊢ ∀ (o : Ordinal.{u}), (o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) ↦ x) = o

Tactic:
lsub_typein

Premises used: Ordinal.familyOfBFamily, Ordinal.bsup, Ordinal.blsub, Ordinal.lsub_typein, Ordinal.familyOfBFamily'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
⊢ (∀ a < o, succ a < o) → (o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) ↦ x) = o

Tactic:
iSup_typein_limit

Premises used: Ordinal.familyOfBFamily, Ordinal.bsup, Ordinal.iSup_typein_limit, Ordinal.familyOfBFamily'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
⊢ ((o + 1).bsup fun (x : Ordinal.{u}) (x_1 : x < o + 1) ↦ x) = o

Tactic:
iSup_typein_succ

Premises used: Ordinal.iSup_typein_succ, Order.succ, Ordinal.familyOfBFamily, Ordinal.bsup, Ordinal.familyOfBFamily'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
⊢ ((succ o).bsup fun (x : Ordinal.{u}) (x_1 : x < succ o) ↦ x) = o

Tactic:
iSup_typein_succ

Premises used: Ordinal.iSup_typein_succ, Ordinal.familyOfBFamily, Ordinal.bsup, Ordinal.familyOfBFamily'
-- Module: Mathlib.SetTheory.Ordinal.Family
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
obtain :
  ∀ (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
⊢ Membership.mem (γ := Set Ordinal.{max (max u v) w}) (o'.brange fun (a : Ordinal.{v}) (ha : a < o') ↦ succ (g a ha)) a

Tactic:
obtain ⟨c, hc, hc'⟩ := h ⟨b, hb, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
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
⊢ succ (g c hc) = a

Tactic:
simp_rw [← hc'] at hb'
-- Module: Mathlib.SetTheory.Ordinal.Family
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
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
hb' : succ (g c hc) = a
⊢ Membership.mem (γ := Set Ordinal.{max (max u v) w}) (o'.brange fun (a : Ordinal.{v}) (ha : a < o') ↦ succ (g a ha)) a

Tactic:
⟨c, hc, hb'⟩

Premises used: Set.Mem, Ordinal.brange, setOf, Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.Family
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
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
hb' : succ (g c hc) = a
⊢ Membership.mem (γ := Set Ordinal.{max (max u v) w}) (o'.brange fun (a : Ordinal.{v}) (ha : a < o') ↦ succ (g a ha)) a

Tactic:
exact ⟨c, hc, hb'⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
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 :
  Eq (α := Set Ordinal.{max (max u v) w})
    {o_1 : Ordinal.{max (max u v) w} | ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o_1}
    {o : Ordinal.{max (max u v) w} | ∃ (i : Ordinal.{v}) (hi : i < o'), g i hi = o}
⊢ o.blsub f = o'.blsub g

Tactic:
(blsub_le_of_brange_subset.{u, v, w} h.le).antisymm (blsub_le_of_brange_subset.{v, u, w} h.ge)

Premises used: Eq.ge, LE.le.antisymm, Eq.le, Ordinal.blsub_le_of_brange_subset
-- Module: Mathlib.SetTheory.Ordinal.Family
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'
rw : g a ha < o'.blsub g
⊢ g a ha < o

Tactic:
rw [← hg]
-- Module: Mathlib.SetTheory.Ordinal.Family
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'.blsub g

Tactic:
apply lt_blsub

Premises used: Ordinal.lt_blsub
-- Module: Mathlib.SetTheory.Ordinal.Family
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
a₁ : o.bsup f ≤ o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯
⊢ (o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯) = o.bsup f

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Family
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

Tactic:
bsup_le fun i hi => ?_

Premises used: Ordinal.bsup_le
-- Module: Mathlib.SetTheory.Ordinal.Family
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 : ∀ (i : Ordinal.{max u v}) (hi : i < o'), f (g i hi) ⋯ ≤ o.bsup f
⊢ (o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯) ≤ o.bsup f

Tactic:
refine bsup_le fun i hi => ?_

Premises used: Ordinal.bsup_le
-- Module: Mathlib.SetTheory.Ordinal.Family
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) ⋯

Tactic:
bsup_le fun i hi => ?_

Premises used: Ordinal.bsup_le
-- Module: Mathlib.SetTheory.Ordinal.Family
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 : ∀ (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) ⋯
⊢ o.bsup f ≤ o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯

Tactic:
refine bsup_le fun i hi => ?_

Premises used: Ordinal.bsup_le
-- Module: Mathlib.SetTheory.Ordinal.Family
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 (g i hi) ⋯ ≤ o.bsup f

Tactic:
apply le_bsup

Premises used: Ordinal.le_bsup
-- Module: Mathlib.SetTheory.Ordinal.Family
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
⊢ ∃ (i_1 : Ordinal.{max u v}) (hi : i_1 < o'), i ≤ g i_1 hi

Tactic:
rw [← hg, lt_blsub_iff] at hi

Premises used: Ordinal.lt_blsub_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
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
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) ⋯
⊢ f i hi_1 ≤ o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯

Tactic:
rcases hi with ⟨j, hj, hj'⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
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
j : Ordinal.{max u v}
hj : j < o'
hj' : i ≤ g j hj
⊢ f i hi ≤ o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯

Tactic:
(hf _ _ hj').trans (le_bsup _ _ _)

Premises used: Ordinal.le_bsup, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Family
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
j : Ordinal.{max u v}
hj : j < o'
hj' : i ≤ g j hj
⊢ f i hi ≤ o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯

Tactic:
exact (hf _ _ hj').trans (le_bsup _ _ _)

Premises used: Ordinal.le_bsup, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Family
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'.blsub fun (a : Ordinal.{max u v}) (ha : a < o') ↦ f (g a ha) ⋯) = o.blsub f

Tactic:
@bsup_comp.{u, v, w} o _ (fun a ha => succ (f a ha))
    (fun {_ _} _ _ h => succ_le_succ_iff.2 (hf _ _ h)) g hg

Premises used: Iff.mpr, Order.succ_le_succ_iff, Ordinal.blsub, Ordinal.bsup_comp
-- Module: Mathlib.SetTheory.Ordinal.Family
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
rw₁ rw₂ : f o = f o
⊢ (Ordinal.bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o

Tactic:
rw [← IsNormal.bsup.{u, u, v} H (fun x _ => x) h.ne_bot, bsup_id_limit fun _ ↦ h.succ_lt]

Premises used: Order.IsSuccLimit.succ_lt, Ordinal.bsup_id_limit
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
rw : ∀ (a : Ordinal.{u}) (ha : a < o), f a < f (succ a)
⊢ (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o

Tactic:
rw [← IsNormal.bsup_eq.{u, v} H h, bsup_eq_blsub_of_lt_succ_limit h]

Premises used: Ordinal.bsup_eq_blsub_of_lt_succ_limit
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ ∀ (a : Ordinal.{u}) (ha : a < o), f a < f (succ a)

Tactic:
fun a _ => H.strictMono (lt_succ a)

Premises used: Order.lt_succ, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ ∀ (a : Ordinal.{u}) (ha : a < o), f a < f (succ a)

Tactic:
exact fun a _ => H.strictMono (lt_succ a)

Premises used: Order.lt_succ, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Family
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
rw : IsLUB (f '' Iio a) (bsup.{u, v} a fun (x : Ordinal.{u}) (x_1 : x < a) ↦ f x)
⊢ IsLUB (f '' Iio a) (f a)

Tactic:
rw [← h₂ _ ho]
-- Module: Mathlib.SetTheory.Ordinal.Family
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) (bsup.{u, v} a fun (x : Ordinal.{u}) (x_1 : x < a) ↦ f x)

Tactic:
simpa [IsLUB, upperBounds, lowerBounds, IsLeast, bsup_le_iff] using le_bsup _

Premises used: lowerBounds, upperBounds, IsLeast, Ordinal.le_bsup, Ordinal.bsup_le_iff, IsLUB
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : Ordinal.{u} → Ordinal.{max u v}
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)
⊢ 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

Tactic:
rw [isNormal_iff_lt_succ_and_bsup_eq.{u, v}, and_congr_right_iff]

Premises used: and_congr_right_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
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
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
⊢ (∀ (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
-- Module: Mathlib.SetTheory.Ordinal.Family
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
⊢ (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o

Tactic:
have := H o ho
-- Module: Mathlib.SetTheory.Ordinal.Family
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
⊢ (blsub.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o

Tactic:
have := H o ho
-- Module: Mathlib.SetTheory.Ordinal.Family
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
this : (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ f x) = f o
mp mp₁ mp₂ mp₃ : (bsup.{u, v} o fun (a : Ordinal.{u}) (x : a < o) ↦ f a) = f o
⊢ (blsub.{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 *

Premises used: Ordinal.bsup_eq_blsub_of_lt_succ_limit
-- Module: Mathlib.SetTheory.Ordinal.Family
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
mpr mpr₁ mpr₂ 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
⊢ (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 *

Premises used: Ordinal.bsup_eq_blsub_of_lt_succ_limit
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f g : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hg : IsNormal g
⊢ f = g ↔ f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (succ a) = g (succ a)

Tactic:
Order.IsNormal.ext_iff hf hg

Premises used: Order.IsNormal.ext_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
obtain : ∀ (a : α) (ha : f a = ⨆ (i : α), succ (f i)), False
⊢ False

Tactic:
obtain ⟨a, ha⟩ := h (⨆ i, succ (f i))

Premises used: Order.succ, iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
a : α
ha : f a = ⨆ (i : α), succ (f i)
apply : f a < ⨆ (i : α), succ (f i)
⊢ False

Tactic:
apply ha.not_lt

Premises used: Eq.not_lt
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
a : α
ha : f a = ⨆ (i : α), succ (f i)
rw : ∃ (i : α), f a < succ (f i)
⊢ f a < ⨆ (i : α), succ (f i)

Tactic:
rw [Ordinal.lt_iSup_iff]

Premises used: Ordinal.lt_iSup_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
a : α
ha : f a = ⨆ (i : α), succ (f i)
⊢ ∃ (i : α), f a < succ (f i)

Tactic:
⟨a, Order.lt_succ _⟩

Premises used: Order.lt_succ, Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
a : α
ha : f a = ⨆ (i : α), succ (f i)
⊢ ∃ (i : α), f a < succ (f i)

Tactic:
exact ⟨a, Order.lt_succ _⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : Ordinal.{u} → α
⊢ ¬Injective f

Tactic:
fun h ↦ not_surjective_of_ordinal _ (invFun_surjective h)

Premises used: Function.invFun, Function.invFun_surjective, not_surjective_of_ordinal, Not
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
⊢ ¬Small.{u, max (u + 1) (v + 1)} Ordinal.{max u v}

Tactic:
fun h =>
  @not_injective_of_ordinal _ h _ fun _a _b => Ordinal.lift_inj.{v, u}.1

Premises used: not_injective_of_ordinal, Ordinal.lift, Ordinal.lift_inj, Iff.mp, Not
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
⊢ Uncountable Ordinal.{u}

Tactic:
Uncountable.of_not_small not_small_ordinal.{u}

Premises used: not_small_ordinal, Uncountable.of_not_small
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
rw : ¬Small.{u, u + 1} (↑sᶜ : Type (u + 1))
⊢ ¬BddAbove sᶜ

Tactic:
rw [bddAbove_iff_small]

Premises used: Ordinal.bddAbove_iff_small
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
h : Small.{u, u + 1} (↑sᶜ : Type (u + 1))
⊢ Small.{u, u + 1} (↑(s ∪ sᶜ) : Type (u + 1))

Tactic:
have := small_union s sᶜ
-- Module: Mathlib.SetTheory.Ordinal.Family
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))
⊢ Small.{u, u + 1} Ordinal.{u}

Tactic:
rw [union_compl_self, small_univ_iff] at this

Premises used: Set.union_compl_self, small_univ_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
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} Ordinal.{u}
⊢ False

Tactic:
not_small_ordinal this

Premises used: not_small_ordinal
-- Module: Mathlib.SetTheory.Ordinal.Family
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} Ordinal.{u}
⊢ False

Tactic:
exact not_small_ordinal this

Premises used: not_small_ordinal
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
⊢ iSup Nat.cast = ω

Tactic:
(Ordinal.iSup_le fun n => (natCast_lt_omega0 n).le).antisymm <| omega0_le.2 <| Ordinal.le_iSup _

Premises used: Iff.mpr, Ordinal.iSup_le, LE.le.antisymm, Ordinal.omega0_le, LT.lt.le, Ordinal.natCast_lt_omega0, Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : Ordinal.{u} → Ordinal.{v}
hf : IsNormal f
rw : ⨆ (n : ℕ), f (↑n : Ordinal.{u}) = f (iSup Nat.cast)
rw₁ rw₂ : Eq.{v + 2} (α := Ordinal.{v}) (⨆ (n : ℕ), f (↑n : Ordinal.{u})) (⨆ (i : ℕ), f (↑i : Ordinal.{u}))
⊢ ⨆ (n : ℕ), f (↑n : Ordinal.{u}) = f ω

Tactic:
rw [← iSup_natCast, hf.map_iSup bddAbove_of_small]

Premises used: Ordinal.bddAbove_of_small, Order.IsNormal.map_iSup, Ordinal.iSup_natCast
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
ι : Type u_1
inst : Small.{u, u_1} ι
inst_1 : Nonempty ι
f : ι → Ordinal.{u}
⊢ o + ⨆ (i : ι), f i = ⨆ (i : ι), o + f i

Tactic:
(isNormal_add_right o).map_iSup bddAbove_of_small

Premises used: Ordinal.bddAbove_of_small, Order.IsNormal.map_iSup, Ordinal.isNormal_add_right