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

Goal state before:
pp: case pos
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : BddAbove s
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

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

Tactic:
·

Goal state after:
case pos
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : BddAbove s
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b * b) = log b n

pp: case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b * b) = log b n

Tactic:
·

Goal state after:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b * b) = log b n
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
ha : 1 < a
⊢ a ^ b ≠ 1

Tactic:
·

Goal state after:
case inr
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
ha : 1 < a
⊢ a ^ b ≠ 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
a b c : Ordinal.{u_4}
hb₀ : b ≠ 0
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r

Tactic:
·

Goal state after:
case inl
a c : Ordinal.{u_4}
⊢ a < 0 * c ↔ ∃ q < c, ∃ r < 0, a = 0 * q + r
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 s = sSup ((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 s = sSup ((fun x ↦ o * x) '' s)
Module: Mathlib.SetTheory.Ordinal.Exponential

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

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

pp: case inr.inr
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
l' : IsSuccLimit b
⊢ IsSuccLimit (a ^ b)

Tactic:
·

Goal state after:
case inl
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
e : b = 0
⊢ IsSuccLimit (a ^ b)
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 ^ succ b)

pp: case inr.inr
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
l' : IsSuccLimit b
⊢ IsSuccLimit (a ^ b)

Tactic:
·

Goal state after:
case inr.inl
a : Ordinal.{u_1}
l : IsSuccLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ IsSuccLimit (a ^ succ b)
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 ∅
Module: Mathlib.Data.Nat.Log

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

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

Tactic:
·

Goal state after:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b * b) = log b n
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
·

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

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

pp: case inr
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 < a
⊢ a ^ b ≤ a ^ c

Tactic:
·

Goal state after:
case inl
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : a = 1
⊢ a ^ b ≤ a ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
·

Goal state after:
case inr
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 < a
⊢ a ^ b ≤ a ^ c
Module: Mathlib.Data.Nat.Log

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

Tactic:
by lia

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

Goal state before:
pp: case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
⊢ a ^ c ≤ b ^ c

pp: case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
⊢ a ^ c ≤ b ^ c

Tactic:
·

Goal state after:
case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
⊢ a ^ c ≤ b ^ c
Module: Mathlib.Data.Nat.Log

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

Tactic:
by lia

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 lia

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

Goal state before:
pp: case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
⊢ a ^ c ≤ b ^ c

Tactic:
·

Goal state after:
case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
⊢ a ^ c ≤ b ^ c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
⊢ log2 0 = log 2 0

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

Tactic:
·

Goal state after:
case inl
⊢ log2 0 = log 2 0
Module: Mathlib.SetTheory.Ordinal.Exponential

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

pp: case inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : 1 < a
⊢ a ^ 1 ≤ a ^ b

Tactic:
·

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

Goal state before:
pp: case inl
b k : ℕ
⊢ log (b ^ k) 0 = log b 0 / k

pp: case inr
b k n : ℕ
hn : n ≠ 0
⊢ log (b ^ k) n = log b n / k

Tactic:
·

Goal state after:
case inl
b k : ℕ
⊢ log (b ^ k) 0 = log b 0 / k
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 < 1
⊢ a ^ 1 ≤ a ^ b

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

Tactic:
·

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

Goal state before:
pp: case inr
b k n : ℕ
hn : n ≠ 0
⊢ log (b ^ k) n = log b n / k

Tactic:
·

Goal state after:
case inr
b k n : ℕ
hn : n ≠ 0
⊢ log (b ^ k) n = log b n / k
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b n : ℕ
hn : n ≠ 0
⊢ log (b ^ 0) n = log b n / 0

pp: case inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
⊢ log (b ^ k) n = log b n / k

Tactic:
·

Goal state after:
case inr.inl
b n : ℕ
hn : n ≠ 0
⊢ log (b ^ 0) n = log b n / 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
⊢ log (b ^ k) n = log b n / k

Tactic:
·

Goal state after:
case inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
⊢ log (b ^ k) n = log b n / k
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
⊢ log (b ^ k) n = log b n / k

pp: case inr.inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ log (b ^ k) n = log b n / k

Tactic:
·

Goal state after:
case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
⊢ log (b ^ k) n = log b n / k
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

pp: case inr
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
·

Goal state after:
case inl
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n
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
⊢ log (b ^ k) n = log b n / k

Tactic:
·

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

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

Tactic:
·

Goal state after:
case inr
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
m : ℕ
⊢ ↑(m / 0) = ↑m / ↑0

pp: case inr
m n : ℕ
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
·

Goal state after:
case inl
m : ℕ
⊢ ↑(m / 0) = ↑m / ↑0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
m n : ℕ
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
·

Goal state after:
case inr
m n : ℕ
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m / ↑n ≤ ↑(m / n)

Tactic:
·

