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

Goal state before:
pp: case zero
⊢ 0 * zero = 0

pp: case oadd
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ 0 * a✝².oadd a✝¹ a✝ = 0

Tactic:
<;>

Goal state after:
case zero
⊢ 0 * zero = 0

case oadd
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ 0 * a✝².oadd a✝¹ a✝ = 0
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
⊢ zero * 0 = 0

pp: case oadd
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ a✝².oadd a✝¹ a✝ * 0 = 0

Tactic:
<;>

Goal state after:
case zero
⊢ zero * 0 = 0

case oadd
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ a✝².oadd a✝¹ a✝ * 0 = 0
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: x : ZFSet.{u_1}
⊢ x ∈ V_ (succ x.rank)

Tactic:
by
  simp [mem_vonNeumann]

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: a b : Ordinal.{u}
⊢ V_ a ∈ V_ b ↔ a < b

Tactic:
by
  simp [mem_vonNeumann]

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

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)

pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)

Tactic:
<;>

Goal state after:
case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)

case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : ¬e₂ = 0
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
x✝ : NF 0
h₂ : zero.NF
⊢ (0 * zero).NF

pp: case oadd
x✝ : NF 0
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 * a✝².oadd a✝¹ a✝).NF

Tactic:
<;>

Goal state after:
case zero
x✝ : NF 0
h₂ : zero.NF
⊢ (0 * zero).NF

case oadd
x✝ : NF 0
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 * a✝².oadd a✝¹ a✝).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
x✝ : NF 0
h₂ : zero.NF
⊢ (0 * zero).repr = repr 0 * zero.repr

pp: case oadd
x✝ : NF 0
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 * a✝².oadd a✝¹ a✝).repr = repr 0 * (a✝².oadd a✝¹ a✝).repr

Tactic:
<;>

Goal state after:
case zero
x✝ : NF 0
h₂ : zero.NF
⊢ (0 * zero).repr = repr 0 * zero.repr

