mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case hf_tendsto
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ Tendsto (Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) atTop atTop

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

Tactic:
·

Goal state after:
case hf_tendsto
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ Tendsto (Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) atTop atTop
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
e₁ : o₁.split = (zero, m)
N₁ : zero.NF
r₁ : o₁.repr = zero.repr + ↑m
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

pp: case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
·

Goal state after:
case zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
e₁ : o₁.split = (zero, m)
N₁ : zero.NF
r₁ : o₁.repr = zero.repr + ↑m
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
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 : ℝ → ℝ),
    (basis_hd :: basis_tl).getLast? = some g →
      (Real.log ∘ Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) =o[atTop] (Real.log ∘ g)

Tactic:
·

Goal state after:
case hf_comp
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ ∀ (g : ℝ → ℝ),
    (basis_hd :: basis_tl).getLast? = some g →
      (Real.log ∘ Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) =o[atTop] (Real.log ∘ g)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

pp: case zero.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
·

Goal state after:
case zero.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
h : o₂ = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
h : ¬o₂ = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
·

Goal state after:
case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
h : o₂ = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
h : ¬o₂ = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
·

Goal state after:
case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
h : ¬o₂ = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case hl
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f) =ᶠ[atTop] fun x ↦ (g ^ b) x / (f ^ a) x

pp: case h
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ Tendsto (Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f)) atTop atTop

Tactic:
·

Goal state after:
case hl
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f) =ᶠ[atTop] fun x ↦ (g ^ b) x / (f ^ a) x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
·

Goal state after:
case zero.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : m = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
·

Goal state after:
case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : m = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case hf
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < f x

pp: case hg
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ Tendsto hd atTop atTop

pp: case h
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

pp: case hb
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ 0 < exp

Tactic:
·

Goal state after:
case hf
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < f x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case hg
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ Tendsto hd atTop atTop

pp: case h
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

pp: case hb
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ 0 < exp

Tactic:
·

Goal state after:
case hg
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ Tendsto hd atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case h
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

pp: case hb
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ 0 < exp

Tactic:
·

Goal state after:
case h
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case hb
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ 0 < exp

Tactic:
·

Goal state after:
case hb
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ 0 < exp
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ω ^ b'.repr * ↑↑(m.succPNat ^ k) = ω ^ b'.repr * (↑m + 1) ^ ↑k

pp: case neg.a1
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ 1 < ↑m + 1

pp: case neg.h
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ↑m + 1 < ω

Tactic:
·

Goal state after:
case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ω ^ b'.repr * ↑↑(m.succPNat ^ k) = ω ^ b'.repr * (↑m + 1) ^ ↑k
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.a1
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ 1 < ↑m + 1

pp: case neg.h
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ↑m + 1 < ω

Tactic:
·

Goal state after:
case neg.a1
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ 1 < ↑m + 1
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.h
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ↑m + 1 < ω

Tactic:
·

Goal state after:
case neg.h
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ↑m + 1 < ω
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
·

Goal state after:
case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
simp only [opow_def, e₁, r₁, split_eq_scale_split' e₂, opowAux2, repr]

Goal state after:
case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
⊢ (match (scale 1 b', k) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
e₂ : o₂.split' = (b', 0)
r₂ : o₂.repr = ω * b'.repr + ↑0
⊢ (match (scale 1 b', 0) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr

pp: case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (match (scale 1 b', k + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr

Tactic:
·

Goal state after:
case oadd.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
e₂ : o₂.split' = (b', 0)
r₂ : o₂.repr = ω * b'.repr + ↑0
⊢ (match (scale 1 b', 0) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case pos
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
s t : Stream'.Seq α
hst : s = t
⊢ dist (op s) (op t) ≤ dist s t

pp: case neg
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
s t : Stream'.Seq α
hst : ¬s = t
⊢ dist (op s) (op t) ≤ dist s t

Tactic:
·

Goal state after:
case pos
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
s t : Stream'.Seq α
hst : s = t
⊢ dist (op s) (op t) ≤ dist s t
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (match (scale 1 b', k + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr

Tactic:
·

Goal state after:
case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (match (scale 1 b', k + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inl
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h✝ : a < b + o
h : a < b
⊢ ∃ i, a < b + f i

pp: case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a < b + o
h' : b ≤ a
⊢ ∃ i, a < b + f i

Tactic:
·

Goal state after:
case inl
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h✝ : a < b + o
h : a < b
⊢ ∃ i, a < b + f i
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a < b + o
h' : b ≤ a
⊢ ∃ i, a < b + f i

Tactic:
·

Goal state after:
case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a < b + o
h' : b ≤ a
⊢ ∃ i, a < b + f i
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case h.h.h.inl
γ : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
x✝ y✝ : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x✝ y✝
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = y ∨ ∃ exp coef c x' y', x = cons exp coef (op c x') ∧ y = cons exp coef (op c y') ∧ motive x' y'
x y : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
ih : motive x y
h : x = y
⊢ x = y ∨ ∃ hd u' v' c, x = Seq.cons hd (op c u') ∧ y = Seq.cons hd (op c v') ∧ motive u' v'

pp: case h.h.h.inr
γ : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
x y : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x y
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = y ∨ ∃ exp coef c x' y', x = cons exp coef (op c x') ∧ y = cons exp coef (op c y') ∧ motive x' y'
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
x' y' : Multiseries basis_hd basis_tl
h_next : motive x' y'
ih : motive (cons exp coef (op c x')) (cons exp coef (op c y'))
⊢ cons exp coef (op c x') = cons exp coef (op c y') ∨
    ∃ hd u' v' c_1,
      cons exp coef (op c x') = Seq.cons hd (op c_1 u') ∧
        cons exp coef (op c y') = Seq.cons hd (op c_1 v') ∧ motive u' v'

Tactic:
·

Goal state after:
case h.h.h.inl
γ : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
x✝ y✝ : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x✝ y✝
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = y ∨ ∃ exp coef c x' y', x = cons exp coef (op c x') ∧ y = cons exp coef (op c y') ∧ motive x' y'
x y : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
ih : motive x y
h : x = y
⊢ x = y ∨ ∃ hd u' v' c, x = Seq.cons hd (op c u') ∧ y = Seq.cons hd (op c v') ∧ motive u' v'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: β : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
next : β
f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)
b : β
h : f b = some (exp, coef, next)
⊢ corec f b = cons exp coef (corec f next)

Tactic:
simp only [corec, cons]

Goal state after:
β : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
next : β
f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)
b : β
h : f b = some (exp, coef, next)
⊢ Seq.corec (fun a ↦ Option.map (fun x ↦ ((x.1, x.2.1), x.2.2)) (f a)) b =
    Seq.cons (exp, coef) (Seq.corec (fun a ↦ Option.map (fun x ↦ ((x.1, x.2.1), x.2.2)) (f a)) next)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ Seq.nil = nil

pp: β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ Option.map
      (fun x ↦
        match x with
        | (exp, coef, c, next) => ((exp, coef), c, next))
      (F b) =
    none

Tactic:
·

Goal state after:
β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ Seq.nil = nil