awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
m : ℕ
⊢ ∀ (n : ℕ),
    (↑(m ^ n) : Ordinal.{u_1}) =
      HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : 0 < o
inl : ∀ (ho₁ : 1 < o), ⨆ (n : ℕ), o ^ n = o ^ ω
inr :
  ∀ (ho : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 0 1),
    ⨆ (n : ℕ), HPow.hPow (α := Ordinal.{u_1}) 1 n = HPow.hPow (α := Ordinal.{u_1}) 1 ω
⊢ ⨆ (n : ℕ), o ^ n = o ^ ω

Tactic:
rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl

Premises used: Iff.mpr, LE.le.lt_or_eq, rfl, Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : 0 < o
ho₁ : 1 < o
⊢ ⨆ (n : ℕ), o ^ n = o ^ ω

Tactic:
simpa using apply_omega0_of_isNormal (isNormal_opow ho₁)

Premises used: Ordinal.isNormal_opow, Ordinal.apply_omega0_of_isNormal
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
ho : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
⊢ ⨆ (n : ℕ), HPow.hPow (α := Ordinal.{u_1}) 1 n = HPow.hPow (α := Ordinal.{u_1}) 1 ω

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
m n : ℕ
obtain : ∀ (hm : m ≤ 1), (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
inr : ∀ (hm : 1 < m), (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})

Tactic:
obtain hm | hm := le_or_gt m 1

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
m n : ℕ
hm : m ≤ 1
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ : (↑0 : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})

Tactic:
rw_mod_cast [Nat.log_of_left_le_one hm, log_of_left_le_one (mod_cast hm)]

Premises used: Ordinal.log_of_left_le_one, Nat.log_of_left_le_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
m n : ℕ
hm : m ≤ 1
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})

Tactic:
case inl => rw_mod_cast [Nat.log_of_left_le_one hm, log_of_left_le_one (mod_cast hm)]

Premises used: Ordinal.log_of_left_le_one, Nat.log_of_left_le_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
m n : ℕ
hm : 1 < m
obtain : (↑(Nat.log m 0) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑0 : Ordinal.{u_1})
inr : ∀ (hn : n ≠ 0), (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
m : ℕ
hm : 1 < m
⊢ (↑(Nat.log m 0) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑0 : Ordinal.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
m : ℕ
hm : 1 < m
⊢ (↑(Nat.log m 0) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑0 : Ordinal.{u_1})

Tactic:
case inl => simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
m n : ℕ
hm : 1 < m
hn : n ≠ 0
inr inr₁ inr₂ inr₃ inr₄ inr₅ : (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
inr₆ : log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1}) = (↑(Nat.log m n) : Ordinal.{u_1})
inr₇ :
  HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (↑m : Ordinal.{u_1}) (↑(Nat.log m n) : Ordinal.{u_1}) ≤
      (↑n : Ordinal.{u_1}) ∧
    (↑n : Ordinal.{u_1}) <
      HPow.hPow (α := Ordinal.{u_1}) (↑m : Ordinal.{u_1})
        (HAdd.hAdd (α := Ordinal.{u_1}) (↑(Nat.log m n) : Ordinal.{u_1}) 1)
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})

Tactic:
rw_mod_cast [eq_comm, log_eq_iff (mod_cast hm) (mod_cast hn), ← Nat.log_eq_iff (.inr ⟨hm, hn⟩)]

Premises used: Nat.log_eq_iff, eq_comm, Ordinal.log_eq_iff, And.intro, Or.inr
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : ι
rw : ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : ι) → Ordinal.{u}) i < type r
⊢ ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : ι) → Ordinal.{u}) i < o

Tactic:
rw [← ho]
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : ι
⊢ ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : ι) → Ordinal.{u}) i < type r

Tactic:
typein_lt_type r i

Premises used: Ordinal.typein_lt_type
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : ι
⊢ ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : ι) → Ordinal.{u}) i < type r

Tactic:
exact typein_lt_type r i

Premises used: Ordinal.typein_lt_type
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u_3
r : ι → ι → Prop
inst : IsWellOrder ι r
f : ι → α
i : ι
⊢ bfamilyOfFamily' r f
      (((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u_3}) ↦ x1 < x2) : (a : ι) → Ordinal.{u_3}) i)
      ⋯ =
    f i

Tactic:
simp only [bfamilyOfFamily', enum_typein]

Premises used: Ordinal.bfamilyOfFamily', Ordinal.enum_typein
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u_3
f : ι → α
i : ι
⊢ bfamilyOfFamily f
      ((PrincipalSeg.toRelEmbedding (r := WellOrderingRel) (s := fun (x1 x2 : Ordinal.{u_3}) ↦ x1 < x2)
            (typein WellOrderingRel) :
          (a : ι) → Ordinal.{u_3})
        i)
      ⋯ =
    f i

Tactic:
bfamilyOfFamily'_typein _ f i

Premises used: Ordinal.bfamilyOfFamily, Ordinal.bfamilyOfFamily'_typein
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
rwa rwa₁ rwa₂ rwa₃ : i ∈ Iio o
⊢ i ∈ Iio (type r)

Tactic:
rwa [ho]
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ familyOfBFamily' r ho f
      ((enum r : (a : (↑(Iio (type r)) : Type (u + 1))) → ι)
        (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio (type r)) i ⋯)) =
    f i hi

Tactic:
simp only [familyOfBFamily', typein_enum]

Premises used: Ordinal.typein_enum, Ordinal.familyOfBFamily'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → α
i : Ordinal.{u_3}
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_3 + 1))) → o.ToType)
        (Subtype.mk (p := fun (x : Ordinal.{u_3}) ↦ x ∈ Iio (type fun (x1 x2 : o.ToType) ↦ x1 < x2)) i ⋯)) =
    f i hi

Tactic:
familyOfBFamily'_enum _ (type_toType o) f _ _

Premises used: Ordinal.familyOfBFamily, Ordinal.familyOfBFamily'_enum, Ordinal.type_toType
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → α
a : α
⊢ a ∈ o.brange f ↔ ∃ (i : Ordinal.{u_3}) (hi : i < o), f i hi = a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Ordinal.brange, setOf
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → α
i : Ordinal.{u_3}
hi : i < o
⊢ f i hi ∈ o.brange f

Tactic:
⟨i, hi, rfl⟩

Premises used: Set.Mem, Ordinal.brange, setOf, Exists.intro, rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
⊢ range (familyOfBFamily' r ho f) = o.brange f

Tactic:
Set.ext fun a => ⟨?_, ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
refine_1 : ∀ a ∈ range (familyOfBFamily' r ho f), a ∈ o.brange f
refine_2 : ∀ a ∈ o.brange f, a ∈ range (familyOfBFamily' r ho f)
⊢ range (familyOfBFamily' r ho f) = o.brange f

Tactic:
refine Set.ext fun a => ⟨?_, ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
b : ι
⊢ familyOfBFamily' r ho f b ∈ o.brange f

Tactic:
apply mem_brange_self

Premises used: Ordinal.mem_brange_self
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ f i hi ∈ range (familyOfBFamily' r ho f)

Tactic:
⟨_, familyOfBFamily'_enum _ _ _ _ _⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, Ordinal.familyOfBFamily'_enum
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ f i hi ∈ range (familyOfBFamily' r ho f)

Tactic:
exact ⟨_, familyOfBFamily'_enum _ _ _ _ _⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → α
⊢ range (o.familyOfBFamily f) = o.brange f

Tactic:
range_familyOfBFamily' _ _ f

Premises used: Ordinal.familyOfBFamily, Ordinal.range_familyOfBFamily'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
f : ι → α
⊢ (type r).brange (bfamilyOfFamily' r f) = range f

Tactic:
Set.ext fun a => ⟨?_, ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
f : ι → α
refine_1 : ∀ a ∈ (type r).brange (bfamilyOfFamily' r f), a ∈ range f
refine_2 : ∀ a ∈ range f, a ∈ (type r).brange (bfamilyOfFamily' r f)
⊢ (type r).brange (bfamilyOfFamily' r f) = range f

Tactic:
refine Set.ext fun a => ⟨?_, ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
f : ι → α
i : Ordinal.{u}
hi : i < type r
⊢ bfamilyOfFamily' r f i hi ∈ range f

Tactic:
apply mem_range_self

Premises used: Set.mem_range_self
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
f : ι → α
b : ι
⊢ f b ∈ (type r).brange (bfamilyOfFamily' r f)

Tactic:
⟨_, _, bfamilyOfFamily'_typein _ _ _⟩

Premises used: Set.Mem, Ordinal.bfamilyOfFamily'_typein, Ordinal.brange, setOf, Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
f : ι → α
b : ι
⊢ f b ∈ (type r).brange (bfamilyOfFamily' r f)

Tactic:
exact ⟨_, _, bfamilyOfFamily'_typein _ _ _⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
ι : Type u
f : ι → α
⊢ (type (α := ι) WellOrderingRel).brange (bfamilyOfFamily f) = range f

Tactic:
brange_bfamilyOfFamily' _ _

Premises used: Ordinal.bfamilyOfFamily, Ordinal.brange_bfamilyOfFamily'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
o : Ordinal.{u_3}
ho : o ≠ 0
c : α
rw : Eq (α := Set α) (range (o.familyOfBFamily fun (x : Ordinal.{u_3}) (x_1 : x < o) ↦ c)) {c}
⊢ Eq (α := Set α) (o.brange fun (x : Ordinal.{u_3}) (x_1 : x < o) ↦ c) {c}

Tactic:
rw [← range_familyOfBFamily]

Premises used: Ordinal.range_familyOfBFamily
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
o : Ordinal.{u_3}
ho : o ≠ 0
c : α
⊢ Eq (α := Set α) (range (o.familyOfBFamily fun (x : Ordinal.{u_3}) (x_1 : x < o) ↦ c)) {c}

Tactic:
@Set.range_const _ o.ToType (nonempty_toType_iff.2 ho) c

Premises used: Ordinal.familyOfBFamily, Ordinal.familyOfBFamily', Set.range_const
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
o : Ordinal.{u_3}
ho : o ≠ 0
c : α
⊢ Eq (α := Set α) (range (o.familyOfBFamily fun (x : Ordinal.{u_3}) (x_1 : x < o) ↦ c)) {c}

Tactic:
exact @Set.range_const _ o.ToType (nonempty_toType_iff.2 ho) c

Premises used: Set.range_const
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
f : ι → α
g : α → β
⊢ Eq (α := (i : Ordinal.{u}) → (hi : i < type r) → β)
    (fun (i : Ordinal.{u}) (hi : i < type r) ↦ g (bfamilyOfFamily' r f i hi)) (bfamilyOfFamily' r (g ∘ f))

Tactic:
rfl

Premises used: Ordinal.bfamilyOfFamily', rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
β : Type u_2
ι : Type u
f : ι → α
g : α → β
⊢ (fun (i : Ordinal.{u}) (hi : i < type (α := ι) WellOrderingRel) ↦ g (bfamilyOfFamily f i hi)) =
    bfamilyOfFamily (g ∘ f)

Tactic:
rfl

Premises used: Ordinal.bfamilyOfFamily', Ordinal.bfamilyOfFamily, rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
g : α → β
⊢ g ∘ familyOfBFamily' r ho f = familyOfBFamily' r ho fun (i : Ordinal.{u}) (hi : i < o) ↦ g (f i hi)

Tactic:
rfl

Premises used: Ordinal.familyOfBFamily', rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
α : Type u_1
β : Type u_2
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → α
g : α → β
⊢ g ∘ o.familyOfBFamily f = o.familyOfBFamily fun (i : Ordinal.{u_3}) (hi : i < o) ↦ g (f i hi)

Tactic:
rfl

Premises used: Ordinal.familyOfBFamily, Ordinal.familyOfBFamily', rfl
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
inst : Small.{u, u + 1} (↑s : Type (u + 1))
obtain : ∀ (a : Cardinal.{u}) (ha : a ∈ upperBounds (succ ∘ card '' s)), BddAbove s
⊢ BddAbove s

Tactic:
obtain ⟨a, ha⟩ := Cardinal.bddAbove_of_small (s := (succ ∘ card) '' s)

Premises used: Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
inst : Small.{u, u + 1} (↑s : Type (u + 1))
a : Cardinal.{u}
ha : a ∈ upperBounds (succ ∘ card '' s)
⊢ BddAbove s

Tactic:
⟨a.ord, fun b hb ↦ le_of_lt ?_⟩

Premises used: le_of_lt, BddAbove, Cardinal.ord, Set.Nonempty, Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
inst : Small.{u, u + 1} (↑s : Type (u + 1))
a : Cardinal.{u}
ha : a ∈ upperBounds (succ ∘ card '' s)
refine : ∀ (b : Ordinal.{u}) (hb : b ∈ s), b < a.ord
⊢ BddAbove s

Tactic:
refine ⟨a.ord, fun b hb ↦ le_of_lt ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
inst : Small.{u, u + 1} (↑s : Type (u + 1))
a : Cardinal.{u}
ha : a ∈ upperBounds (succ ∘ card '' s)
b : Ordinal.{u}
hb : b ∈ s
⊢ b < a.ord

Tactic:
simpa [lt_ord] using ha (mem_image_of_mem _ hb)

Premises used: Set.mem_image_of_mem, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ BddAbove (range f)

Tactic:
bddAbove_of_small

Premises used: Ordinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
⊢ BddAbove s ↔ Small.{u, u + 1} (↑s : Type (u + 1))

Tactic:
⟨fun ⟨a, h⟩ ↦ small_subset (s := Iic a) fun _ hx ↦ h hx, fun _ ↦ bddAbove_of_small⟩

Premises used: Set.Elem, Ordinal.bddAbove_of_small, _private.0.Ordinal.bddAbove_iff_small.match_1, small_subset, Iff.intro, Small
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
hf : BddAbove s
f : Ordinal.{u} → Ordinal.{max u v}
rw :
  ∀ (hf : Small.{u, u + 1} (↑s : Type (u + 1))) (f : Ordinal.{u} → Ordinal.{max u v}),
    Small.{max u v, (max u v) + 1} (↑(f '' s) : Type ((max u v) + 1))
⊢ BddAbove (f '' s)

Tactic:
rw [bddAbove_iff_small] at hf ⊢

Premises used: Ordinal.bddAbove_iff_small
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
hf : Small.{u, u + 1} (↑s : Type (u + 1))
f : Ordinal.{u} → Ordinal.{max u v}
⊢ Small.{max u v, (max u v) + 1} (↑(f '' s) : Type ((max u v) + 1))

Tactic:
small_lift _

Premises used: small_lift
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
s : Set Ordinal.{u}
hf : Small.{u, u + 1} (↑s : Type (u + 1))
f : Ordinal.{u} → Ordinal.{max u v}
⊢ Small.{max u v, (max u v) + 1} (↑(f '' s) : Type ((max u v) + 1))

Tactic:
exact small_lift _

Premises used: small_lift
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
g : Ordinal.{v} → Ordinal.{max v w}
rw : BddAbove (g '' range f)
⊢ BddAbove (range (g ∘ f))

Tactic:
rw [range_comp]

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

Tactic:
bddAbove_image hf g

Premises used: Ordinal.bddAbove_image
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
g : Ordinal.{v} → Ordinal.{max v w}
⊢ BddAbove (g '' range f)

Tactic:
exact bddAbove_image hf g

Premises used: Ordinal.bddAbove_image
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
⊢ ∀ (i : ι), f i ≤ ⨆ (i : ι), f i

Tactic:
le_ciSup bddAbove_of_small

Premises used: Ordinal.bddAbove_of_small, le_ciSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
a : Ordinal.{u}
inst : Small.{u, u_3} ι
⊢ ⨆ (i : ι), f i ≤ a ↔ ∀ (i : ι), f i ≤ a

Tactic:
ciSup_le_iff' bddAbove_of_small

Premises used: ciSup_le_iff', Ordinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Sort u_3
f : ι → Ordinal.{u_4}
a : Ordinal.{u_4}
⊢ (∀ (i : ι), f i ≤ a) → ⨆ (i : ι), f i ≤ a

Tactic:
ciSup_le'

Premises used: ciSup_le'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
a : Ordinal.{u}
inst : Small.{u, u_3} ι
⊢ a < ⨆ (i : ι), f i ↔ ∃ (i : ι), a < f i

Tactic:
lt_ciSup_iff' bddAbove_of_small

Premises used: Ordinal.bddAbove_of_small, lt_ciSup_iff'
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
i : ι
rw : f i + 1 ≤ ⨆ (i : ι), f i + 1
⊢ f i < ⨆ (i : ι), f i + 1

Tactic:
rw [← add_one_le_iff]

Premises used: Order.add_one_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
i : ι
⊢ f i + 1 ≤ ⨆ (i : ι), f i + 1

Tactic:
apply Ordinal.le_iSup

Premises used: Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
a : Ordinal.{u}
inst : Small.{u, u_3} ι
⊢ ⨆ (i : ι), f i + 1 ≤ a ↔ ∀ (i : ι), f i < a

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Sort u_3
f : ι → Ordinal.{u}
a : Ordinal.{u}
h : ∀ (i : ι), f i < a
⊢ ∀ (i : ι), f i + 1 ≤ a

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
a : Ordinal.{u}
inst : Small.{u, u_3} ι
⊢ a < ⨆ (i : ι), f i + 1 ↔ ∃ (i : ι), a ≤ f i

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
hf : ∀ (i : ι), f i ≠ iSup f
a : Ordinal.{u}
hao : a < iSup f
by_contra! : ∀ (hoa : iSup f ≤ succ a), False
⊢ succ a < iSup f

Tactic:
by_contra! hoa
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
hf : ∀ (i : ι), f i ≠ iSup f
a : Ordinal.{u}
hao : a < iSup f
hoa : iSup f ≤ succ a
⊢ False

Tactic:
hao.not_ge (Ordinal.iSup_le fun i ↦ le_of_lt_succ <|
    ((Ordinal.le_iSup _ _).lt_of_ne (hf i)).trans_le hoa)

Premises used: Ordinal.iSup_le, LE.le.lt_of_ne, Ordinal.le_iSup, LT.lt.trans_le, LT.lt.not_ge, Order.le_of_lt_succ
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
hf : ∀ (i : ι), f i ≠ iSup f
a : Ordinal.{u}
hao : a < iSup f
hoa : iSup f ≤ succ a
⊢ False

Tactic:
exact hao.not_ge (Ordinal.iSup_le fun i ↦ le_of_lt_succ <|
    ((Ordinal.le_iSup _ _).lt_of_ne (hf i)).trans_le hoa)

Premises used: Ordinal.iSup_le, LE.le.lt_of_ne, Ordinal.le_iSup, LT.lt.trans_le, LT.lt.not_ge, Order.le_of_lt_succ
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
⊢ iSup f = 0 ↔ ∀ (i : ι), f i = 0

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

Premises used: Iff.mpr, zero_le, Ordinal.iSup_le, le_antisymm, Iff.intro, nonpos_iff_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
h : ∀ (h : iSup f = 0) (i : ι), f i = 0
⊢ iSup f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
refine
    ⟨fun h i => ?_, fun h =>
      le_antisymm (Ordinal.iSup_le fun i => nonpos_iff_eq_zero.2 (h i)) zero_le⟩
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
h : iSup f = 0
i : ι
rw : f i ≤ iSup f
⊢ f i = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← h]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
h : iSup f = 0
i : ι
⊢ f i ≤ iSup f

Tactic:
Ordinal.le_iSup f i

Premises used: Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
h : iSup f = 0
i : ι
⊢ f i ≤ iSup f

Tactic:
exact Ordinal.le_iSup f i

Premises used: Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.Family
Goal:
ι : Sort u_3
ι' : Sort u_4
f : ι → Ordinal.{u_5}
g : ι' → Ordinal.{u_5}
h : range f = range g
⊢ iSup f = iSup g

Tactic:
congr_arg _ h

Premises used: iSup, congr_arg
-- 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 : ∀ (i : α ⊕ β), f i ≤ max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))
apply₁ : LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (a : α), f (Sum.inl a)) (⨆ (i : α ⊕ β), f i)
apply₂ : LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (b : β), f (Sum.inr b)) (⨆ (i : α ⊕ β), f i)
⊢ iSup f = max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))

Tactic:
apply (Ordinal.iSup_le _).antisymm (max_le _ _)

Premises used: Ordinal.iSup_le, LE.le.antisymm, max_le
-- 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} β
i : α
⊢ f (Sum.inl i) ≤ max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))

Tactic:
le_max_of_le_left (Ordinal.le_iSup (fun x ↦ f (Sum.inl x)) i)

Premises used: Sum.inl, Ordinal.le_iSup, le_max_of_le_left
-- 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} β
i : α
⊢ f (Sum.inl i) ≤ max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))

Tactic:
exact le_max_of_le_left (Ordinal.le_iSup (fun x ↦ f (Sum.inl x)) i)

Premises used: Sum.inl, Ordinal.le_iSup, le_max_of_le_left
-- 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} β
i : β
⊢ f (Sum.inr i) ≤ max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))

Tactic:
le_max_of_le_right (Ordinal.le_iSup (fun x ↦ f (Sum.inr x)) i)

Premises used: Ordinal.le_iSup, Sum.inr, le_max_of_le_right
-- 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} β
i : β
⊢ f (Sum.inr i) ≤ max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))

Tactic:
exact le_max_of_le_right (Ordinal.le_iSup (fun x ↦ f (Sum.inr x)) i)

Premises used: Ordinal.le_iSup, Sum.inr, le_max_of_le_right
-- 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 (a : α) ↦ f (Sum.inl a)) (range fun (i : α ⊕ β) ↦ f i)
⊢ LE.le.{u + 1} (α := Ordinal.{u}) (⨆ (a : α), f (Sum.inl a)) (⨆ (i : α ⊕ β), f i)

Tactic:
apply csSup_le_csSup' bddAbove_of_small

Premises used: csSup_le_csSup', Ordinal.bddAbove_of_small