case oadd
x✝ : NF 0
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 * a✝².oadd a✝¹ a✝).repr = repr 0 * (a✝².oadd a✝¹ a✝).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : e = 0
⊢ (e.oadd n a).split = (scale 1 o', m)

pp: case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : ¬e = 0
⊢ (e.oadd n a).split = (scale 1 o', m)

Tactic:
<;>

Goal state after:
case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : e = 0
⊢ (e.oadd n a).split = (scale 1 o', m)

case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : ¬e = 0
⊢ (e.oadd n a).split = (scale 1 o', m)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : e = 0
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + ↑m

pp: case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : ¬e = 0
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + ↑m

Tactic:
<;>

Goal state after:
case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : e = 0
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + ↑m

case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
e0 : ¬e = 0
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
n : ℕ
⊢ zero.mulNat n = zero * ↑n

pp: case oadd
n : ℕ
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ (a✝².oadd a✝¹ a✝).mulNat n = a✝².oadd a✝¹ a✝ * ↑n

Tactic:
<;>

Goal state after:
case zero
n : ℕ
⊢ zero.mulNat n = zero * ↑n

case oadd
n : ℕ
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ (a✝².oadd a✝¹ a✝).mulNat n = a✝².oadd a✝¹ a✝ * ↑n
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero.zero
⊢ zero.mulNat 0 = zero * ↑0

pp: case zero.succ
n✝ : ℕ
⊢ zero.mulNat (n✝ + 1) = zero * ↑(n✝ + 1)

pp: case oadd.zero
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ (a✝².oadd a✝¹ a✝).mulNat 0 = a✝².oadd a✝¹ a✝ * ↑0

pp: case oadd.succ
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
n✝ : ℕ
⊢ (a✝².oadd a✝¹ a✝).mulNat (n✝ + 1) = a✝².oadd a✝¹ a✝ * ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero.zero
⊢ zero.mulNat 0 = zero * ↑0

case zero.succ
n✝ : ℕ
⊢ zero.mulNat (n✝ + 1) = zero * ↑(n✝ + 1)

case oadd.zero
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ (a✝².oadd a✝¹ a✝).mulNat 0 = a✝².oadd a✝¹ a✝ * ↑0

case oadd.succ
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
n✝ : ℕ
⊢ (a✝².oadd a✝¹ a✝).mulNat (n✝ + 1) = a✝².oadd a✝¹ a✝ * ↑(n✝ + 1)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero.zero
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
⊢ (match 0, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF

pp: case zero.succ
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
n✝ : ℕ
⊢ (match n✝ + 1, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF

Tactic:
<;>

Goal state after:
case zero.zero
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
⊢ (match 0, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF

case zero.succ
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
n✝ : ℕ
⊢ (match n✝ + 1, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.succ.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑m) k m).NF

pp: case oadd.succ.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
n✝ : ℕ
e₂ : o₂.split' = (b', n✝ + 1 + 1)
⊢ (match (scale 1 b', n✝ + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑m) k m).NF

Tactic:
<;>

Goal state after:
case oadd.succ.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑m) k m).NF

case oadd.succ.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
n✝ : ℕ
e₂ : o₂.split' = (b', n✝ + 1 + 1)
⊢ (match (scale 1 b', n✝ + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑m) k m).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
⊢ (e.opowAux a0 a 0 0).repr = ω ^ e.repr * (opowAux 0 a0 a 0 0).repr

pp: case succ
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
n✝ : ℕ
⊢ (e.opowAux a0 a 0 (n✝ + 1)).repr = ω ^ e.repr * (opowAux 0 a0 a 0 (n✝ + 1)).repr

Tactic:
<;>

Goal state after:
case zero
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
⊢ (e.opowAux a0 a 0 0).repr = ω ^ e.repr * (opowAux 0 a0 a 0 0).repr

case succ
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
n✝ : ℕ
⊢ (e.opowAux a0 a 0 (n✝ + 1)).repr = ω ^ e.repr * (opowAux 0 a0 a 0 (n✝ + 1)).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : m = 0
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

pp: case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

Tactic:
<;>

Goal state after:
case pos
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : m = 0
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr

case neg
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
h : ¬m = 0
⊢ (e.opowAux a0 a (k + 1) m).repr = ω ^ e.repr * (opowAux 0 a0 a (k + 1) m).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero.zero
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
h : a'.repr + ↑0 < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) 0 0).repr
⊢ (0 ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑0) ∧
    (ω ^ a0.repr) ^ ↑0 * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑0) ^ succ ↑0

pp: case zero.succ
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
n✝ : ℕ
h : a'.repr + ↑(n✝ + 1) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) 0 (n✝ + 1)).repr
⊢ (0 ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑0) ∧
    (ω ^ a0.repr) ^ ↑0 * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑(n✝ + 1)) ^ succ ↑0

Tactic:
<;>

Goal state after:
case zero.zero
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
h : a'.repr + ↑0 < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) 0 0).repr
⊢ (0 ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑0) ∧
    (ω ^ a0.repr) ^ ↑0 * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑0) ^ succ ↑0

case zero.succ
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
n✝ : ℕ
h : a'.repr + ↑(n✝ + 1) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) 0 (n✝ + 1)).repr
⊢ (0 ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑0) ∧
    (ω ^ a0.repr) ^ ↑0 * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑(n✝ + 1)) ^ succ ↑0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil
α : Type u_1
t : Stream'.Seq α
h : nil.head = t.head
⊢ dist nil t = 2⁻¹ * dist nil.tail t.tail

pp: case cons
α : Type u_1
t : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝ s✝).head = t.head
⊢ dist (Seq.cons x✝ s✝) t = 2⁻¹ * dist (Seq.cons x✝ s✝).tail t.tail

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
t : Stream'.Seq α
h : nil.head = t.head
⊢ dist nil t = 2⁻¹ * dist nil.tail t.tail

case cons
α : Type u_1
t : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝ s✝).head = t.head
⊢ dist (Seq.cons x✝ s✝) t = 2⁻¹ * dist (Seq.cons x✝ s✝).tail t.tail
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil.nil
α : Type u_1
h : nil.head = nil.head
⊢ dist nil nil = 2⁻¹ * dist nil.tail nil.tail

pp: case nil.cons
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : nil.head = (Seq.cons x✝ s✝).head
⊢ dist nil (Seq.cons x✝ s✝) = 2⁻¹ * dist nil.tail (Seq.cons x✝ s✝).tail

pp: case cons.nil
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝ s✝).head = nil.head
⊢ dist (Seq.cons x✝ s✝) nil = 2⁻¹ * dist (Seq.cons x✝ s✝).tail nil.tail

pp: case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝¹ s✝¹).head = (Seq.cons x✝ s✝).head
⊢ dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) = 2⁻¹ * dist (Seq.cons x✝¹ s✝¹).tail (Seq.cons x✝ s✝).tail

Tactic:
<;>

Goal state after:
case nil.nil
α : Type u_1
h : nil.head = nil.head
⊢ dist nil nil = 2⁻¹ * dist nil.tail nil.tail

case nil.cons
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : nil.head = (Seq.cons x✝ s✝).head
⊢ dist nil (Seq.cons x✝ s✝) = 2⁻¹ * dist nil.tail (Seq.cons x✝ s✝).tail

