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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ ¬r ((enum r) ⟨(#↑s).ord, ⋯⟩) (⋯.min sᶜ h)

Tactic:
by

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

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

Tactic:
by

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

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

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.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
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha ↦ succ (f a ha)
b : Ordinal.{u}
hb : b < o
hb' : (fun a ha ↦ succ (f a ha)) b hb = a
⊢ a ∈ o'.brange fun a ha ↦ succ (g a ha)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o

Tactic:
by

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

Goal state before:
pp: b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ log b n = log b (n / b) + 1

Tactic:
by

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

Goal state before:
pp: b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
⊢ b ^ x ≤ y

Tactic:
by

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

Goal state before:
pp: b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
⊢ x ≤ log b y

Tactic:
by

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

Goal state before:
pp: a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
⊢ (a * b + c) / (a * d) = b / d

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

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}
⊢ a * b / (a * c) = b / c

Tactic:
by

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

Goal state before:
pp: b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
⊢ log b y < x

Tactic:
by

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

Goal state before:
pp: b x : ℕ
hx : x = 0
⊢ log b x ≤ x

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
⊢ a / b = c

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)

Tactic:
by

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

Goal state before:
pp: o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
⊢ (o'.bsup fun a ha ↦ f (g a ha) ⋯) = o.bsup f

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a / b = 1 ↔ b ≤ a ∧ a < b * 2

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
l m : List α
o : Ordinal.{u}
hl : l.SortedGT
hm : m.SortedGT
hmltl : m < l
hlt : ∀ i ∈ l, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
⊢ ∀ i ∈ m, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
by
  rw [← IsNormal.bsup_eq.{u, v} H h, bsup_eq_blsub_of_lt_succ_limit h]
  exact fun a _ => H.strictMono (lt_succ a)

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

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

Tactic:
by

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

Goal state before:
pp: b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ 0 ^ a ≤ 1

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ 0 ^ a = 0

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ a ^ 0 = 1

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a → IsSuccLimit (a + b)

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ^ (b + 1) = a ^ b * a

Tactic:
by

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

Goal state before:
pp: case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b ^ (0 + 1)
⊢ log b n = 0

Tactic:
rw [Nat.pow_one] at h₂

Goal state after:
case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b
⊢ log b n = 0
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
x✝ : (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)
h₂ : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
a✝ : Ordinal.{u}
ho : IsSuccLimit a✝
⊢ IsLUB (f '' Iio a✝) (f a✝)

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ IsSuccLimit (a + b) ↔ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a

Tactic:
by

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

Goal state before:
pp: b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
⊢ log b n = m

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccLimit b
⊢ a ^ b = ⨆ x, a ^ ↑x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit (a + b) ↔ IsSuccPrelimit b

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
⊢ a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : IsSuccLimit c
⊢ a < b ^ c ↔ ∃ c' < c, a < b ^ c'

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ a ^ 1 = a

Tactic:
by

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

Goal state before:
pp: a c b : Ordinal.{u_4}
x✝ : a ∣ a * b + c
d : Ordinal.{u_4}
e : a * b + c = a * d
⊢ c = a * (d - b)

Tactic:
by

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b (n * b) = log b n + 1

Tactic:
by

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

Goal state before:
pp: b : ℕ
⊢ b ^ log b 0 ≤ 0 + 1

Tactic:
by

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

Goal state before:
pp: a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * b + c

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
H : ∀ b' < b, 1 ^ b' ≤ c
⊢ 1 ≤ c

Tactic:
by

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

Goal state before:
pp: b : ℕ
⊢ Monotone (log b)

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : a * b ≠ 0
h : b = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : b ≠ 0
h : a ∣ b
⊢ a ≤ b

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
h₁ : a ∣ b
h₂ : b ∣ a
a0 : a = 0
⊢ a = b

Tactic:
by

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

Goal state before:
pp: b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
H : 1 ≤ c
b' : Ordinal.{u_1}
h : b' < b
⊢ 1 ^ b' ≤ c

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
h₁ : a ∣ b
h₂ : b ∣ a
a0 : ¬a = 0
b0 : b = 0
⊢ a = b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ 1 ^ a = 1

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < a ^ 0

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : a < b
⊢ a % b = a

Tactic:
by

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

Goal state before:
pp: b : Ordinal.{u_4}
⊢ 0 % b = 0

Tactic:
by

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n < log b (n + 1) ↔ b ^ log b (n + 1) = n + 1

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a % b < b

Tactic:
by

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ b ^ log b (n + 1) ≠ n + 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < a ^ b

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_4}
H : b ∣ a
⊢ a % b = 0

Tactic:
by

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

Goal state before:
pp: b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b n ≤ log c n

Tactic:
by

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

