mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → Ordinal.{max u_3 u_4}
⊢ (type r).bsup (bfamilyOfFamily' r f) = iSup f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ 0 ∈ Iio (typeLT ToType 1)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ (type r).bsup (bfamilyOfFamily' r f) = (type r').bsup (bfamilyOfFamily' r' f)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ o₁.bsup f = o₂.bsup fun a h ↦ f a ⋯

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
hb : b ∈ s
⊢ ∃ a, enumOrd s a = b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: 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
⊢ f i hi ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.bsup f ↔ ∃ i, ∃ (hi : i < o), a < f i hi

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : b = b'
⊢ r a' a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ a = (enum fun x1 x2 ↦ x1 < x2) ⟨0, uniqueToTypeOne._proof_2⟩

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : ToType 1
⊢ 0 ∈ Iio (typeLT ToType 1)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
⊢ enumOrd t ≤ enumOrd s

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: 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
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
⊢ f ((type r).bsup g) = (type r).bsup fun a h ↦ f (g a h)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ o.bsup f
a : Ordinal.{max u v}
⊢ a < o.bsup f → succ a < o.bsup f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ o.bsup f = 0 ↔ ∀ (i : Ordinal.{u_3}) (hi : i < o), f i hi = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : ¬b = b'
⊢ s b' b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}
⊢ bsup 1 f = f 0 ⋯

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ enumOrd s = f ↔ StrictMono f ∧ range f = s

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: 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
⊢ f i hi ≤ o'.bsup g

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ ⨆ a, f ↑a ⋯ = o.bsup f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
a : Ordinal.{max u_3 u_4}
⊢ a < lsub f ↔ ∃ i, a ≤ f i

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f = lsub f ∨ succ (iSup f) = lsub f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ succ (iSup f) ≤ lsub f ↔ ∃ i, f i = iSup f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ typeLT α ∈ range succ ↔ ∃ x, IsMax x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : IsSuccLimit b
⊢ a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
⊢ IsNormal (enumOrd s)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: ⊢ enumOrd univ = id

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ IsSuccPrelimit (typeLT α) ↔ NoMaxOrder α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
⊢ ?m.88 < lsub f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: x : ToType 1
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding x = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
⊢ enumOrd s 0 = sInf s

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
x y : o.ToType
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding x ≤ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding y ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
h : 0 < a
⊢ IsNormal fun x ↦ a * x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : IsSuccLimit c
⊢ a < b * c ↔ ∃ c' < c, a < b * c'

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f = lsub f ↔ ∀ a < lsub f, succ a < lsub f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
i : ι
⊢ f i < iSup f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
a : (succ o).ToType
⊢ a ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨o, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ lsub f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Small.List

Goal state before:
pp: α : Type v
inst✝ : Small.{u, v} α
⊢ Small.{u, v} (List α)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : b ≤ 1
n : ℕ
⊢ log b n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : n < b
⊢ log b n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
⊢ fuel ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ b > 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ fuel + 1 ≤ 2 * fuel

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
⊢ n < (b * b) ^ fuel

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max v u_3}
⊢ lsub f = 0 ↔ IsEmpty ι

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit (0 * b)

pp: case inr
a b : Ordinal.{u_4}
hb : IsSuccLimit b
ha : 0 < a
⊢ IsSuccPrelimit (a * b)

Tactic:
· rw [zero_mul]
    exact isSuccPrelimit_zero