case cons.nil
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝ s✝).head = nil.head
⊢ dist (Seq.cons x✝ s✝) nil = 2⁻¹ * dist (Seq.cons x✝ s✝).tail nil.tail

case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝¹ s✝¹).head = (Seq.cons x✝ s✝).head
⊢ dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) = 2⁻¹ * dist (Seq.cons x✝¹ s✝¹).tail (Seq.cons x✝ s✝).tail
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil.nil
α : Type u_1
h : True
⊢ dist nil nil = 2⁻¹ * dist nil.tail nil.tail

pp: case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : x✝¹ = x✝
⊢ dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) = 2⁻¹ * dist (Seq.cons x✝¹ s✝¹).tail (Seq.cons x✝ s✝).tail

Tactic:
<;>

Goal state after:
case nil.nil
α : Type u_1
h : True
⊢ dist nil nil = 2⁻¹ * dist nil.tail nil.tail

case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : x✝¹ = x✝
⊢ dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) = 2⁻¹ * dist (Seq.cons x✝¹ s✝¹).tail (Seq.cons x✝ s✝).tail
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil
α : Type u_1
t : Stream'.Seq α
h : dist nil t ≤ 2⁻¹
⊢ nil = nil ∧ t = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ t = Seq.cons hd t'

pp: case cons
α : Type u_1
t : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝ s✝) t ≤ 2⁻¹
⊢ Seq.cons x✝ s✝ = nil ∧ t = nil ∨ ∃ hd s' t', Seq.cons x✝ s✝ = Seq.cons hd s' ∧ t = Seq.cons hd t'

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
t : Stream'.Seq α
h : dist nil t ≤ 2⁻¹
⊢ nil = nil ∧ t = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ t = Seq.cons hd t'

case cons
α : Type u_1
t : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝ s✝) t ≤ 2⁻¹
⊢ Seq.cons x✝ s✝ = nil ∧ t = nil ∨ ∃ hd s' t', Seq.cons x✝ s✝ = Seq.cons hd s' ∧ t = Seq.cons hd t'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil.nil
α : Type u_1
h : dist nil nil ≤ 2⁻¹
⊢ nil = nil ∧ nil = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ nil = Seq.cons hd t'

pp: case nil.cons
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : dist nil (Seq.cons x✝ s✝) ≤ 2⁻¹
⊢ nil = nil ∧ Seq.cons x✝ s✝ = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'

pp: case cons.nil
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝ s✝) nil ≤ 2⁻¹
⊢ Seq.cons x✝ s✝ = nil ∧ nil = nil ∨ ∃ hd s' t', Seq.cons x✝ s✝ = Seq.cons hd s' ∧ nil = Seq.cons hd t'

pp: case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 2⁻¹
⊢ Seq.cons x✝¹ s✝¹ = nil ∧ Seq.cons x✝ s✝ = nil ∨
    ∃ hd s' t', Seq.cons x✝¹ s✝¹ = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'

Tactic:
<;>

Goal state after:
case nil.nil
α : Type u_1
h : dist nil nil ≤ 2⁻¹
⊢ nil = nil ∧ nil = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ nil = Seq.cons hd t'

case nil.cons
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : dist nil (Seq.cons x✝ s✝) ≤ 2⁻¹
⊢ nil = nil ∧ Seq.cons x✝ s✝ = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'

case cons.nil
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝ s✝) nil ≤ 2⁻¹
⊢ Seq.cons x✝ s✝ = nil ∧ nil = nil ∨ ∃ hd s' t', Seq.cons x✝ s✝ = Seq.cons hd s' ∧ nil = Seq.cons hd t'

case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 2⁻¹
⊢ Seq.cons x✝¹ s✝¹ = nil ∧ Seq.cons x✝ s✝ = nil ∨
    ∃ hd s' t', Seq.cons x✝¹ s✝¹ = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil.nil
α : Type u_1
h : True
⊢ nil = nil ∧ nil = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ nil = Seq.cons hd t'

pp: case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 1 / 2
⊢ Seq.cons x✝¹ s✝¹ = nil ∧ Seq.cons x✝ s✝ = nil ∨
    ∃ hd s' t', Seq.cons x✝¹ s✝¹ = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'

Tactic:
<;>

Goal state after:
case nil.nil
α : Type u_1
h : True
⊢ nil = nil ∧ nil = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ nil = Seq.cons hd t'

case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 1 / 2
⊢ Seq.cons x✝¹ s✝¹ = nil ∧ Seq.cons x✝ s✝ = nil ∨
    ∃ hd s' t', Seq.cons x✝¹ s✝¹ = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