Goal state before:
pp: b c m n : ℕ
hc : 1 < c
hb : c ≤ b
hmn : m ≤ n
⊢ log c m ≤ log c n

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
⊢ IsNormal f ↔
    (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
by

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

Goal state before:
pp: x y z : Ordinal.{u_4}
⊢ (x * y + z) % x = z % x

Tactic:
by

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

Goal state before:
pp: x y : Ordinal.{u_4}
⊢ x * y % x = 0

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{u_1}
n : ℕ
⊢ a ^ ↑n = a ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → Ordinal.{u}
⊢ ¬Surjective f

Tactic:
by

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

Goal state before:
pp: b n : ℕ
⊢ log b (n / b) = log b n - 1

Tactic:
by

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

Goal state before:
pp: a : Ordinal.{u_1}
h : 1 < a
⊢ IsNormal fun x ↦ a ^ x

Tactic:
by

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

Goal state before:
pp: w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ (x * y + w) % (x * z) = x * (y % z) + w

Tactic:
by

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ ¬BddAbove sᶜ

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{v}
hf : IsNormal f
⊢ ⨆ n, f ↑n = f ω

Tactic:
by

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

Goal state before:
pp: x y z : Ordinal.{u_4}
⊢ x * y % (x * z) = x * (y % z)

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ 1 < a ^ b ↔ 1 < a ∧ b ≠ 0

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a = 1 ∨ b = 0 → a ^ b = 1

Tactic:
by

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

Goal state before:
pp: b n k : ℕ
⊢ log b (n / b ^ k) = log b n - k

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = a % c

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ^ b = 1 ↔ a = 1 ∨ b = 0

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
⊢ IsSuccLimit (a ^ b)

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

Tactic:
by

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

Goal state before:
pp: b c : Ordinal.{u_4}
P : Ordinal.{u_4} → Prop
⊢ (∀ a < b * c, P a) ↔ ∀ q < c, ∀ r < b, P (b * q + r)

Tactic:
by

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

Goal state before:
pp: b c : Ordinal.{u_4}
P : Ordinal.{u_4} → Prop
⊢ (∃ a < b * c, P a) ↔ ∃ q < c, ∃ r < b, P (b * q + r)

Tactic:
by

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ 0 < b

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_1}
h₁ : 0 < a
h₂ : b ≤ c
⊢ a ^ b ≤ a ^ c

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ o * ⨆ i, f i = ⨆ i, o * f i

Tactic:
by

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

Goal state before:
pp: b n : ℕ
⊢ log b (n / b * b) = log b n

Tactic:
by

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < b

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ⨆ n, o + ↑n = o + ω

Tactic:
by

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < n + b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ CharZero Ordinal.{u_4}

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ⨆ n, o * ↑n = o * ω

Tactic:
by

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ (n + b - 1) / b < n

Tactic:
by

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

Goal state before:
pp: m : ℕ
⊢ ↑(m * 0) = ↑m * ↑0

Tactic:
by

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

Goal state before:
pp: b : Bool
n : ℕ
hn : n ≠ 0
⊢ log 2 (bit b n) = log 2 n + 1

Tactic:
by

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

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ n.log2 = log 2 n

Tactic:
apply eq_of_forall_le_iff

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ ∀ (c : ℕ), c ≤ n.log2 ↔ c ≤ log 2 n
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
ab : a ≤ b
⊢ a ^ c ≤ b ^ c

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.log2 = log 2 n

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ ↑(m * (n + 1)) = ↑m * ↑(n + 1)

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ≤ a ^ b

Tactic:
by

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

Goal state before:
pp: b k n : ℕ
⊢ log (b ^ k) n = log b n / k

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≤ 1
b : ℕ
⊢ clog b n = 0

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : 1 < b
⊢ a < a ^ b

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c ≤ b ^ c

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ succ c < b ^ succ c

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ ↑(m % n) = ↑m % ↑n

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ ↑(m % n) = ↑m % ↑n

Tactic:
by
  rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add,
    Nat.div_add_mod]

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

Goal state before:
pp: ⊢ lift.{u, v} ↑0 = ↑0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ lift.{u, v} ↑(n + 1) = ↑(n + 1)

Tactic:
by

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

Goal state before:
pp: x : ℕ
⊢ (typein LT.lt).toRelEmbedding x = ↑x

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : Fin n
⊢ (typein LT.lt).toRelEmbedding x = ↑↑x

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_1}
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
x : Fin n
⊢ ↑↑x ∈ Iio (type LT.lt)

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : Fin n
⊢ (enum LT.lt) ⟨↑↑x, ⋯⟩ = x

Tactic:
by

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ^ (1 + b) = a * a ^ b

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_1}
h : b ≤ c
⊢ a ^ c = a ^ b * a ^ (c - b)

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o < ω ↔ ∃ n, o = ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : ℕ
⊢ ↑x ∈ Iio (type LT.lt)

Tactic:
by

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

Goal state before:
pp: x : ℕ
⊢ (enum LT.lt) ⟨↑x, ⋯⟩ = x

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Nat.cast '' Iio n = Iio ↑n

Tactic:
by

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

Goal state before:
pp: ⊢ 1 < ω

Tactic:
by

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

Goal state before:
pp: ⊢ IsSuccLimit ω

Tactic:
by

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

Goal state before:
pp: ⊢ IsSuccLimit ω

Tactic:
by
  rw [isSuccLimit_iff, isSuccPrelimit_iff_succ_lt]
  refine ⟨omega0_ne_zero, fun o h => ?_⟩
  obtain ⟨n, rfl⟩ := lt_omega0.1 h
  exact natCast_lt_omega0 (n + 1)

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

Goal state before:
pp: o : Ordinal.{u_4}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_4}
h : a < ω
⊢ a < o

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑n + ω = ω

Tactic:
by

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

Goal state before:
pp: n b fuel : ℕ
hn : 1 < n
hb : 1 < b
hfuel : n < b ^ fuel
⊢ (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧ 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 : Ordinal.{u_4}
h : a < ω
⊢ a + ω = ω

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a

Tactic:
by

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

Goal state before:
pp: a b c : Ordinal.{u_1}
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
⊢ ↑n + o = o

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∃ i, nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b

Tactic:
by

Goal state after: