awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact h _
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a) → bsup.{u, v} o f ≤ a

Tactic:
bsup_le_iff.2

Premises used: Iff.mpr, Ordinal.bsup_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 ≤ bsup.{u_3, u_4} o f

Tactic:
bsup_le_iff.1 le_rfl _ _

Premises used: le_rfl, Ordinal.bsup_le_iff, Iff.mp
-- 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 < bsup.{u, v} o f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), a < f i hi

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

Premises used: not_le, Classical.not_forall
-- Module: Mathlib.SetTheory.Ordinal.Family
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
⊢ Nonempty α

Tactic:
haveI := type_ne_zero_iff_nonempty.1 h
-- Module: Mathlib.SetTheory.Ordinal.Family
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)))
ho ho₁ : type r = type r
⊢ 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)

Tactic:
rw [← iSup'_eq_bsup r, Order.IsNormal.map_iSup H bddAbove_of_small, ← iSup'_eq_bsup r]

Premises used: Ordinal.bddAbove_of_small, Ordinal.iSup'_eq_bsup, Order.IsNormal.map_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
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 α
⊢ 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)))

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
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 α
⊢ type r = type r

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (h : i < o), f i h ≠ bsup.{u, v} o f) ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < bsup.{u, v} o f

Tactic:
⟨fun hf _ _ => lt_of_le_of_ne (le_bsup _ _ _) (hf _ _), fun hf _ _ => ne_of_lt (hf _ _)⟩

Premises used: Ordinal.le_bsup, Iff.intro, ne_of_lt, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Ordinal.Family
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}
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)
⊢ a < bsup.{u, v} o f → succ a < bsup.{u, v} o f

Tactic:
rw [← iSup_eq_bsup] at *

Premises used: Ordinal.iSup_eq_bsup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ iSup (o.familyOfBFamily f)
a : Ordinal.{max u v}
⊢ a < iSup (o.familyOfBFamily f) → succ a < iSup (o.familyOfBFamily f)

Tactic:
succ_lt_iSup_of_ne_iSup fun i => hf _

Premises used: Ordinal.familyOfBFamily, LT.lt, Ordinal.familyOfBFamily', Ordinal.type_toType, Ordinal.familyOfBFamily'._proof_1, Ordinal.succ_lt_iSup_of_ne_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ iSup (o.familyOfBFamily f)
a : Ordinal.{max u v}
⊢ a < iSup (o.familyOfBFamily f) → succ a < iSup (o.familyOfBFamily f)

Tactic:
exact succ_lt_iSup_of_ne_iSup fun i => hf _

Premises used: LT.lt, Ordinal.type_toType, Ordinal.familyOfBFamily'._proof_1, Ordinal.succ_lt_iSup_of_ne_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
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

Tactic:
⟨fun h i hi => ?_, fun h =>
      le_antisymm (bsup_le fun i hi => nonpos_iff_eq_zero.2 (h i hi)) zero_le⟩

Premises used: Iff.mpr, zero_le, Ordinal.bsup_le, le_antisymm, Iff.intro, nonpos_iff_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
h : ∀ (h : bsup.{u_3, u_4} o f = 0) (i : Ordinal.{u_3}) (hi : i < o), f i hi = 0
⊢ 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⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
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
rw : f i hi ≤ bsup.{u_3, u_4} o f
⊢ f i hi = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← h]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Family
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 ≤ bsup.{u_3, u_4} o f

Tactic:
le_bsup f i hi

Premises used: Ordinal.le_bsup
-- Module: Mathlib.SetTheory.Ordinal.Family
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 ≤ bsup.{u_3, u_4} o f

Tactic:
exact le_bsup f i hi

