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

Goal state before:
pp: case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ 0 = 0

pp: case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ b + c ≠ 0

Tactic:
]

Goal state after:
case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ b + c ≠ 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: x : ℕ
this : Fintype ↑(Iio x)
⊢ Fintype.card ↑(Iio x) = x

Tactic:
]

Goal state after:
x : ℕ
this : Fintype ↑(Iio x)
⊢ Fintype.card ↑(Iio x) = x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: x : ℕ
this : Fintype ↑(Iio x)
⊢ Fintype.card ↑(Iio x) = Fintype.card (Fin x)

Tactic:
]

Goal state after:
x : ℕ
this : Fintype ↑(Iio x)
⊢ Fintype.card ↑(Iio x) = Fintype.card (Fin x)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
x : Fin n
⊢ Fintype.card ↑(Iio x) = ↑x

Tactic:
]

Goal state after:
n : ℕ
x : Fin n
⊢ Fintype.card ↑(Iio x) = ↑x
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: ⊢ ω ≠ 0 ∧ ∀ a < ω, succ a < ω

Tactic:
]

Goal state after:
⊢ ω ≠ 0 ∧ ∀ a < ω, succ a < ω
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
]

Goal state after:
o : Ordinal.{u_4}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_4}
h : a < ω
n : ℕ
e : a = ↑n
⊢ succ ↑n ≤ o
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
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
⊢ w < b ^ u

Tactic:
]

Goal state after:
case hab
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ w < b ^ u
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case case1.inl
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd + 1 ≤ y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y

Tactic:
]

Goal state after:
case case1.inl
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd + 1 ≤ y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y
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 * x ≤ b ^ u * x

Tactic:
]

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

Goal state before:
pp: case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
⊢ ∀ d < ω, ω * (x / ω) + d ≤ a

Tactic:
]

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
⊢ ∀ d < ω, ω * (x / ω) + d ≤ a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ succ u ≤ b ^ x

Tactic:
]

Goal state after:
b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ succ u ≤ b ^ x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
n : ℕ
hb : ↑n < ω
⊢ x + ↑n ≤ a

Tactic:
]

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
n : ℕ
hb : ↑n < ω
⊢ x + ↑n ≤ a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a ≠ 0 ∧ ω ∣ a ↔ a ≠ 0 ∧ ω ∣ a

Tactic:
]

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < (clog.go n b n).snd + 1

pp: case hc
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 1 < b ∧ 1 < n

Tactic:
]

Goal state after:
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < (clog.go n b n).snd + 1

case hc
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 1 < b ∧ 1 < n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c.ord.card = c.ord.card

pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ω ≤ c.ord

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ω ≤ c.ord
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ℵ₀ ≤ c

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ℵ₀ ≤ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ sSup ((fun x ↦ b ^ x) ⁻¹' Iic 0) = 0

Tactic:
]

Goal state after:
case inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ sSup ((fun x ↦ b ^ x) ⁻¹' Iic 0) = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ 0 + 1 = 1

pp: case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1

Tactic:
]

Goal state after:
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
]

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

Goal state before:
pp: case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ n + b - 1 < succ 1 * b

pp: case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ 0 < b

Tactic:
]

Goal state after:
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ n + b - 1 < succ 1 * b

case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ 0 < b
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

Goal state after:
case inl
b x y : ℕ
h : x ≤ b ^ y
hb : 1 < b
⊢ x ≤ b ^ y
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
⊢ c ≤ a.card

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

Tactic:
]

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

case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ a.card
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x : ℕ
hb : 1 < b
z : ℕ
⊢ x ≤ z ↔ x ≤ z

Tactic:
]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ (clog b x).pred < clog b x

Tactic:
]

Goal state after:
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ (clog b x).pred < clog b x
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

Goal state after:
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ 0 ≤ clog b m
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

Goal state after:
case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ n ≤ b ^ clog b m
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

Goal state after:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ n ≤ b ^ clog c n
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ clog b n
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.zero
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog b 0

Tactic:
]

Goal state after:
case inr.zero
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog 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
⊢ ℵ₀ ≤ 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

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 inl
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ 0
hb : b ≤ 1
⊢ b ^ c ≤ x

Tactic:
]

Goal state after:
case inl
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ 0
hb : b ≤ 1
⊢ b ^ c ≤ x
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
⊢ c ≤ log b x

Tactic:
]

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

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

Tactic:
]

Goal state after:
case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ n < n + 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 ≤ f i (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 ≤ f i (nfpFamily f a)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
⊢ clog b n = clog b (n + 1) ↔ clog b (n + 1) ≤ clog b n

Tactic:
]

Goal state after:
b n : ℕ
hb : 1 < b
⊢ clog b n = clog b (n + 1) ↔ clog b (n + 1) ≤ clog b n
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
⊢ log b x ≤ log b x

Tactic:
]

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

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

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord
Module: Mathlib.Data.Nat.Log

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

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
l : List ι
⊢ a ≤ a

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (x : Ordinal.{u}), ∃ y ∈ ⋂ i, fixedPoints (f i), x < y

Tactic:
]

Goal state after:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (x : Ordinal.{u}), ∃ y ∈ ⋂ i, fixedPoints (f i), x < y
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b x : Ordinal.{u_1}
hx : 1 ≤ x
hb : b ≤ 1
⊢ b ^ log b x ≤ x

Tactic:
]

Goal state after:
case inl
b x : Ordinal.{u_1}
hx : 1 ≤ x
hb : b ≤ 1
⊢ b ^ log b x ≤ x
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
]

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

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))

