awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
h : Nonempty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ 0 < lsub.{u_3, u_4} f

Tactic:
h.elim fun i => (lt_lsub f i).pos

Premises used: LT.lt.pos, Nonempty.elim, Ordinal.lt_lsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
⊢ lsub.{u_3, v} f = 0 ↔ IsEmpty ι

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

Premises used: IsEmpty.mk, Iff.intro, Ordinal.lsub_empty
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
refine : ∀ (h : lsub.{u_3, v} f = 0) (i : ι), False
⊢ lsub.{u_3, v} f = 0 ↔ IsEmpty ι

Tactic:
refine ⟨fun h => ⟨fun i => ?_⟩, fun h => @lsub_empty _ h _⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub.{u_3, v} f = 0
i : ι
⊢ 0 < lsub.{u_3, v} f

Tactic:
have := @lsub_pos.{_, v} _ ⟨i⟩ f
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub.{u_3, v} f = 0
i : ι
this : 0 < lsub.{u_3, v} f
⊢ LT.lt (α := Ordinal.{max u_3 v}) 0 0

Tactic:
rw [h] at this
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub.{u_3, v} f = 0
i : ι
this : LT.lt (α := Ordinal.{max u_3 v}) 0 0
⊢ False

Tactic:
this.false

Premises used: LT.lt.false
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub.{u_3, v} f = 0
i : ι
this : LT.lt (α := Ordinal.{max u_3 v}) 0 0
⊢ False

Tactic:
exact this.false

Premises used: LT.lt.false
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
inst : Nonempty ι
o : Ordinal.{max u_4 u_3}
⊢ (lsub.{u_3, u_4} fun (x : ι) ↦ o) = succ o

Tactic:
ciSup_const

Premises used: Order.succ, Ordinal.lsub, ciSup_const
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
inst : Unique ι
f : ι → Ordinal.{max u_4 u_3}
⊢ lsub.{u_3, u_4} f = succ (f default)

Tactic:
ciSup_unique

Premises used: ciSup_unique, Ordinal.lsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ succ '' range f ⊆ succ '' range g

Tactic:
Set.image_mono h

Premises used: Set.image_mono
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
h₁ : range (succ ∘ f) = succ '' range f
h₂ : range (succ ∘ g) = succ '' range g
convert_2 : Ordinal.{max (max u v) w} → Ordinal.{max u v w}
⊢ range (succ ∘ f) ⊆ range (succ ∘ g)

Tactic:
convert! Set.image_mono h

Premises used: Set.image_mono
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ range (succ ∘ f) = succ '' range f

Tactic:
apply Set.range_comp

Premises used: Set.range_comp
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ range (succ ∘ g) = succ '' range g

Tactic:
apply Set.range_comp

Premises used: Set.range_comp
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f = range g
⊢ lsub f = lsub g

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

Premises used: Eq.ge, LE.le.antisymm, Eq.le, Ordinal.lsub_le_of_range_subset
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u
β : Type v
f : α ⊕ β → Ordinal.{max (max u v) w}
⊢ lsub f = max (lsub fun (a : α) ↦ f (Sum.inl a)) (lsub fun (b : β) ↦ f (Sum.inr b))

Tactic:
iSup_sum _

Premises used: Ordinal.iSup_sum, Ordinal.lsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ lsub.{u_3, u_4} f ∉ range f

Tactic:
fun ⟨i, h⟩ =>
  h.not_lt (lt_lsub f i)

Premises used: False, _private.0.Ordinal.lsub_notMem_range.match_1, Ordinal.lt_lsub, Eq.not_lt, Not
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (range f)ᶜ.Nonempty

Tactic:
⟨_, lsub_notMem_range f⟩

Premises used: Set.Nonempty, Exists.intro, Ordinal.lsub_notMem_range
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
by_contra! :
  ∀
    (h :
      lsub (ι := o.ToType)
          (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦
                x1 < x2) (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
            (a : o.ToType) → Ordinal.{u}) <
        o),
    False
⊢ o ≤
    lsub (ι := o.ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
        (a : o.ToType) → Ordinal.{u})