Premises used: Ordinal.le_bsup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
hf : ∀ {a a' : Ordinal.{u_3}} (ha : a < o) (ha' : a' < o), a < a' → f a ha < f a' ha'
ho : ∀ a < o, succ a < o
i : Ordinal.{u_3}
h : i < o
⊢ f i h < bsup.{u_3, u_4} o f

Tactic:
(hf _ _ <| lt_succ i).trans_le (le_bsup f (succ i) <| ho _ h)

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

Tactic:
le_antisymm (bsup_le fun _i hi => hf _ _ <| le_of_lt_succ hi) (le_bsup _ _ _)

Premises used: Ordinal.bsup_le, Order.lt_succ, le_antisymm, Ordinal.le_bsup, Order.le_of_lt_succ
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
f : (a : Ordinal.{u_3}) → a < 0 → Ordinal.{max u_3 u_4}
⊢ bsup.{u_3, u_4} 0 f = 0

Tactic:
bsup_eq_zero_iff.2 fun _i hi => (not_lt_zero hi).elim

Premises used: Iff.mpr, False.elim, not_lt_zero, Ordinal.bsup_eq_zero_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
o : Ordinal.{u}
ho : o ≠ 0
a : Ordinal.{max u v}
⊢ (bsup.{u, v} o fun (x : Ordinal.{u}) (x_1 : x < o) ↦ a) = a

Tactic:
le_antisymm (bsup_le fun _ _ => le_rfl) (le_bsup _ 0 (pos_iff_ne_zero.2 ho))

Premises used: Iff.mpr, le_rfl, Ordinal.bsup_le, le_antisymm, Ordinal.le_bsup, OfNat.ofNat, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Family
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 ⋯
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)
      ⋯ =
    f 0 ⋯
⊢ bsup.{u_3, u_4} 1 f = f 0 ⋯

Tactic:
simp_rw [← iSup_eq_bsup, ciSup_unique, familyOfBFamily, familyOfBFamily', typein_one_toType]

Premises used: Ordinal.iSup_eq_bsup, ciSup_unique, Ordinal.familyOfBFamily, Ordinal.familyOfBFamily', Ordinal.typein_one_toType
-- 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
i : Ordinal.{u}
hi : i < o
obtain : ∀ (j : Ordinal.{v}) (hj : j < o') (hj' : g j hj = f i hi), f i hi ≤ o'.bsup g
⊢ f i hi ≤ o'.bsup g

Tactic:
obtain ⟨j, hj, hj'⟩ := h ⟨i, hi, 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
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
rw : g j hj ≤ o'.bsup g
⊢ f i hi ≤ o'.bsup g

Tactic:
rw [← hj']
-- 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
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ g j hj ≤ o'.bsup g

Tactic:
apply le_bsup

Premises used: Ordinal.le_bsup
-- 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
⊢ o.bsup f = o'.bsup g

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

Premises used: Eq.ge, LE.le.antisymm, Eq.le, Ordinal.bsup_le_of_brange_subset
-- Module: Mathlib.SetTheory.Ordinal.Family
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)
simp_rw₂ :
  sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯) =
    sSup (range (o.familyOfBFamily f))
simp_rw₃ :
  sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯) = sSup (o.brange f)
simp_rw₄ :
  Eq (α := Ordinal.{max u_4 u_3})
    (sSup (range fun (a : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))) ↦ f (↑a : Ordinal.{u_3}) ⋯))
    (sSup {a : Ordinal.{max u_3 u_4} | ∃ (i : Ordinal.{u_3}) (hi : i < o), f i hi = a})
simp_rw₅ :
  Eq (α := Ordinal.{max u_4 u_3})
    (sSup
      {x : Ordinal.{max u_4 u_3} |
        ∃ (y : (↑{x : Ordinal.{u_3} | x < o} : Type (u_3 + 1))), f (↑y : Ordinal.{u_3}) ⋯ = x})
    (sSup {a : Ordinal.{max u_3 u_4} | ∃ (i : Ordinal.{u_3}) (hi : i < o), f i hi = a})
