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

Goal state before:
pp: case succ
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a ∘ (op a)^[n]) a < o

Tactic:
]

Goal state after:
case succ
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a ∘ (op a)^[n]) a < o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case right.refine_1
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
S : Set Ordinal.{u}
i : ι
hi : (fun i ↦ fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ (fun i ↦ fixedPoints (f i)) i

Tactic:
]

Goal state after:
case right.refine_1
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
S : Set Ordinal.{u}
i : ι
hi : (fun i ↦ fixedPoints (f i)) i = S
⊢ derivFamily f a ∈ (fun i ↦ fixedPoints (f i)) i
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
]

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

Goal state before:
pp: a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
⊢ ∀ (i : ↑(Set.Iio o)), op a ↑i ≤ o

Tactic:
]

Goal state after:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
⊢ ∀ (i : ↑(Set.Iio o)), op a ↑i ≤ o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
]

Goal state after:
case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
⊢ ∀ (i : ι), f i a = a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : ℕ), f^[i] a ≤ nfp f a

Tactic:
]

Goal state after:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : ℕ), f^[i] a ≤ nfp f a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ List.foldr (fun x ↦ f) a (List.replicate n ()) ≤ nfp f a

Tactic:
]

Goal state after:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ List.foldr (fun x ↦ f) a (List.replicate n ()) ≤ nfp f a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ f^[l.length] a ≤ ⨆ n, f^[n] a

Tactic:
]

Goal state after:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ f^[l.length] a ≤ ⨆ n, f^[n] a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ ⨆ n, f^[n] a

Tactic:
]

Goal state after:
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ ⨆ n, f^[n] a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a * ↑n + a % ω ^ log ω a < a

Tactic:
]

Goal state after:
case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a * ↑n + a % ω ^ log ω a < a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < ⨆ n, f^[n] b ↔ ∃ n, a < f^[n] b

Tactic:
]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < ⨆ n, f^[n] b ↔ ∃ n, a < f^[n] b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case neg
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : ¬BddAbove s
⊢ IsPrincipal op (sSup ∅)

Tactic:
]

Goal state after:
case neg
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : ¬BddAbove s
⊢ IsPrincipal op (sSup ∅)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ↑n + 1 ≤ ↑(n + 1)

pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a ≠ 0

Tactic:
]

Goal state after:
case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ↑n + 1 ≤ ↑(n + 1)

case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a ≠ 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ ⨆ n, f^[n] a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b

Tactic:
]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ ⨆ n, f^[n] a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case h
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ a < ω ^ log ω a * (a / ω ^ log ω a + 1)

Tactic:
]

Goal state after:
case h
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ a < ω ^ log ω a * (a / ω ^ log ω a + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
⊢ f^[n.succ] a ≤ nfp f a

Tactic:
]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
⊢ f^[n.succ] a ≤ nfp f a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * ↑n
⊢ ω ^ b * ↑n ≤ ω ^ b * ↑n

pp: case hc
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * ↑n
⊢ 0 < ω

Tactic:
]

Goal state after:
case hc
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * ↑n
⊢ 0 < ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfpFamily (fun x ↦ f) a ↔ ∀ (i : Unit), f b < nfpFamily (fun x ↦ f) a

Tactic:
]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfpFamily (fun x ↦ f) a ↔ ∀ (i : Unit), f b < nfpFamily (fun x ↦ f) a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∀ (i : Unit), f a ≤ a

Tactic:
]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∀ (i : Unit), f a ≤ a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ (∃ y, deriv f y = a) ↔ ∃ o, deriv f o = a

Tactic:
]

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

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : ∃ n, a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
hb : ∃ n, b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Tactic:
]

Goal state after:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : ∃ n, a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
hb : ∃ n, b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ ⨆ n, 0^[n] a = a

Tactic:
]

Goal state after:
a : Ordinal.{u_1}
⊢ ⨆ n, 0^[n] a = a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case succ
a : Ordinal.{u_1}
n✝ : ℕ
⊢ (0 ∘ 0^[n✝]) a ≤ 0^[0] a

Tactic:
]

Goal state after:
case succ
a : Ordinal.{u_1}
n✝ : ℕ
⊢ (0 ∘ 0^[n✝]) a ≤ 0^[0] a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
]

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

Goal state before:
pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun x ↦ a + x) 0 ≤ nfp (fun x ↦ a + x) b

Tactic:
]

Goal state after:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun x ↦ a + x) 0 ≤ nfp (fun x ↦ a + x) b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a * ω ≤ a * ω