h : a'.repr + ↑0 < ω ^ a0.repr
ω00 : 0 < ω0 ^ ↑0
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (0 + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) 0 0).repr
IH : (0 ≠ 0 → R < ω0 ^ succ ↑0) ∧ ω0 ^ ↑0 * α' + R = (α' + ↑0) ^ succ ↑0
RR : R' = ω0 ^ ↑0 * (α' * ↑0) + R
Rl : R < ω ^ (a0.repr * succ ↑0)
⊢ R = 0

pp: case succ
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
h : a'.repr + ↑0 < ω ^ a0.repr
n✝ : ℕ
ω00 : 0 < ω0 ^ ↑(n✝ + 1)
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (n✝ + 1 + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (n✝ + 1) 0).repr
IH : (n✝ + 1 ≠ 0 → R < ω0 ^ succ ↑(n✝ + 1)) ∧ ω0 ^ ↑(n✝ + 1) * α' + R = (α' + ↑0) ^ succ ↑(n✝ + 1)
RR : R' = ω0 ^ ↑(n✝ + 1) * (α' * ↑0) + R
Rl : R < ω ^ (a0.repr * succ ↑(n✝ + 1))
⊢ R = 0

Tactic:
<;>

Goal state after:
case zero
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
h : a'.repr + ↑0 < ω ^ a0.repr
ω00 : 0 < ω0 ^ ↑0
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (0 + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) 0 0).repr
IH : (0 ≠ 0 → R < ω0 ^ succ ↑0) ∧ ω0 ^ ↑0 * α' + R = (α' + ↑0) ^ succ ↑0
RR : R' = ω0 ^ ↑0 * (α' * ↑0) + R
Rl : R < ω ^ (a0.repr * succ ↑0)
⊢ R = 0

case succ
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
h : a'.repr + ↑0 < ω ^ a0.repr
n✝ : ℕ
ω00 : 0 < ω0 ^ ↑(n✝ + 1)
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (n✝ + 1 + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (n✝ + 1) 0).repr
IH : (n✝ + 1 ≠ 0 → R < ω0 ^ succ ↑(n✝ + 1)) ∧ ω0 ^ ↑(n✝ + 1) * α' + R = (α' + ↑0) ^ succ ↑(n✝ + 1)
RR : R' = ω0 ^ ↑(n✝ + 1) * (α' * ↑0) + R
Rl : R < ω ^ (a0.repr * succ ↑(n✝ + 1))
⊢ R = 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case inl
α : Type u_1
⊢ dist nil nil ≤ 2⁻¹

pp: case inr
α : Type u_1
hd : α
s' t' : Stream'.Seq α
⊢ dist (Seq.cons hd s') (Seq.cons hd t') ≤ 2⁻¹

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
⊢ dist nil nil ≤ 2⁻¹

case inr
α : Type u_1
hd : α
s' t' : Stream'.Seq α
⊢ dist (Seq.cons hd s') (Seq.cons hd t') ≤ 2⁻¹
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case hf_comp
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
g : ℝ → ℝ
hg : (basis_hd :: basis_tl).getLast? = some g
⊢ (Real.log ∘ Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) =o[atTop] (Real.log ∘ g)

Tactic:
simpa [List.getLast_of_getLast?_eq_some hg] using Real.isLittleO_log_id_atTop.comp_tendsto <|
      Real.tendsto_log_atTop.comp <| h_basis.tendsto_atTop <| List.mem_of_getLast? hg

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case inl
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
hx : op (Seq.cons hd x) = nil
hy : op (Seq.cons hd y) = nil
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

pp: case inr
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
w✝² : α
w✝¹ w✝ : Stream'.Seq α
hx : op (Seq.cons hd x) = Seq.cons w✝² w✝¹
hy : op (Seq.cons hd y) = Seq.cons w✝² w✝
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
hx : op (Seq.cons hd x) = nil
hy : op (Seq.cons hd y) = nil
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

case inr
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
w✝² : α
w✝¹ w✝ : Stream'.Seq α
hx : op (Seq.cons hd x) = Seq.cons w✝² w✝¹
hy : op (Seq.cons hd y) = Seq.cons w✝² w✝
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case inl
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
⊢ nil.head = nil.head

pp: case inr
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
hd : α
s_tl t_tl : Stream'.Seq α
⊢ (Seq.cons hd s_tl).head = (Seq.cons hd t_tl).head

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
⊢ nil.head = nil.head

case inr
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
hd : α
s_tl t_tl : Stream'.Seq α
⊢ (Seq.cons hd s_tl).head = (Seq.cons hd t_tl).head