Tactic:
]

Goal state after:
case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ b ≤ o

Tactic:
]

Goal state after:
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ b ≤ o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
⊢ IsLUB (Set.range fun x ↦ derivFamily f ↑x) (⨆ b, derivFamily f ↑b)

Tactic:
]

Goal state after:
case refine_2
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
⊢ IsLUB (Set.range fun x ↦ derivFamily f ↑x) (⨆ b, derivFamily f ↑b)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ o < b

Tactic:
]

Goal state after:
case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ o < b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case zero
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
⊢ f i (nfpFamily f 0) = nfpFamily f 0

Tactic:
]

Goal state after:
case zero
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
⊢ f i (nfpFamily f 0) = nfpFamily f 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case add_one
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o✝ : Ordinal.{u}
a✝ : f i (derivFamily f o✝) = derivFamily f o✝
⊢ f i (nfpFamily f (derivFamily f o✝ + 1)) = nfpFamily f (derivFamily f o✝ + 1)

Tactic:
]

Goal state after:
case add_one
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o✝ : Ordinal.{u}
a✝ : f i (derivFamily f o✝) = derivFamily f o✝
⊢ f i (nfpFamily f (derivFamily f o✝ + 1)) = nfpFamily f (derivFamily f o✝ + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : b ≤ 1
⊢ 0 ≤ 0

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.FixedPoint

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ ⨆ i_1, f i (derivFamily f ↑i_1) = ⨆ b, derivFamily f ↑b

Tactic:
]

Goal state after:
case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ ⨆ i_1, f i (derivFamily f ↑i_1) = ⨆ b, derivFamily f ↑b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
⊢ (∀ (i_1 : ↑(Set.Iio o)), f i (derivFamily f ↑i_1) ≤ c) ↔ ∀ (i : ↑(Set.Iio o)), derivFamily f ↑i ≤ c

Tactic:
]

Goal state after:
case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
⊢ (∀ (i_1 : ↑(Set.Iio o)), f i (derivFamily f ↑i_1) ≤ c) ↔ ∀ (i : ↑(Set.Iio o)), derivFamily f ↑i ≤ c
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
]

Goal state after:
case inl
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
a : ↑(Set.Iio o)
⊢ derivFamily f ↑a ≤ c ↔ derivFamily f ↑a ≤ c

Tactic:
]

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

Goal state before:
pp: case inr
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ o % b ^ log b o < b ^ log b o

Tactic:
]

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

Goal state before:
pp: case zero
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ nfpFamily f 0 ≤ a

Tactic:
]

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

Goal state before:
pp: case mpr.a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ x < b ^ (y + 1)

Tactic:
]

Goal state after:
case mpr.a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ x < b ^ (y + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ b ^ y ≤ x

Tactic:
]

Goal state after:
case a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ b ^ y ≤ x
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case add_one.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ nfpFamily f (derivFamily f o + 1) ≤ a

Tactic:
]

Goal state after:
case add_one.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ nfpFamily f (derivFamily f o + 1) ≤ a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ (u + log b v) ≤ b ^ u * v + w ∧ b ^ u * v + w < b ^ (u + log b v + 1)

pp: case hx
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w ≠ 0

Tactic:
]

Goal state after:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ (u + log b v) ≤ b ^ u * v + w ∧ b ^ u * v + w < b ^ (u + log b v + 1)

case hx
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w ≠ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case left
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v ≤ b ^ u * v

Tactic:
]

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

Goal state before:
pp: case right
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * (v + 1) ≤ b ^ u * b ^ (log b v + 1)

Tactic:
]

Goal state after:
case right
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * (v + 1) ≤ b ^ u * b ^ (log b v + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case h₂
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ v < b ^ (log b v + 1)

Tactic:
]

Goal state after:
case h₂
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ v < b ^ (log b v + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case limit.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : ∃ x, ¬derivFamily f ↑x ≤ a
⊢ ∃ o, derivFamily f o = a

Tactic:
]

Goal state after:
case limit.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : ∃ x, ¬derivFamily f ↑x ≤ a
⊢ ∃ o, derivFamily f o = a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case e'_2
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = log b (b ^ x)

Tactic:
]

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

Goal state before:
pp: case e'_3
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ b ^ log b o ≤ o

Tactic:
]

Goal state after:
case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ b ^ log b o ≤ o
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
]

Goal state after:
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o < b ^ succ (log b o)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ i, fixedPoints (f i)

Tactic:
]

Goal state after:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ i, fixedPoints (f i)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case right
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ (∀ (a : Ordinal.{u}), derivFamily f a ∈ ⋂ i, fixedPoints (f i)) ∧
    ∀ b ∈ ⋂ i, fixedPoints (f i), ∃ a, derivFamily f a = b

Tactic:
]

Goal state after:
case right
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ (∀ (a : Ordinal.{u}), derivFamily f a ∈ ⋂ i, fixedPoints (f i)) ∧
    ∀ b ∈ ⋂ i, fixedPoints (f i), ∃ a, derivFamily f a = b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case e'_2.e'_5
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 2 ^ log 2 o = 2 ^ log 2 o

Tactic:
]

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

Goal state before:
pp: case zero
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
⊢ id a < o

Tactic:
]

Goal state after:
case zero
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
⊢ id a < o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ log b x * b ^ log b y ≤ x * y

Tactic:
]

Goal state after:
case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ log b x * b ^ log b y ≤ x * y