simp_rw₆ :
  Eq (α := Ordinal.{max u_4 u_3})
    (sSup
      {x : Ordinal.{max u_4 u_3} |
        ∃ (a : Ordinal.{u_3}) (h : Membership.mem (γ := Set Ordinal.{u_3}) {x : Ordinal.{u_3} | x < o} a), f a ⋯ = x})
    (sSup {a : Ordinal.{max u_3 u_4} | ∃ (i : Ordinal.{u_3}) (hi : i < o), f i hi = a})
⊢ ⨆ (a : (↑(Iio o) : Type (u_3 + 1))), f (↑a : Ordinal.{u_3}) ⋯ = bsup.{u_3, u_4} o f

Tactic:
simp_rw [Iio, bsup, iSup, range_familyOfBFamily, brange, range, Subtype.exists, mem_setOf]

Premises used: iSup, Ordinal.brange, Subtype.exists, Ordinal.bsup, Set.mem_setOf, Ordinal.range_familyOfBFamily, Set.range, Set.Iio
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup (succ ∘ f) = lsub.{u_3, u_4} f

Tactic:
rfl

Premises used: Ordinal.lsub, rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
a : Ordinal.{max u_3 u_4}
⊢ lsub.{u_3, u_4} f ≤ a ↔ ∀ (i : ι), f i < a

Tactic:
Ordinal.iSup_add_one_le_iff

Premises used: Order.succ, Ordinal.lsub, Ordinal.iSup_add_one_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
a : Ordinal.{max u_4 u_3}
⊢ (∀ (i : ι), f i < a) → lsub.{u_3, u_4} f ≤ a

Tactic:
lsub_le_iff.2

Premises used: Iff.mpr, Ordinal.lsub_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
i : ι
⊢ f i < lsub.{u_3, u_4} f

Tactic:
Ordinal.lt_iSup_add_one f i

Premises used: Order.succ, Ordinal.lsub, Ordinal.lt_iSup_add_one
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
a : Ordinal.{max u_3 u_4}
⊢ a < lsub.{u_3, u_4} f ↔ ∃ (i : ι), a ≤ f i

Tactic:
simpa only [not_forall, not_lt, not_le] using not_congr lsub_le_iff

Premises used: not_le, not_lt, Ordinal.lsub_le_iff, Classical.not_forall, not_congr
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f ≤ lsub.{u_3, u_4} f

Tactic:
Ordinal.iSup_le fun i => (lt_lsub f i).le

Premises used: Ordinal.iSup_le, LT.lt.le, Ordinal.lt_lsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ lsub.{u_3, u_4} f ≤ succ (iSup f)

Tactic:
lsub_le fun i => lt_succ_iff.2 (Ordinal.le_iSup f i)

Premises used: Iff.mpr, Order.lt_succ_iff, Ordinal.le_iSup, Ordinal.lsub_le
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
inl : ∀ (h : iSup f = lsub.{u_3, u_4} f), iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f
inr : ∀ (h : iSup f < lsub.{u_3, u_4} f), iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f
⊢ iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f

Tactic:
rcases eq_or_lt_of_le (iSup_le_lsub f) with h | h

Premises used: Ordinal.iSup_le_lsub, eq_or_lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub.{u_3, u_4} f
⊢ iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f

Tactic:
Or.inl h

Premises used: Or.inl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub.{u_3, u_4} f
⊢ iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f

Tactic:
exact Or.inl h

Premises used: Or.inl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f < lsub.{u_3, u_4} f
⊢ iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f

Tactic:
Or.inr ((succ_le_of_lt h).antisymm (lsub_le_succ_iSup f))

Premises used: LE.le.antisymm, Order.succ_le_of_lt, Ordinal.lsub_le_succ_iSup, Or.inr
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f < lsub.{u_3, u_4} f
⊢ iSup f = lsub.{u_3, u_4} f ∨ succ (iSup f) = lsub.{u_3, u_4} f

Tactic:
exact Or.inr ((succ_le_of_lt h).antisymm (lsub_le_succ_iSup f))

