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

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

pp: case inr.inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * succ b)

pp: case inr.inr
a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
lb : IsSuccLimit b
⊢ IsSuccLimit (a * b)

Tactic:
·

Goal state after:
case inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < 0
⊢ IsSuccLimit (a * 0)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr.inr
a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
lb : IsSuccLimit b
⊢ IsSuccLimit (a * b)

Tactic:
·

Goal state after:
case inr.inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * succ b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
·

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

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

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

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : (#α).ord ≤ type s
⊢ #α ≤ (type s).card

pp: case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : #α ≤ (type s).card
⊢ (#α).ord ≤ type s

Tactic:
·

Goal state after:
case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : (#α).ord ≤ type s
⊢ #α ≤ (type s).card
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : #α ≤ (type s).card
⊢ (#α).ord ≤ type s

Tactic:
·

Goal state after:
case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : #α ≤ (type s).card
⊢ (#α).ord ≤ type s
Module: Mathlib.SetTheory.Ordinal.Family

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

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

Tactic:
·

Goal state after:
case refine_1
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (o.bsup f) ≤ o.blsub f
⊢ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
c : Cardinal.{v}
a : Ordinal.{max v u}
ha : a < Ordinal.lift.{u, v} c.ord
⊢ a < (lift.{u, v} c).ord

pp: case refine_2
c : Cardinal.{v}
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord

Tactic:
·

Goal state after:
case refine_1
c : Cardinal.{v}
a : Ordinal.{max v u}
ha : a < Ordinal.lift.{u, v} c.ord
⊢ a < (lift.{u, v} c).ord
Module: Mathlib.SetTheory.Ordinal.Basic

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

Tactic:
·

Goal state after:
case refine_2
c : Cardinal.{v}
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord
Module: Mathlib.SetTheory.Ordinal.Basic

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

Tactic:
ord_le,

Goal state after:
case refine_2
c : Cardinal.{v}
⊢ lift.{u, v} c ≤ (Ordinal.lift.{u, v} c.ord).card
Module: Mathlib.Data.Nat.Log

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

pp: case inr
b n : ℕ
hb : 1 ≥ b
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

Tactic:
·

Goal state after:
case inl
b n : ℕ
hb : 1 < b
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
Module: Mathlib.Data.Nat.Log

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

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

Tactic:
·

Goal state after:
case inl.inl
b : ℕ
hb : 1 < b
⊢ log b 0 = 0 ↔ 0 < b ∨ b ≤ 1
Module: Mathlib.Data.Nat.Log

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

Tactic:
·

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

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

pp: case inr
a b c : Ordinal.{u_4}
h : a ≤ b * c
b0 : b ≠ 0
⊢ a / b ≤ c

Tactic:
·

Goal state after:
case inl
a c : Ordinal.{u_4}
h : a ≤ 0 * c
⊢ a / 0 ≤ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
h : a ≤ b * c
b0 : b ≠ 0
⊢ a / b ≤ c

Tactic:
·

Goal state after:
case inr
a b c : Ordinal.{u_4}
h : a ≤ b * c
b0 : b ≠ 0
⊢ a / b ≤ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / c ≤ b / c

Tactic:
·

Goal state after:
case inl
a b : Ordinal.{u_4}
h : a ≤ b
⊢ a / 0 ≤ b / 0
Module: Mathlib.Data.Nat.Log

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

Tactic:
·

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

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / c ≤ b / c

Tactic:
·

Goal state after:
case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / c ≤ b / c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ a + c / b ≤ (b * a + c) / b

Tactic:
·

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

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

pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1

Tactic:
·

Goal state after:
case zero
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ log b n < 0 ↔ log b (n / b) + 1 < 0
Module: Mathlib.Data.Nat.Log

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

Tactic:
·

Goal state after:
case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
·

Goal state after:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ a + c / b ≤ (b * a + c) / b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

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

Tactic:
·

Goal state after:
case inl
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
⊢ (a * b + c) / (a * 0) = b / 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
·

Goal state after:
case inr
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
⊢ (a * b + c) / (a * d) = 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 * b + c) / (a * d) ≤ b / d

pp: case a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b / d ≤ (a * b + c) / (a * 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) ≤ 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 * 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 a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b / d ≤ (a * b + c) / (a * d)

Tactic:
·

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

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

pp: case inr
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
hy : y ≠ 0
⊢ log b y < x

Tactic:
·

Goal state after:
case inl
b x : ℕ
hx : x ≠ 0
hlt : 0 < b ^ x
⊢ log b 0 < x
Module: Mathlib.Data.Nat.Log

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

Tactic:
·

Goal state after:
case inr
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
hy : y ≠ 0
⊢ log b y < x
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'
⊢ f (g i hi) ⋯ ≤ o.bsup f

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
⊢ 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'
⊢ f (g i hi) ⋯ ≤ o.bsup f
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
hb : b ≠ 0
⊢ a / b = c

Tactic:
·

Goal state after:
case inl
a c : Ordinal.{u_4}
hle : 0 * c ≤ a
hlt : a < 0 * (c + 1)
⊢ a / 0 = c
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
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

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

Tactic:
·

Goal state after:
case inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
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
⊢ 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
⊢ f i hi ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

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

Tactic:
·

Goal state after:
case inl
a c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / 0 = c ↔ 0 * c ≤ a ∧ a < 0 * (c + 1)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
⊢ a * (b - c) = a * b - a * c

Tactic:
·

Goal state after:
case inl
b c : Ordinal.{u_4}
⊢ 0 * (b - c) = 0 * b - 0 * c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
⊢ a * (b - c) = a * b - a * c

Tactic:
·

Goal state after:
case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
⊢ a * (b - c) = a * b - a * c
Module: Mathlib.Data.Nat.Log

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

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

Tactic:
·

Goal state after:
case inr.inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hm : m ≠ 0
hb : b ≤ 1
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
Module: Mathlib.Data.Nat.Log

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

Tactic:
·

Goal state after:
case inr.inr
b m : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < b ∧ 0 ≠ 0
⊢ log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

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

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

Tactic:
·

Goal state after:
case inl
⊢ 0 ^ 0 = 1
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
·

Goal state after:
case inr
a : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ 0 = 1
Module: Mathlib.SetTheory.Ordinal.Exponential

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

pp: case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ (b + 1) = a ^ b * a

Tactic:
·

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

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

Tactic:
·

Goal state after:
case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ (b + 1) = a ^ b * a
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

pp: case inr
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
hm : m ≠ 0
⊢ log b n = m

Tactic:
·

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

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

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

Tactic:
·

Goal state after:
case inl
a : Ordinal.{u_4}
h : IsSuccLimit (a + 0)
⊢ IsSuccLimit 0 ∨ 0 = 0 ∧ IsSuccLimit a
Module: Mathlib.Data.Nat.Log

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

Tactic:
·

Goal state after:
case inr
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
hm : m ≠ 0
⊢ log b n = m
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
a b : Ordinal.{u_4}
h : IsSuccLimit a
hb : b ≠ 0
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b

Tactic:
·

Goal state after:
case inl
a : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit 0 ∨ 0 = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
·

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

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

pp: case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ log b (n + 1)

Tactic:
·

Goal state after:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ log b (n + 1)
Module: Mathlib.Data.Nat.Log

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

Tactic:
·

Goal state after:
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ log b (n + 1)
Module: Mathlib.Data.Nat.Log

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

pp: case refine_2
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : b ^ log b (n + 1) = n + 1
⊢ log b n < log b (n + 1)

Tactic:
·

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

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

Tactic:
·

Goal state after:
case refine_2
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : b ^ log b (n + 1) = n + 1
⊢ log b n < log b (n + 1)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
a : Ordinal.{u_4}
ha : a ≠ 0
⊢ a % a = 0

Tactic:
·

Goal state after:
case inl
⊢ 0 % 0 = 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a : Ordinal.{u_4}
ha : a ≠ 0
⊢ a % a = 0

Tactic:
·

Goal state after:
case inr
a : Ordinal.{u_4}
ha : a ≠ 0
⊢ a % a = 0
Module: Mathlib.Data.Nat.Log

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

pp: case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n

Tactic:
·

Goal state after:
case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
c : Ordinal.{u_4}
⊢ 0 * c % 0 = 0

pp: case inr
b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ b * c % b = 0

Tactic:
·

Goal state after:
case inl
c : Ordinal.{u_4}
⊢ 0 * c % 0 = 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ b * c % b = 0

Tactic:
·

Goal state after:
case inr
b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ b * c % b = 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ (x * y + z) % x = z % x

Tactic:
·

Goal state after:
case inl
y z : Ordinal.{u_4}
⊢ (0 * y + z) % 0 = z % 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
·

Goal state after:
case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ (x * y + z) % x = z % x
Module: Mathlib.Data.Nat.Log

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

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

Tactic:
·

Goal state after:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b) = log b n - 1
Module: Mathlib.Data.Nat.Log

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

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

Tactic:
·

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

Goal state before:
pp: case refine_1
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ ∀ (a_1 : Ordinal.{u_1}), a ^ a_1 < a ^ succ a_1

pp: case refine_2
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
a✝ : Ordinal.{u_1}
hl : IsSuccLimit a✝
⊢ IsLUB ((fun x ↦ a ^ x) '' Iio a✝) (a ^ a✝)

Tactic:
·

Goal state after:
case refine_1
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ ∀ (a_1 : Ordinal.{u_1}), a ^ a_1 < a ^ succ a_1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_2
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
a✝ : Ordinal.{u_1}
hl : IsSuccLimit a✝
⊢ IsLUB ((fun x ↦ a ^ x) '' Iio a✝) (a ^ a✝)

Tactic:
·

Goal state after:
case refine_2
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
a✝ : Ordinal.{u_1}
hl : IsSuccLimit a✝
⊢ IsLUB ((fun x ↦ a ^ x) '' Iio a✝) (a ^ a✝)
Module: Mathlib.SetTheory.Ordinal.Exponential

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

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

Tactic:
·

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

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

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

Tactic:
·

Goal state after:
case inl
y z : Ordinal.{u_4}
⊢ 0 * y % (0 * z) = 0 * (y % z)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_1.inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ b ≤ 1

pp: case refine_1.inl.inr
b : Ordinal.{u_1}
⊢ 1 ^ b ≤ 1

pp: case refine_1.inr
a : Ordinal.{u_1}
⊢ a ^ 0 ≤ 1

Tactic:
·

Goal state after:
case refine_1.inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ 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:
·

Goal state after:
case inr
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * (y % z)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_1.inl.inr
b : Ordinal.{u_1}
⊢ 1 ^ b ≤ 1

pp: case refine_1.inr
a : Ordinal.{u_1}
⊢ a ^ 0 ≤ 1

Tactic:
·

Goal state after:
case refine_1.inl.inr
b : Ordinal.{u_1}
⊢ 1 ^ b ≤ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
·

Goal state after:
case refine_1.inr
a : Ordinal.{u_1}
⊢ a ^ 0 ≤ 1
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
⊢ 1 < a ^ b

Tactic:
·

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

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

pp: case inr
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

Tactic:
·

Goal state after:
case inl
o : Ordinal.{u_1}
⊢ o * sSup ∅ = sSup ((fun x ↦ o * x) '' ∅)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case inr.inl
s : Set Ordinal.{u_1}
hs : s.Nonempty
⊢ 0 * sSup s = sSup ((fun x ↦ 0 * x) '' s)

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

Tactic:
·

Goal state after:
case inr.inl
s : Set Ordinal.{u_1}
hs : s.Nonempty
⊢ 0 * sSup s = sSup ((fun x ↦ 0 * x) '' s)
Module: Mathlib.SetTheory.Ordinal.Exponential

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

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

Tactic:
·

Goal state after:
case inl
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
ha : a ≤ 1
⊢ a ^ b ≠ 1