Tactic:
]

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ deriv (fun x ↦ a + x) 0 ≤ b

Tactic:
]

Goal state after:
case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ deriv (fun x ↦ a + x) 0 ≤ b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x ↦ a + x) c = b
⊢ deriv (fun x ↦ a + x) 0 ≤ deriv (fun x ↦ a + x) c

Tactic:
]

Goal state after:
case refine_1
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x ↦ a + x) c = b
⊢ deriv (fun x ↦ a + x) 0 ≤ deriv (fun x ↦ a + x) c
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b

Tactic:
]

Goal state after:
case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a * ω + (b - a * ω) = b

Tactic:
]

Goal state after:
case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a * ω + (b - a * ω) = b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a + b = b

Tactic:
]

Goal state after:
a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a + b = b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u}
⊢ deriv (fun x ↦ a + x) ⊥ = a * ω + ⊥ ∧
    ∀ (a_1 : Ordinal.{u}), deriv (fun x ↦ a + x) a_1 = a * ω + a_1 → deriv (fun x ↦ a + x) (succ a_1) = a * ω + succ a_1

Tactic:
]

Goal state after:
a : Ordinal.{u}
⊢ deriv (fun x ↦ a + x) ⊥ = a * ω + ⊥ ∧
    ∀ (a_1 : Ordinal.{u}), deriv (fun x ↦ a + x) a_1 = a * ω + a_1 → deriv (fun x ↦ a + x) (succ a_1) = a * ω + succ a_1
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_1
a : Ordinal.{u}
⊢ nfp (fun x ↦ a + x) 0 = a * ω

Tactic:
]

Goal state after:
case refine_1
a : Ordinal.{u}
⊢ nfp (fun x ↦ a + x) 0 = a * ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x ↦ a✝ + x) a = a✝ * ω + a
⊢ nfp (fun x ↦ a✝ + x) (a✝ * ω + a + 1) = a✝ * ω + a + 1

Tactic:
]

Goal state after:
case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x ↦ a✝ + x) a = a✝ * ω + a
⊢ nfp (fun x ↦ a✝ + x) (a✝ * ω + a + 1) = a✝ * ω + a + 1
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
ha : 0 < a
⊢ ⨆ n, (fun x ↦ a * x)^[n] 1 = ⨆ n, a ^ n

Tactic:
]

Goal state after:
a : Ordinal.{u_1}
ha : 0 < a
⊢ ⨆ n, (fun x ↦ a * x)^[n] 1 = ⨆ n, a ^ n
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ ∀ (n : ℕ), (fun x ↦ a * x)^[n] 0 ≤ 0

Tactic:
]

Goal state after:
a : Ordinal.{u_1}
⊢ ∀ (n : ℕ), (fun x ↦ a * x)^[n] 0 ≤ 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0
⊢ nfp (fun x ↦ 0 * x) b = 0 ^ ω

Tactic:
]

Goal state after:
case inl
b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0
⊢ nfp (fun x ↦ 0 * x) b = 0 ^ ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ ω ≤ a ^ ω

Tactic:
]

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

Goal state before:
pp: case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ op a b < ((fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n]) o

Tactic:
]

Goal state after:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ op a b < ((fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n]) o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x ↦ a * x) 1 ≤ nfp (fun x ↦ a * x) b

Tactic:
]

Goal state after:
case a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x ↦ a * x) 1 ≤ nfp (fun x ↦ a * x) b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ≤ b

Tactic:
]

Goal state after:
case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ≤ b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
⊢ ¬b = 0 → a ^ ω ≤ b

Tactic:
]

Goal state after:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
⊢ ¬b = 0 → a ^ ω ≤ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : o.IsInitial
c : Cardinal.{u_1}
⊢ o ≤ c.ord ↔ o ≤ c.ord

Tactic:
]

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

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ nfp (fun x ↦ a * x) 1 ≤ b

Tactic:
]

Goal state after:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ nfp (fun x ↦ a * x) 1 ≤ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a.IsInitial
h : a ≤ b.card.ord
⊢ a ≤ b

Tactic:
]

Goal state after:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a ≤ b.card.ord
⊢ a ≤ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a.IsInitial
h : a ≤ b.card.ord
⊢ b ≤ b

Tactic:
]

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

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : 1 ≤ b
⊢ nfp (fun x ↦ a * x) 1 ≤ b

Tactic:
]

Goal state after:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : 1 ≤ b
⊢ nfp (fun x ↦ a * x) 1 ≤ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c.ord = c.ord

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ω = ω