Premises used: LE.le.antisymm, Order.succ_le_of_lt, Ordinal.lsub_le_succ_iSup, Or.inr
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ succ (iSup f) ≤ lsub.{u_3, u_4} f ↔ ∃ (i : ι), f i = iSup f

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

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
refine_1 : ∀ (h : succ (iSup f) ≤ lsub.{u_3, u_4} f), ∃ (i : ι), f i = iSup f
refine_2 : (∃ (i : ι), f i = iSup f) → succ (iSup f) ≤ lsub.{u_3, u_4} f
⊢ succ (iSup f) ≤ lsub.{u_3, u_4} f ↔ ∃ (i : ι), f i = iSup f

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : succ (iSup f) ≤ lsub.{u_3, u_4} f
refine_1 : ∀ (hf : ∀ (i : ι), f i ≠ iSup f), False
⊢ ∃ (i : ι), f i = iSup f

Tactic:
by_contra! hf
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : succ (iSup f) ≤ lsub.{u_3, u_4} f
hf : ∀ (i : ι), f i ≠ iSup f
⊢ (∀ (a : ι), f a ≠ ⨆ (i : ι), f i) ↔ ∀ (a : ι), f a < ⨆ (i : ι), f i

Tactic:
have := forall_congr' fun i ↦ (Ordinal.le_iSup f i).lt_iff_ne.symm
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : succ (iSup f) ≤ lsub.{u_3, u_4} f
hf : ∀ (i : ι), f i ≠ iSup f
this : (∀ (a : ι), f a ≠ ⨆ (i : ι), f i) ↔ ∀ (a : ι), f a < ⨆ (i : ι), f i
⊢ False

Tactic:
(succ_le_iff.1 h).ne ((iSup_le_lsub f).antisymm (lsub_le (this.1 hf)))

Premises used: Ordinal.iSup_le_lsub, LE.le.antisymm, Order.succ_le_iff, Iff.mp, Ordinal.lsub_le, LT.lt.ne
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : succ (iSup f) ≤ lsub.{u_3, u_4} f
hf : ∀ (i : ι), f i ≠ iSup f
this : (∀ (a : ι), f a ≠ ⨆ (i : ι), f i) ↔ ∀ (a : ι), f a < ⨆ (i : ι), f i
⊢ False

Tactic:
exact (succ_le_iff.1 h).ne ((iSup_le_lsub f).antisymm (lsub_le (this.1 hf)))

Premises used: Ordinal.iSup_le_lsub, LE.le.antisymm, Order.succ_le_iff, Iff.mp, Ordinal.lsub_le, LT.lt.ne
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w : ι
hf : f w = iSup f
refine_2 : f w < lsub.{u_3, u_4} f
⊢ succ (iSup f) ≤ lsub.{u_3, u_4} f

Tactic:
rw [succ_le_iff, ← hf]

Premises used: Order.succ_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w : ι
hf : f w = iSup f
⊢ f w < lsub.{u_3, u_4} f

Tactic:
lt_lsub _ _

Premises used: Ordinal.lt_lsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w : ι
hf : f w = iSup f
⊢ f w < lsub.{u_3, u_4} f

Tactic:
exact lt_lsub _ _

Premises used: Ordinal.lt_lsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ succ (iSup f) = lsub.{u_3, u_4} f ↔ ∃ (i : ι), f i = iSup f

Tactic:
(lsub_le_succ_iSup f).ge_iff_eq'.symm.trans (succ_iSup_le_lsub_iff f)

Premises used: LE.le.ge_iff_eq', Ordinal.lsub_le_succ_iSup, Iff.trans, Iff.symm, Ordinal.succ_iSup_le_lsub_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f = lsub.{u_3, u_4} f ↔ ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f

Tactic:
⟨fun h => ?_, fun hf => le_antisymm (iSup_le_lsub f) (lsub_le fun i => ?_)⟩

Premises used: Ordinal.iSup_le_lsub, le_antisymm, Iff.intro, Ordinal.lsub_le
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
refine_1 : ∀ (h : iSup f = lsub.{u_3, u_4} f), ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
refine_2 : ∀ (hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f) (i : ι), f i < iSup f
⊢ iSup f = lsub.{u_3, u_4} f ↔ ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f

Tactic:
refine ⟨fun h => ?_, fun hf => le_antisymm (iSup_le_lsub f) (lsub_le fun i => ?_)⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub.{u_3, u_4} f
refine_1 : ∀ a < iSup f, succ a < iSup f
⊢ ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f

Tactic:
rw [← h]
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub.{u_3, u_4} f
⊢ ∀ a < iSup f, succ a < iSup f

Tactic:
fun a => succ_lt_iSup_of_ne_iSup fun i => (lsub_le_iff.1 (le_of_eq h.symm) i).ne

Premises used: Ordinal.lsub_le_iff, Iff.mp, le_of_eq, Eq.symm, LT.lt.ne, Ordinal.succ_lt_iSup_of_ne_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub.{u_3, u_4} f
⊢ ∀ a < iSup f, succ a < iSup f

Tactic:
exact fun a => succ_lt_iSup_of_ne_iSup fun i => (lsub_le_iff.1 (le_of_eq h.symm) i).ne

Premises used: Ordinal.lsub_le_iff, Iff.mp, le_of_eq, Eq.symm, LT.lt.ne, Ordinal.succ_lt_iSup_of_ne_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
refine_2 : ∀ (hle : iSup f ≤ f i), False
⊢ f i < iSup f

Tactic:
by_contra! hle
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
⊢ succ (iSup f) = lsub.{u_3, u_4} f

Tactic:
have heq := (succ_iSup_eq_lsub_iff f).2 ⟨i, le_antisymm (Ordinal.le_iSup _ _) hle⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub.{u_3, u_4} f
rw : iSup f < succ (iSup f)
⊢ iSup f < lsub.{u_3, u_4} f

Tactic:
rw [← heq]
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub.{u_3, u_4} f
⊢ iSup f < succ (iSup f)

Tactic:
lt_succ (iSup f)

Premises used: iSup, Order.lt_succ
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub.{u_3, u_4} f
⊢ iSup f < succ (iSup f)

Tactic:
exact lt_succ (iSup f)

Premises used: iSup, Order.lt_succ
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub.{u_3, u_4} f
⊢ succ (iSup f) < lsub.{u_3, u_4} f

Tactic:
have :=
    hf _
      (by
        rw [← heq]
        exact lt_succ (iSup f))
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub.{u_3, u_4} f
this : succ (iSup f) < lsub.{u_3, u_4} f
⊢ lsub.{u_3, u_4} f < lsub.{u_3, u_4} f

Tactic:
rw [heq] at this
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub.{u_3, u_4} f
this : lsub.{u_3, u_4} f < lsub.{u_3, u_4} f
⊢ False

Tactic:
this.false

Premises used: LT.lt.false
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub.{u_3, u_4} f, succ a < lsub.{u_3, u_4} f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub.{u_3, u_4} f
this : lsub.{u_3, u_4} f < lsub.{u_3, u_4} f
⊢ False

Tactic:
exact this.false

Premises used: LT.lt.false
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub.{u_3, u_4} f
i : ι
rw : f i < lsub.{u_3, u_4} f
⊢ f i < iSup f

Tactic:
rw [h]
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub.{u_3, u_4} f
i : ι
⊢ f i < lsub.{u_3, u_4} f

Tactic:
apply lt_lsub

Premises used: Ordinal.lt_lsub
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
rw : ∀ (i : ι), f i < 0
⊢ lsub.{u_3, u_4} f = 0

Tactic:
rw [← nonpos_iff_eq_zero, lsub_le_iff]

Premises used: Ordinal.lsub_le_iff, nonpos_iff_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ ∀ (i : ι), f i < 0

Tactic:
h.elim

Premises used: IsEmpty.elim
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ ∀ (i : ι), f i < 0

Tactic:
exact h.elim