Tactic:
by_contra! h
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
h :
  lsub (ι := o.ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
        (a : o.ToType) → Ordinal.{u}) <
    o
⊢ lsub (ι := o.ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
        (a : o.ToType) → Ordinal.{u}) <
    type fun (x1 x2 : o.ToType) ↦ x1 < x2

Tactic:
have h := h.trans_eq (type_toType o).symm
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
h_1 :
  lsub (ι := o.ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
        (a : o.ToType) → Ordinal.{u}) <
    o
h :
  lsub (ι := o.ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
        (a : o.ToType) → Ordinal.{u}) <
    type fun (x1 x2 : o.ToType) ↦ x1 < x2
⊢ False

Tactic:
simpa [typein_enum] using lt_lsub.{u, u} (typein (· < ·)) (enum (· < ·) ⟨_, h⟩)

Premises used: Ordinal.typein_enum
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
ho rwa rwa₁ rwa₂ rwa₃ : ∀ a < o, succ a < o
⊢ IsSuccPrelimit o

Tactic:
rwa [isSuccPrelimit_iff_succ_lt]

Premises used: Order.isSuccPrelimit_iff_succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
ho : ∀ a < o, succ a < o
⊢ IsSuccPrelimit o

Tactic:
replace ho : IsSuccPrelimit o := by rwa [isSuccPrelimit_iff_succ_lt]
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
ho : IsSuccPrelimit o
rw :
  sSup
      {b : Ordinal.{u} |
        b <
          PrincipalSeg.top (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)} =
    o
⊢ iSup (ι := o.ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)) :
        (a : o.ToType) → Ordinal.{u}) =
    o

Tactic:
rw [iSup, PrincipalSeg.range_eq]

Premises used: iSup, PrincipalSeg.range_eq
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
ho : IsSuccPrelimit o
⊢ sSup
      {b : Ordinal.{u} |
        b <
          PrincipalSeg.top (r := fun (x1 x2 : o.ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (typein fun (x1 x2 : o.ToType) ↦ x1 < x2)} =
    o

Tactic:
simpa [Iio_def] using ho.sSup_Iio

Premises used: Set.Iio_def, Order.IsSuccPrelimit.sSup_Iio
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
rw :
  sSup
      {b : Ordinal.{u_3} |
        b <
          PrincipalSeg.top (r := fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{u_3}) ↦ x1 < x2) (typein fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2)} =
    sSup (Iic o)
⊢ iSup (ι := (succ o).ToType)
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (succ o).ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_3}) ↦
            x1 < x2) (typein fun (x1 x2 : (succ o).ToType) ↦ x1 < x2)) :
        (a : (succ o).ToType) → Ordinal.{u_3}) =
    o

Tactic:
rw [← csSup_Iic (a := o), iSup, PrincipalSeg.range_eq]

Premises used: iSup, csSup_Iic, PrincipalSeg.range_eq
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
e_a :
  Eq.{u_3 + 2} (α := Ordinal.{u_3} → Prop)
    (fun (b : Ordinal.{u_3}) ↦
      b <
        PrincipalSeg.top (r := fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_3}) ↦
          x1 < x2) (typein fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2))
    fun (x : Ordinal.{u_3}) ↦ x ≤ o
⊢ sSup
      {b : Ordinal.{u_3} |
        b <
          PrincipalSeg.top (r := fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2) (s :=
            fun (x1 x2 : Ordinal.{u_3}) ↦ x1 < x2) (typein fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2)} =
    sSup (Iic o)

Tactic:
congr
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
⊢ Eq.{u_3 + 2} (α := Ordinal.{u_3} → Prop)
    (fun (b : Ordinal.{u_3}) ↦
      b <
        PrincipalSeg.top (r := fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u_3}) ↦
          x1 < x2) (typein fun (x1 x2 : (succ (sSup (Iic o))).ToType) ↦ x1 < x2))
    fun (x : Ordinal.{u_3}) ↦ x ≤ o

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (bsup.{u, v} o fun (a : Ordinal.{u}) (ha : a < o) ↦ succ (f a ha)) = blsub.{u, v} o f

Tactic:
rfl

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

Tactic:
iSup'_eq_bsup r ho fun a ha => succ (f a ha)

Premises used: Order.succ, Ordinal.iSup'_eq_bsup, Ordinal.lsub, Ordinal.blsub, Ordinal.familyOfBFamily'
-- 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.{max u v}
rw : blsub.{u, v} o f = lsub.{u, v} (familyOfBFamily' r' ho' f)
rw₁ rw₂ : blsub.{u, v} o f = blsub.{u, v} o f
⊢ lsub.{u, v} (familyOfBFamily' r ho f) = lsub.{u, v} (familyOfBFamily' r' ho' f)

Tactic:
rw [lsub_eq_blsub', lsub_eq_blsub']

Premises used: Ordinal.lsub_eq_blsub'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ lsub.{u, v} (o.familyOfBFamily f) = blsub.{u, v} o f

Tactic:
lsub_eq_blsub' _ _ _

Premises used: Ordinal.familyOfBFamily, Ordinal.lsub_eq_blsub'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
f : ι → Ordinal.{max u v}
⊢ blsub.{u, v} (type r) (bfamilyOfFamily' r f) = lsub.{u, v} f

Tactic:
bsup'_eq_iSup r (succ ∘ f)

Premises used: Ordinal.bfamilyOfFamily', Order.succ, Function.comp, Ordinal.lsub, Ordinal.blsub, 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 : lsub.{u, v} f = blsub.{u, v} (type r') (bfamilyOfFamily' r' f)
rw₁ rw₂ : lsub.{u, v} f = lsub.{u, v} f
⊢ blsub.{u, v} (type r) (bfamilyOfFamily' r f) = blsub.{u, v} (type r') (bfamilyOfFamily' r' f)

Tactic:
rw [blsub_eq_lsub', blsub_eq_lsub']

Premises used: Ordinal.blsub_eq_lsub'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ blsub.{u, v} (type (α := ι) WellOrderingRel) (bfamilyOfFamily f) = lsub.{u, v} f

Tactic:
blsub_eq_lsub' _ _

Premises used: Ordinal.bfamilyOfFamily, Ordinal.blsub_eq_lsub'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
subst : blsub.{u, v} o₁ f = blsub.{u, v} o₁ fun (a : Ordinal.{u}) (h : a < o₁) ↦ f a ⋯
⊢ blsub.{u, v} o₁ f = blsub.{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}
⊢ blsub.{u, v} o₁ f = blsub.{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}
⊢ (bsup.{u, v} o fun (a : Ordinal.{u}) (ha : a < o) ↦ succ (f a ha)) ≤ a ↔
    ∀ (i : Ordinal.{u}) (h : i < o), succ (f i h) ≤ a

Tactic:
bsup_le_iff.{_, v} (f := fun a ha => succ (f a ha)) (a := a)

Premises used: Ordinal.bsup_le_iff
-- 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 : ∀ (a_1 : Ordinal.{u}), (∀ (h : a_1 < o), f a_1 h < a) ↔ ∀ (h : a_1 < o), succ (f a_1 h) ≤ a
⊢ blsub.{u, v} o f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a

Tactic:
convert! bsup_le_iff.{_, v} (f := fun a ha => succ (f a ha)) (a := a) using 2
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
a_1 : Ordinal.{u}
⊢ (∀ (h : a_1 < o), f a_1 h < a) ↔ ∀ (h : a_1 < o), succ (f a_1 h) ≤ a

Tactic:
simp_rw [succ_le_iff]

Premises used: Order.succ_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
f : (b : Ordinal.{u_3}) → b < o → Ordinal.{max u_3 u_4}
a : Ordinal.{max u_3 u_4}
⊢ (∀ (i : Ordinal.{u_3}) (h : i < o), f i h < a) → blsub.{u_3, u_4} o f ≤ a

Tactic:
blsub_le_iff.2

Premises used: Iff.mpr, Ordinal.blsub_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
i : Ordinal.{u_3}
h : i < o
⊢ f i h < blsub.{u_3, u_4} o f

Tactic:
blsub_le_iff.1 le_rfl _ _

Premises used: Ordinal.blsub_le_iff, le_rfl, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < blsub.{u, v} o f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), a ≤ f i hi