Goal state after:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑(m / n) ≤ ↑m / ↑n
Module: Mathlib.SetTheory.Ordinal.Exponential

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

pp: case inr
a b c : Ordinal.{u_1}
ha : 0 < a
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
·

Goal state after:
case inl
b c : Ordinal.{u_1}
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ (b + 0) = 0 ^ b * 0 ^ 0

pp: case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

Tactic:
·

Goal state after:
case inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ (b + 0) = 0 ^ b * 0 ^ 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m / ↑n ≤ ↑(m / n)

Tactic:
·

Goal state after:
case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m / ↑n ≤ ↑(m / n)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inl
b c : Ordinal.{u_1}
ha : 0 < 1
⊢ 1 ^ (b + c) = 1 ^ b * 1 ^ c

pp: case inr.inr
a b c : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
·

Goal state after:
case inr.inl
b c : Ordinal.{u_1}
ha : 0 < 1
⊢ 1 ^ (b + c) = 1 ^ b * 1 ^ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
have : Fintype <| Iio x := Nat.fintypeIio x
  rw [← type_Iio_lt, type_fintype, Nat.cast_inj]
  nth_rw 2 [← Fintype.card_fin x]
  exact Fintype.card_congr Fin.equivSubtype.symm

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

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

pp: case inr
a b c : Ordinal.{u_1}
hb : 0 < b
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
·

Goal state after:
case inl
a c : Ordinal.{u_1}
⊢ a ^ (0 * c) = (a ^ 0) ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inl
b c : Ordinal.{u_1}
hb : 0 < b
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

pp: case inr.inr
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
·

Goal state after:
case inr.inl
b c : Ordinal.{u_1}
hb : 0 < b
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
o : Ordinal.{u_4}
ho : ω ≤ o
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
·

Goal state after:
case inl
o : Ordinal.{u_4}
ho : o < ω
⊢ (∃ n, o = ↑n) ∨ ω ≤ o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
·

Goal state after:
case inr
o : Ordinal.{u_4}
ho : ω ≤ o
⊢ (∃ n, o = ↑n) ∨ ω ≤ o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr.inl
b c : Ordinal.{u_1}
hb : 0 < b
ha : 1 ≠ 0
⊢ 1 ^ (b * c) = (1 ^ b) ^ c

pp: case inr.inr.inr
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
·

Goal state after:
case inr.inr.inl
b c : Ordinal.{u_1}
hb : 0 < b
ha : 1 ≠ 0
⊢ 1 ^ (b * c) = (1 ^ b) ^ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
a : Ordinal.{u_4}
ha : a < ↑n + ω
m : ℕ
hb' : ↑m < ω
hb : a ≤ ↑n + ↑m
⊢ a < ω

Tactic:
apply hb.trans_lt

Goal state after:
n : ℕ
a : Ordinal.{u_4}
ha : a < ↑n + ω
m : ℕ
hb' : ↑m < ω
hb : a ≤ ↑n + ↑m
⊢ ↑n + ↑m < ω
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case hab
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * v + w < b ^ u * (v + 1)

pp: case hbc
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * (v + 1) ≤ b ^ u * x

Tactic:
·

Goal state after:
case hab
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * v + w < b ^ u * (v + 1)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
⊢ a ≤ ω * (a / ω)

pp: case refine_2
a : Ordinal.{u_4}
h : ω ∣ a
⊢ IsSuccPrelimit a

Tactic:
·

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
⊢ a ≤ ω * (a / ω)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case hbc
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * (v + 1) ≤ b ^ u * x

Tactic:
·

Goal state after:
case hbc
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * (v + 1) ≤ b ^ u * x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case refine_2
a : Ordinal.{u_4}
h : ω ∣ a
⊢ IsSuccPrelimit a

Tactic:
·

Goal state after:
case refine_2
a : Ordinal.{u_4}
h : ω ∣ a
⊢ IsSuccPrelimit a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
x : Ordinal.{u_1}
h : 0 ≤ 1
⊢ log 0 x = 0

pp: case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ log 1 x = 0

Tactic:
·

Goal state after:
case inl
x : Ordinal.{u_1}
h : 0 ≤ 1
⊢ log 0 x = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ log 1 x = 0

Tactic:
·

Goal state after:
case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ log 1 x = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case zero
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ clog b n ≤ 0 ↔ clog b ((n + b - 1) / b) + 1 ≤ 0

pp: case succ
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
⊢ clog b n ≤ c + 1 ↔ clog b ((n + b - 1) / b) + 1 ≤ c + 1

Tactic:
·

Goal state after:
case zero
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ clog b n ≤ 0 ↔ clog b ((n + b - 1) / b) + 1 ≤ 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case not_isMin
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬IsMin c.ord

pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord

Tactic:
·

Goal state after:
case not_isMin
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬IsMin c.ord
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord

Tactic:
·

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord
Module: Mathlib.SetTheory.Ordinal.Exponential

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

pp: case inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ log b 0 = 0

Tactic:
·

Goal state after:
case inl
⊢ log 0 0 = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
⊢ clog b n ≤ c + 1 ↔ clog b ((n + b - 1) / b) + 1 ≤ c + 1

Tactic:
·

Goal state after:
case succ
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
⊢ clog b n ≤ c + 1 ↔ clog b ((n + b - 1) / b) + 1 ≤ c + 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ log b 0 = 0

Tactic:
·

Goal state after:
case inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ log b 0 = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ log b 0 = 0

Tactic:
rw [log]
    convert! csSup_empty
    aesop

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

Goal state before:
pp: case inl
b c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ 0 ↔ c ≤ log b 0

pp: case inr
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
hx : x ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x

Tactic:
·

Goal state after:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ 0 ↔ c ≤ log b 0
Module: Mathlib.Data.Nat.Log

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

pp: case inr
b x y : ℕ
h : x ≤ b ^ y
hb : 1 ≥ b
⊢ clog b x ≤ y

Tactic:
·

Goal state after:
case inl
b x y : ℕ
h : x ≤ b ^ y
hb : 1 < b
⊢ clog b x ≤ y
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
hx : x ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x

Tactic:
·

Goal state after:
case inr
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
hx : x ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b x y : ℕ
h : x ≤ b ^ y
hb : 1 ≥ b
⊢ clog b x ≤ y

Tactic:
·

Goal state after:
case inr
b x y : ℕ
h : x ≤ b ^ y
hb : 1 ≥ b
⊢ clog b x ≤ y
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ clog b n ≤ clog b m

pp: case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ clog b n ≤ clog b m

Tactic:
·

Goal state after:
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ clog b n ≤ clog b m
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ 0
⊢ c ≤ log b 0

pp: case inr
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
hx : x ≠ 0
⊢ c ≤ log b x

Tactic:
·

Goal state after:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ 0
⊢ c ≤ log b 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ clog b n ≤ clog b m

Tactic:
·

Goal state after:
case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ clog b n ≤ clog b m
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀.ord ≤ a + 1

pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord

Tactic:
ord_le,

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ (a + 1).card

case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ f i (List.foldr f a l) ≤ ⨆ i, List.foldr f a i

pp: case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ ⨆ i_1, f i (List.foldr f a i_1)

Tactic:
·

Goal state after:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ f i (List.foldr f a l) ≤ ⨆ i, List.foldr f a i
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n

pp: case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n

Tactic:
·

Goal state after:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
hx : x ≠ 0
⊢ c ≤ log b x

Tactic:
·

Goal state after:
case inr
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
hx : x ≠ 0
⊢ c ≤ log b x
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ ⨆ i_1, f i (List.foldr f a i_1)

Tactic:
·

Goal state after:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ ⨆ i_1, f i (List.foldr f a i_1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : b ≤ 1
⊢ b ^ c ≤ x

pp: case inr
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
⊢ b ^ c ≤ x

Tactic:
·

Goal state after:
case inl
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : b ≤ 1
⊢ b ^ c ≤ x
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case refine_1
b n : ℕ
hb : 1 < b
H : clog b n < clog b (n + 1)
⊢ b ^ clog b n = n

pp: case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ clog b n < clog b (n + 1)

Tactic:
·

Goal state after:
case refine_1
b n : ℕ
hb : 1 < b
H : clog b n < clog b (n + 1)
⊢ b ^ clog b n = n
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

pp: case refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ nfpFamily f a

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
⊢ b ≤ nfpFamily f a
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ clog b n < clog b (n + 1)

Tactic:
·

Goal state after:
case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ clog b n < clog b (n + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
⊢ b ^ c ≤ x

Tactic:
·

Goal state after:
case inr
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
⊢ b ^ c ≤ x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ a.card + 1

pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord

Tactic:
·

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ a.card + 1
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ nfpFamily f a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b ^ succ (log b 0)

pp: case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)

Tactic:
·

Goal state after:
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b ^ succ (log b 0)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord

Tactic:
·

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)

Tactic:
·

Goal state after:
case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b n : ℕ
⊢ clog (b ^ 0) n = (clog b n + (0 - 1)) / 0

pp: case inr
b k n : ℕ
hk : k > 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
·

Goal state after:
case inl
b n : ℕ
⊢ clog (b ^ 0) n = (clog b n + (0 - 1)) / 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b k n : ℕ
hk : k > 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
·

Goal state after:
case inr
b k n : ℕ
hk : k > 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b k n : ℕ
hk : k > 0
hb : 1 < b
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

pp: case inr.inr
b k n : ℕ
hk : k > 0
hb : 1 ≥ b
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
·

Goal state after:
case inr.inl
b k n : ℕ
hk : k > 0
hb : 1 < b
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k