mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n < b ^ c * b ↔ n < b ^ c * b

pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 0 < b

pp: case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

pp: case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n / b ≠ 0

pp: case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

pp: case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0

Tactic:
]

Goal state after:
case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 0 < b

case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n / b ≠ 0

case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0
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'.blsub g

Tactic:
]

Goal state after:
α : 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'.blsub g
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + c < a * (d * succ (b / d))

Tactic:
]

Goal state after:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + c < a * (d * succ (b / d))
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * succ b ≤ a * (d * succ (b / d))

Tactic:
]

Goal state after:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * succ b ≤ a * (d * succ (b / d))
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

Goal state after:
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ b ^ x ≤ y
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case h₂
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b < d * succ (b / d)

Tactic:
]

Goal state after:
case h₂
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b < d * succ (b / d)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ y ≠ 0

Tactic:
]

Goal state after:
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ y ≠ 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b ≤ a * b

Tactic:
]

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

Tactic:
]

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

Goal state before:
pp: case a
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
i : Ordinal.{max u v}
hi✝ : i < o
hi : ∃ i_1, ∃ (hi : i_1 < o'), i ≤ g i_1 hi
⊢ f i hi✝ ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯

Tactic:
]

Goal state after:
case a
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
i : Ordinal.{max u v}
hi✝ : i < o
hi : ∃ i_1, ∃ (hi : i_1 < o'), i ≤ g i_1 hi
⊢ f i hi✝ ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ b ^ m ≤ n ∧ n < b ^ m.succ ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

pp: case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

pp: case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

pp: case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

pp: case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

Tactic:
]

Goal state after:
case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : b ≤ 1 ∨ n = 0
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
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
⊢ f o = f o

Tactic:
]

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) = o.blsub fun x x_1 ↦ f x

pp: f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ ∀ a < o, f a < f (succ a)

Tactic:
]

Goal state after:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ ∀ a < o, f a < f (succ a)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ b ≤ c + d / a ↔ b ≤ c + d / a

Tactic:
]

Goal state after:
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✝) (a✝.bsup fun x x_1 ↦ f x)

Tactic:
]

Goal state after:
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✝) (a✝.bsup fun x x_1 ↦ f x)
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
]

Goal state after:
a : Ordinal.{u_1}
⊢ 1 - a ≤ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
]

Goal state after:
a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ a ≠ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case inr
a : Ordinal.{u_1}
h : a ≠ 0
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case inl
b : Ordinal.{u_1}
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ (limitRecOn (b + 1) 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) =
    (limitRecOn b 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) * a

Tactic:
]

Goal state after:
case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ (limitRecOn (b + 1) 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) =
    (limitRecOn b 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) * a
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

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

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
h' : b ≠ 0
⊢ IsSuccLimit (a + b - a) ∨ a + b - a = 0 ∧ IsSuccLimit a

Tactic:
]

Goal state after:
case inr
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
h' : b ≠ 0
⊢ IsSuccLimit (a + b - a) ∨ a + b - a = 0 ∧ IsSuccLimit a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b

Tactic:
]

Goal state after:
a b : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
f : Ordinal.{u} → Ordinal.{max u v}
⊢ (∀ (a : Ordinal.{u}), f a < f (succ a)) →
    ((∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o) ↔
      ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
⊢ (∀ (a_1 : Ordinal.{u_1}) (b_1 : a_1 ∈ Iio b), a ^ ↑⟨a_1, b_1⟩ ≤ c) ↔ ∀ b' < b, a ^ b' ≤ c

Tactic:
]

Goal state after:
a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
⊢ (∀ (a_1 : Ordinal.{u_1}) (b_1 : a_1 ∈ Iio b), a ^ ↑⟨a_1, b_1⟩ ≤ c) ↔ ∀ b' < b, a ^ b' ≤ c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ log b n * b ≤ n * b

Tactic:
]

Goal state after:
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ log b n * b ≤ n * b
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

Goal state after:
case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1) * b
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 = c

Tactic:
]

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 + d)

Tactic:
]

Goal state after:
a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * (b + d)
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case limit
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ (∀ b' < b, 1 ^ b' ≤ c) ↔ 1 ≤ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
]

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

Goal state before:
pp: case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ log b (n + 1)

Tactic:
]

Goal state after:
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ log b (n + 1)
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 ≤ c

Tactic:
]

Goal state after:
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 ≤ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
]

Goal state after:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * (a / b) + b
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

Goal state after:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ log b (n + 1) ≤ log b n
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: case mp
f : Ordinal.{u} → Ordinal.{max u v}
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
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.bsup fun x x_1 ↦ f x) = f o
⊢ (o.bsup fun a x ↦ f a) = f o

Tactic:
]