Tactic:
simpa only [not_forall, not_lt, not_le] using not_congr (@blsub_le_iff.{_, v} _ f a)

Premises used: not_le, not_lt, Classical.not_forall
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ bsup.{u, v} o f ≤ blsub.{u, v} o f

Tactic:
bsup_le fun i h => (lt_blsub f i h).le

Premises used: Ordinal.bsup_le, LT.lt.le, Ordinal.lt_blsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ blsub.{u, v} o f ≤ succ (bsup.{u, v} o f)

Tactic:
blsub_le fun i h => lt_succ_iff.2 (le_bsup f i h)

Premises used: Iff.mpr, Ordinal.blsub_le, Order.lt_succ_iff, Ordinal.le_bsup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
rw :
  iSup (o.familyOfBFamily f) = lsub.{u, v} (o.familyOfBFamily f) ∨
    succ (iSup (o.familyOfBFamily f)) = lsub.{u, v} (o.familyOfBFamily f)
⊢ bsup.{u, v} o f = blsub.{u, v} o f ∨ succ (bsup.{u, v} o f) = blsub.{u, v} o f

Tactic:
rw [← iSup_eq_bsup, ← lsub_eq_blsub]

Premises used: Ordinal.iSup_eq_bsup, Ordinal.lsub_eq_blsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ iSup (o.familyOfBFamily f) = lsub.{u, v} (o.familyOfBFamily f) ∨
    succ (iSup (o.familyOfBFamily f)) = lsub.{u, v} (o.familyOfBFamily f)

Tactic:
iSup_eq_lsub_or_succ_iSup_eq_lsub _

Premises used: Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ iSup (o.familyOfBFamily f) = lsub.{u, v} (o.familyOfBFamily f) ∨
    succ (iSup (o.familyOfBFamily f)) = lsub.{u, v} (o.familyOfBFamily f)

Tactic:
exact iSup_eq_lsub_or_succ_iSup_eq_lsub _

Premises used: Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f

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

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
refine_1 : ∀ (h : succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f), ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f
refine_2 : (∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f) → succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f
⊢ succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f
refine_1 : ∀ (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ≠ bsup.{u, v} o f), False
⊢ ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f

Tactic:
by_contra! hf
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ≠ bsup.{u, v} o f
⊢ False

Tactic:
ne_of_lt (succ_le_iff.1 h)
        (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf)))

Premises used: Ordinal.blsub_le, le_antisymm, Ordinal.lt_bsup_of_ne_bsup, Order.succ_le_iff, Iff.mp, Ordinal.bsup_le_blsub, ne_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ≠ bsup.{u, v} o f
⊢ False

Tactic:
exact
      ne_of_lt (succ_le_iff.1 h)
        (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf)))

Premises used: Ordinal.blsub_le, le_antisymm, Ordinal.lt_bsup_of_ne_bsup, Order.succ_le_iff, Iff.mp, Ordinal.bsup_le_blsub, ne_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w : Ordinal.{u}
w_1 : w < o
hf : f w w_1 = bsup.{u, v} o f
refine_2 : f w w_1 < blsub.{u, v} o f
⊢ succ (bsup.{u, v} o f) ≤ blsub.{u, v} o f

Tactic:
rw [succ_le_iff, ← hf]

Premises used: Order.succ_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w : Ordinal.{u}
w_1 : w < o
hf : f w w_1 = bsup.{u, v} o f
⊢ f w w_1 < blsub.{u, v} o f

Tactic:
lt_blsub _ _ _

Premises used: Ordinal.lt_blsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w : Ordinal.{u}
w_1 : w < o
hf : f w w_1 = bsup.{u, v} o f
⊢ f w w_1 < blsub.{u, v} o f

Tactic:
exact lt_blsub _ _ _

Premises used: Ordinal.lt_blsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ succ (bsup.{u, v} o f) = blsub.{u, v} o f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = bsup.{u, v} o f

Tactic:
(blsub_le_bsup_succ f).ge_iff_eq'.symm.trans (bsup_succ_le_blsub f)

Premises used: LE.le.ge_iff_eq', Ordinal.bsup_succ_le_blsub, Iff.trans, Ordinal.blsub_le_bsup_succ, Iff.symm
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
rw :
  iSup (o.familyOfBFamily f) = lsub.{u, v} (o.familyOfBFamily f) ↔
    ∀ a < lsub.{u, v} (o.familyOfBFamily f), succ a < lsub.{u, v} (o.familyOfBFamily f)
⊢ bsup.{u, v} o f = blsub.{u, v} o f ↔ ∀ a < blsub.{u, v} o f, succ a < blsub.{u, v} o f

Tactic:
rw [← iSup_eq_bsup, ← lsub_eq_blsub]

Premises used: Ordinal.iSup_eq_bsup, Ordinal.lsub_eq_blsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ iSup (o.familyOfBFamily f) = lsub.{u, v} (o.familyOfBFamily f) ↔
    ∀ a < lsub.{u, v} (o.familyOfBFamily f), succ a < lsub.{u, v} (o.familyOfBFamily f)

Tactic:
apply iSup_eq_lsub_iff

Premises used: Ordinal.iSup_eq_lsub_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : bsup.{u, v} o f = blsub.{u, v} o f
i : Ordinal.{u}
rw : ∀ (hi : i < o), f i hi < blsub.{u, v} o f
⊢ ∀ (hi : i < o), f i hi < bsup.{u, v} o f

Tactic:
rw [h]
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : bsup.{u, v} o f = blsub.{u, v} o f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < blsub.{u, v} o f

Tactic:
apply lt_blsub

Premises used: Ordinal.lt_blsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯
rw : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < bsup.{u, v} o f
⊢ bsup.{u, v} o f = blsub.{u, v} o f

Tactic:
rw [bsup_eq_blsub_iff_lt_bsup]

Premises used: Ordinal.bsup_eq_blsub_iff_lt_bsup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯
⊢ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < bsup.{u, v} o f

Tactic:
fun i hi => (hf i hi).trans_le (le_bsup f _ _)

Premises used: Order.succ, Order.IsSuccLimit.succ_lt, Ordinal.le_bsup, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯
⊢ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < bsup.{u, v} o f

Tactic:
exact fun i hi => (hf i hi).trans_le (le_bsup f _ _)

Premises used: Order.succ, Order.IsSuccLimit.succ_lt, Ordinal.le_bsup, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < succ o → Ordinal.{max u v}
hf : ∀ {i j : Ordinal.{u}} (hi : i < succ o) (hj : j < succ o), i ≤ j → f i hi ≤ f j hj
⊢ blsub.{u, v} (succ o) f = succ (f o ⋯)

Tactic:
bsup_succ_of_mono fun {_ _} hi hj h => succ_le_succ (hf hi hj h)

Premises used: Ordinal.bsup_succ_of_mono, Ordinal.blsub, Order.succ_le_succ
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
rw : IsEmpty.{u_3 + 1} o.ToType ↔ o = 0
⊢ blsub.{u_3, u_4} o f = 0 ↔ o = 0

Tactic:
rw [← lsub_eq_blsub, lsub_eq_zero_iff]

Premises used: Ordinal.lsub_eq_blsub, Ordinal.lsub_eq_zero_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ IsEmpty.{u_3 + 1} o.ToType ↔ o = 0

Tactic:
isEmpty_toType_iff

Premises used: Ordinal.isEmpty_toType_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ IsEmpty.{u_3 + 1} o.ToType ↔ o = 0

Tactic:
exact isEmpty_toType_iff

Premises used: Ordinal.isEmpty_toType_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : (a : Ordinal.{u_3}) → a < 0 → Ordinal.{max u_3 u_4}
rw rw₁ : Eq.{u_3 + 2} (α := Ordinal.{u_3}) 0 0
⊢ blsub.{u_3, u_4} 0 f = 0

Tactic:
rw [blsub_eq_zero_iff]

Premises used: Ordinal.blsub_eq_zero_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
ho : 0 < o
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
⊢ 0 < blsub.{u_3, u_4} o f

Tactic:
(lt_blsub f 0 ho).pos

Premises used: LT.lt.pos, Ordinal.lt_blsub, OfNat.ofNat