Tactic:
]

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

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

Tactic:
]

Goal state after:
case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ 0 = b ↔ b = 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ op a b < ((fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m]) o

Tactic:
]

Goal state after:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ op a b < ((fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m]) o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ b % a ^ ω = 0

Tactic:
]

Goal state after:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ b % a ^ ω = 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
this : succ a.card ≤ a.card
⊢ False

Tactic:
]

Goal state after:
a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
this : succ a.card ≤ a.card
⊢ False
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ sInf {x | x.IsInitial} = 0

Tactic:
]

Goal state after:
⊢ sInf {x | x.IsInitial} = 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
IH : preOmega ↑n = ↑n
⊢ n < n + 1

Tactic:
]

Goal state after:
n : ℕ
IH : preOmega ↑n = ↑n
⊢ n < n + 1
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ StrictMono ⇑preOmega ∧
    ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Ordinal.{u_1}), (∀ b < o, preOmega b ≤ a) → preOmega o ≤ a

Tactic:
]

Goal state after:
⊢ StrictMono ⇑preOmega ∧
    ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Ordinal.{u_1}), (∀ b < o, preOmega b ≤ a) → preOmega o ≤ a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case succ
a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
n : ℕ
h : a * ↑n < o
⊢ a * ↑n + a < o

Tactic:
]

Goal state after:
case succ
a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
n : ℕ
h : a * ↑n < o
⊢ a * ↑n + a < o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ (preOmega b).card < a.card

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ (preOmega b).card < a.card
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
⊢ o ≠ 0 ∧ ∀ a < o, succ a < o

Tactic:
]

Goal state after:
o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
⊢ o ≠ 0 ∧ ∀ a < o, succ a < o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ b < succ b

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ b < succ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x : Ordinal.{u_1}
⊢ x.IsInitial ↔ x.IsInitial

Tactic:
]

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

Goal state before:
pp: case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
⊢ b % a ^ ω = 0

Tactic:
]

Goal state after:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
⊢ b % a ^ ω = 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 + x2) a b < a + o

Tactic:
]

Goal state after:
case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 + x2) a b < a + o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b c : Ordinal.{u}
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ c = c

Tactic:
]

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

Goal state before:
pp: a : Ordinal.{u}
ha : ∃ a_1 < a, ∃ b < a, a ≤ a_1 + b
⊢ ∃ b < a, ∃ c < a, b + c = a

Tactic:
]

Goal state after:
a : Ordinal.{u}
ha : ∃ a_1 < a, ∃ b < a, a ≤ a_1 + b
⊢ ∃ b < a, ∃ c < a, b + c = a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ c
hab : a - b = a
⊢ False

Tactic:
]

Goal state after:
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ c
hab : a - b = a
⊢ False
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ c
hab : a - b = a
⊢ False

Tactic:
exact H.not_gt hc

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

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

Tactic:
]

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ ∀ b < ω ^ o, b + b < ω ^ o

Tactic:
]

Goal state after:
case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ ∀ b < ω ^ o, b + b < ω ^ o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 ≤ o

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
⊢ 0 ≤ o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_1.inr
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ 0 < a

Tactic:
]

Goal state after:
case inr.refine_1.inr
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ 0 < a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ 0 < 1

Tactic:
]

Goal state after:
⊢ 0 < 1
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * ↑m
⊢ ω ^ c * ↑(m + m) ≤ ω ^ o

Tactic:
]

Goal state after:
case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * ↑m
⊢ ω ^ c * ↑(m + m) ≤ ω ^ o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mp
o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o → ¬o = 0 → o ∈ Set.range fun x ↦ ω ^ x

Tactic:
]

Goal state after:
case mp
o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o → ¬o = 0 → o ∈ Set.range fun x ↦ ω ^ x
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a ^ ω * c = a ^ ω * c

Tactic:
]

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

Goal state before:
pp: α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (#α).ord

Tactic:
]

Goal state after:
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (#α).ord
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl.inl
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 1

Tactic:
]

Goal state after:
case inl.inl
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 1
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a * b = b

Tactic:
]

Goal state after:
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a * b = b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl.inr
b : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
hb : b ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0

Tactic:
]

Goal state after:
case inl.inr
b : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
hb : b ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case h
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : (preOmega a).IsInitial
⊢ ω_ (a - ω) = preOmega a

Tactic:
]

Goal state after:
case h
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : (preOmega a).IsInitial
⊢ ω_ (a - ω) = preOmega a