Goal state after:
case mp
f : Ordinal.{u} → Ordinal.{max u v}
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
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.bsup fun x x_1 ↦ f x) = f o
⊢ (o.bsup fun a x ↦ f a) = f o
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.bsup fun a x ↦ f a) = f o
⊢ (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
]

Goal state after:
case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.bsup fun a x ↦ f a) = f o
⊢ (o.bsup fun x x_1 ↦ f x) = f o
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ 0 = 0 - 1

Tactic:
]

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

Goal state before:
pp: case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ z - x * (z / x) = z - x * (z / x)

pp: case inr.b0
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x ≠ 0

Tactic:
]

Goal state after:
case inr.b0
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x ≠ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
]

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

Goal state before:
pp: case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b (n / b)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
a : α
ha : f a = ⨆ i, succ (f i)
⊢ ∃ i, f a < succ (f i)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
a : α
ha : f a = ⨆ i, succ (f i)
⊢ ∃ i, f a < succ (f i)
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 * (y / z) = x * (y % z) + w

Tactic:
]

Goal state after:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * y + w - x * z * (y / z) = x * (y % z) + w
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
]

Goal state after:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ ¬Small.{u, u + 1} ↑sᶜ
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 * y + w

Tactic:
]

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

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

Tactic:
]

Goal state after:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
this : Small.{u, u + 1} Ordinal.{u}
⊢ False
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
⊢ (a = 0 ∨ a = 1) ∨ b = 0 → a ^ b ≤ 1

Tactic:
]

Goal state after:
case refine_1
a b : Ordinal.{u_1}
⊢ (a = 0 ∨ a = 1) ∨ b = 0 → a ^ b ≤ 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * (y % z)

Tactic:
convert! mul_add_mod_mul hx y z using 1

Goal state after:
case e'_2
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = (x * y + 0) % (x * z)

case e'_3
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * (y % z) = x * (y % z) + 0
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case e'_2
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * y % (x * z)

Tactic:
]

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

Goal state before:
pp: case e'_3
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * (y % z) = x * (y % z)

Tactic:
]

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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = (b * (a / b) + a % b) % c

Tactic:
]

Goal state after:
a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = (b * (a / b) + a % b) % c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
x✝ : 1 < a ∧ b ≠ 0
ha : 1 < a
hb : b ≠ 0
⊢ b ≠ 0

Tactic:
]

Goal state after:
case refine_2
a b : Ordinal.{u_1}
x✝ : 1 < a ∧ b ≠ 0
ha : 1 < a
hb : b ≠ 0
⊢ b ≠ 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
]

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

Goal state before:
pp: case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * ⊥ = sSup ∅

pp: case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ ¬BddAbove ((fun x ↦ o * x) '' s)

Tactic:
]

Goal state after:
case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * ⊥ = sSup ∅

case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ ¬BddAbove ((fun x ↦ o * x) '' s)
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
]

Goal state after:
case inr.inl
a : Ordinal.{u_1}
l : IsSuccLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ IsSuccLimit (a ^ b * a)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
b c : Ordinal.{u_4}
hb₀ : b ≠ 0
q : Ordinal.{u_4}
hq : q < c
r : Ordinal.{u_4}
hr : r < b
⊢ b * c ≤ b * c

Tactic:
]

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

Goal state before:
pp: case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b n = log b n

Tactic:
]

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

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

Tactic:
]

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
a b : ℕ
h : a = b
⊢ a = b

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : ℕ
h : a = b
⊢ a = b
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

Goal state after:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ n + b ≤ n * b
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case inl
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ^ 1 ≤ a ^ b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
m : ℕ
⊢ 2 ^ m ≤ n ↔ 2 ^ m ≤ n

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ a ^ 1 ≤ a ^ b

Tactic:
]

Goal state after:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ a ^ 1 ≤ a ^ b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ 0 ^ b

Tactic:
]

Goal state after:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ 0 ^ b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c ≤ n ↔ (b ^ k) ^ c ≤ n

Tactic:
]

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

Goal state before:
pp: case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ 1 ≤ 1

Tactic:
]

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

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : 1 < a
⊢ 0 < b

Tactic:
]

Goal state after:
case inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : 1 < a
⊢ 0 < b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ 0 = 0

pp: case inr.inr.inr.hb
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ b ^ k ≤ 1

Tactic:
]

Goal state after:
case inr.inr.inr.hb
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ b ^ k ≤ 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
m n : ℕ
h : m ≤ n
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inr.inr.inr.hb
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ b ≤ 1

Tactic:
]

Goal state after:
case inr.inr.inr.hb
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ b ≤ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
]

Goal state after:
a b : Ordinal.{u_1}
ha : 1 < a
hb : 1 < b
⊢ 1 < b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
m n : ℕ
h : n ≤ m
⊢ ↑m = ↑m

Tactic:
]

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

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

Tactic:
]

Goal state after:
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c * a < b ^ c * b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n * n ≤ m

Tactic:
]

Goal state after:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n * n ≤ m