Goal state after:
case inr
a b : Ordinal.{u_4}
hb : IsSuccLimit b
ha : 0 < a
⊢ IsSuccPrelimit (a * b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : 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) ⊆ range (succ ∘ g)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
⊢ o ≤ lsub ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
ho : ∀ a < o, succ a < o
⊢ IsSuccPrelimit o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal.{u}
⊢ ∀ (a b : Type u), isEquivalent a b → ⨅ r, type ↑r = ⨅ r, type ↑r

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u_1
⊢ ∃ x, ∃ (x_1 : WellFoundedLT α), (#α).ord = typeLT α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
⊢ IsSuccLimit (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
ho : ∀ a < o, succ a < o
⊢ iSup ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding = o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
⊢ iSup ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding = o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ 0 • a = a * ↑0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ lsub (familyOfBFamily' r ho f) = lsub (familyOfBFamily' r' ho' f)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
a : Ordinal.{u_4}
⊢ (n + 1) • a = a * ↑(n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ (type r).blsub (bfamilyOfFamily' r f) = (type r').blsub (bfamilyOfFamily' r' f)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ o₁.blsub f = o₂.blsub fun a h ↦ f a ⋯

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: ⊢ GaloisConnection ord card

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ o.blsub f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
⊢ o.card ≤ c ↔ o < (succ c).ord

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.blsub f ↔ ∃ i, ∃ (hi : i < o), a ≤ f i hi

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: n : ℕ
IH : ↑n ≤ (↑n).ord
⊢ (↑n).ord < (↑(n + 1)).ord

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: n : ℕ
⊢ (↑n).ord = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: ⊢ ord 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ (a + b) * c' ≤ a * c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.bsup f = o.blsub f ∨ succ (o.bsup f) = o.blsub f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n fuel : ℕ
hb : 1 < b
hn : n ≠ 0
hfuel : n < b ^ fuel
⊢ (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
⊢ a * c ≤ (a + b) * c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: ⊢ ∀ {a : Cardinal.{u_1}}, IsSuccLimit a → a.ord ∈ lowerBounds (upperBounds (ord '' Iio a))

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: ⊢ ℵ₀.ord = ω

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ succ (o.bsup f) ≤ o.blsub f ↔ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.bsup f = o.blsub f ↔ ∀ a < o.blsub f, succ a < o.blsub f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: c : Cardinal.{v}
⊢ Ordinal.lift.{u, v} c.ord = (lift.{u, v} c).ord

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
⊢ (a + b) * (c + 1) = a * (c + 1) + b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ #c.ord.ToType = c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o * 2 = o + o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a / 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ 0 ∈ (fun x ↦ a * x) ⁻¹' Iic c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
⊢ log b y < x ↔ y < b ^ x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ ((typein r).toRelEmbedding x).card < #α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * succ (a / b)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
i : c.ord.ToType
⊢ #↑(Iio i) < c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * (a / b) + b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : o.bsup f = o.blsub f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < o.bsup f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
⊢ 0 < a.ord ↔ 0 < a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
⊢ ω ≤ a.ord ↔ ℵ₀ ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
b0 : b ≠ 0
⊢ a / b ≤ c ↔ a < b * succ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
⊢ a.ord ≤ ω ↔ a ≤ ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl.inl
b : ℕ
hb : 1 < b
⊢ log b 0 = 0 ↔ 0 < b ∨ b ≤ 1

pp: case inl.inr
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

Tactic:
· grind [log_of_lt]

Goal state after:
case inl.inr
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
h : c ≠ 0
⊢ Nonempty c.ord.ToType

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : c ≠ 0
⊢ a < b / c ↔ c * succ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑n ≤ o.card ↔ ↑n ≤ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: b c : Ordinal.{u_4}
h : c ≠ 0
⊢ 0 < b / c ↔ c ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 1 ≤ o.card ↔ 1 ≤ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: 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) ⋯
⊢ o.bsup f = o.blsub f

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.card ↔ ω ≤ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : a ≤ b * c
⊢ a / b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : b = 0
⊢ b * (a / b) ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑n < o.card ↔ ↑n < o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ o.blsub f = 0 ↔ o = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 < o.card ↔ 0 < o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 1 < o.card ↔ 1 < o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.card ≤ 1 ↔ o ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : (a : Ordinal.{u_3}) → a < 0 → Ordinal.{max u_3 u_4}
⊢ blsub 0 f = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ o.card = ↑n ↔ o = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.card = 0 ↔ o = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.card = 1 ↔ o = 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ o ≤ c.ord ↔ o.card ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u}
b : Ordinal.{max u v}
h : b.card ≤ Cardinal.lift.{v, u} a
⊢ b ∈ range lift.{v, u}

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
⊢ a / c ≤ b / c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝¹ : IsWellOrder α r
inst✝ : Fintype α
⊢ type r = ↑(Fintype.card α)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: n : ℕ
⊢ typeLT Fin n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : 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 i) ⋯ < o
i : Ordinal.{u}
h : i < type r
⊢ f i h < o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ (#↑s).ord ≤ type r

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (type r).blsub f ≤ o ↔ (lsub fun a ↦ f ((typein r).toRelEmbedding a) ⋯) ≤ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ (#↑s).ord < type r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
⊢ n / b ≠ 0

Tactic:
by

Goal state after: