mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
R' : Type u_3
inst✝ : HSMul R' A A
r' : R'
r : R
hr : r = 0
h_smul : ∀ (a : A), r • a = r' • a
a : A
⊢ r' • a = 0 * a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
R' : Type u_3
inst✝ : HSMul R' A A
r' : R'
r r'' : R
hr : r = r''
h_smul : ∀ (a : A), r • a = r' • a
a : A
⊢ r' • a = ((algebraMap R A) r'' + 0) * a

Tactic:
by

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

Goal state before:
pp: x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ x.scale (e.oadd n a) = x.oadd 1 0 * e.oadd n a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
r t : R
h : -r = t
⊢ -(algebraMap R A) r = (algebraMap R A) t

Tactic:
by

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

Goal state before:
pp: x : ONote
inst✝¹ : x.NF
o : ONote
inst✝ : o.NF
⊢ (x.scale o).NF

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
b : ℕ
h : r ^ b = s
⊢ (algebraMap R A) r ^ b = (algebraMap R A) s

Tactic:
by

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

Goal state before:
pp: x : ONote
inst✝¹ : x.NF
o : ONote
inst✝ : o.NF
⊢ (x.scale o).repr = ω ^ x.repr * o.repr

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : Semifield R
inst✝¹ : Semifield A
inst✝ : Algebra R A
r s : R
h : r⁻¹ = s
⊢ ((algebraMap R A) r)⁻¹ = (algebraMap R A) s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : IsNat r 1
⊢ 1 = ↑1

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : IsNat r 1
⊢ IsNat ((algebraMap R A) (r + 0)) 1

Tactic:
by

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

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Tactic:
by

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

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
⊢ ω ∣ o'.repr

Tactic:
by

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

Goal state before:
pp: o e : ONote
n : ℕ+
a : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (e.oadd n a, m)
⊢ a.repr + ↑m < ω ^ e.repr

Tactic:
by

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

Goal state before:
pp: n : ℕ
o : ONote
⊢ o.mulNat n = o * ↑n

Tactic:
by

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

Goal state before:
pp: o : ONote
inst✝ : o.NF
n : ℕ
⊢ (o.mulNat n).NF

Tactic:
by

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

Goal state before:
pp: e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
⊢ ∀ (k m : ℕ), (e.opowAux a0 a k m).NF

Tactic:
by

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

Goal state before:
pp: o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
⊢ (o₁ ^ o₂).NF

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ e.repr * succ b < e.repr * ω

Tactic:
gcongr; exact isSuccLimit_omega0.succ_lt l

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

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ e.repr * succ b < e.repr * ω

Tactic:
by

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

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
a' : Ordinal.{0}
e0 : e.repr ≠ 0
h : a' < ω ^ e.repr
aa : a.repr = a'
n : ℕ+
⊢ (ω ^ e.repr * ↑↑n + a') ^ ω = (ω ^ e.repr) ^ ω

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Algebra.Basic

Goal state before:
pp: «$u» «$v» : Level
«$R» : Type u
«$A» : Type v
«$sR» : CommSemiring «$R»
«$sA» : CommSemiring «$A»
«$sAlg» : Algebra «$R» «$A»
$a✝ $b✝ «$a» «$b» : «$A»
«$r» «$s» «$t» : «$R»
«$pt» : «$r» * «$s» = «$t»
⊢ (algebraMap «$R» «$A») «$r» * (algebraMap «$R» «$A») «$s» = (algebraMap «$R» «$A») «$t»

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Algebra.Basic

Goal state before:
pp: «$u» «$v» : Level
«$R» : Type u
«$A» : Type v
«$sR» : CommSemiring «$R»
«$sA» : CommSemiring «$A»
«$sAlg» : Algebra «$R» «$A»
«$a» «$b» : «$A»
«$r» : «$R» := Nat.rawCast 1
⊢ Nat.rawCast 1 = (algebraMap «$R» «$A») («$r» + 0)

Tactic:
by

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

Goal state before:
pp: f g b : ℝ → ℝ
exp : ℝ
h_eq : g =ᶠ[atTop] f
h : Majorized f b exp
⊢ Majorized g b exp

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h✝ : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
x✝ : ℝ
h : 0 < f x✝
⊢ (fun t ↦ f t ^ exp / f t ^ exp') x✝ = (fun t ↦ f t ^ (exp - exp')) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun x ↦ f (c + x⁻¹)) atTop l
⊢ Tendsto f (𝓝[>] c) l

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun x ↦ f (c - x⁻¹)) atTop l
⊢ Tendsto f (𝓝[<] c) l

Tactic:
by

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

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ f t ^ (exp - exp')
⊢ 0 < exp' - exp

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h_neg : Tendsto (fun x ↦ f (c - x⁻¹)) atTop l
h_pos : Tendsto (fun x ↦ f (c + x⁻¹)) atTop l
⊢ Tendsto f (𝓝[≠] c) l

Tactic:
by

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

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

Tactic:
rw [← Ordinal.opow_add]

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

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
⊢ Majorized (f ^ exp) f exp

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
f : 𝕜 → α
c : 𝕜
inst✝ : TopologicalSpace α
a b : α
h_neg : Tendsto (fun x ↦ f (c - x⁻¹)) atTop (𝓝 a)
h_pos : Tendsto (fun x ↦ f (c + x⁻¹)) atTop (𝓝 b)
h_eq : a = b
⊢ Tendsto f (𝓝[≠] c) (𝓝 a)

Tactic:
by

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

Goal state before:
pp: f b : ℝ → ℝ
exp1 exp2 : ℝ
h_lt : exp1 ≤ exp2
h : ∀ exp' > exp1, f =o[atTop] (b ^ exp')
exp' : ℝ
h_exp : exp' > exp2
⊢ exp' > exp1

Tactic:
by

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

Goal state before:
pp: f b : ℝ → ℝ
exp1 exp2 : ℝ
h_lt : exp1 ≤ exp2
h : Majorized f b exp1
⊢ Majorized f b exp2

Tactic:
by

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

Goal state before:
pp: f b : ℝ → ℝ
exp : ℝ
h_lt : exp < 0
h : Majorized f b exp
⊢ 0 > exp

Tactic:
by

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

Goal state before:
pp: f b : ℝ → ℝ
exp : ℝ
h_lt : exp < 0
h : Majorized f b exp
⊢ Tendsto f atTop (𝓝 0)

Tactic:
by

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

Goal state before:
pp: b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c : ℝ
⊢ Majorized (fun x ↦ c) b 0

Tactic:
by

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

Goal state before:
pp: f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
exp' : ℝ
h_exp' : exp' > exp
⊢ exp' > f_exp

Tactic:
by

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

Goal state before:
pp: f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
exp' : ℝ
h_exp' : exp' > exp
⊢ exp' > g_exp

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : Majorized f b f_exp
hg : Majorized g b g_exp
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
⊢ Majorized (f + g) b exp

Tactic:
simp only [Majorized] at *
  intro exp' h_exp'
  exact (hf _ (by order)).add (hg _ (by order))

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

Goal state before:
pp: f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : Majorized f b f_exp
hg : Majorized g b g_exp
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
⊢ Majorized (f + g) b exp

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
⊢ f_exp + ε > f_exp

Tactic:
by

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

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
⊢ g_exp + ε > g_exp

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : Majorized f b f_exp
hg : Majorized g b g_exp
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
⊢ Majorized (f * g) b (f_exp + g_exp)

Tactic:
by

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

Goal state before:
pp: f g basis_hd : ℝ → ℝ
exp : ℝ
hf : Majorized f basis_hd exp
hg : g =O[atTop] fun x ↦ 1
⊢ Majorized (f * g) basis_hd exp

Tactic:
by

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

Goal state before:
pp: ⊢ WellFormedBasis []

Tactic:
by

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

Goal state before:
pp: f : ℝ → ℝ
hf : Tendsto f atTop atTop
⊢ WellFormedBasis [f]

Tactic:
by

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
h : WellFormedBasis (basis_hd :: basis_tl)
⊢ List.Sublist basis_tl (basis_hd :: basis_tl)

Tactic:
by

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

Goal state before:
pp: left right : Basis
h : WellFormedBasis (left ++ right)
⊢ List.Sublist right (left ++ right)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
this : IsClosed {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ CompleteSpace (Stream'.Seq α)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
hn : s n = none
⊢ 0 < (1 / 2) ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
hg : g ∈ basis_begin
h :
  List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (basis_begin ++ [basis_end]) ∧
    ∀ (f : ℝ → ℝ), f ∈ basis_begin ∨ f = basis_end → Tendsto f atTop atTop
⊢ (Real.log ∘ basis_end) =o[atTop] (Real.log ∘ g)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
hn : s n = none
t : Stream' (Option α)
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ n ≤ n + 1

Tactic:
by

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

Goal state before:
pp: basis : Basis
f : ℝ → ℝ
h : WellFormedBasis basis
h_comp : ∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ ∀ g ∈ basis, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ n + 1 ≤ n + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
⊢ CompleteSpace (Stream'.Seq α)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Stream' α
⊢ dist s t ≤ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : s ≠ t
⊢ ∃ n, dist s t = 2⁻¹ ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
⊢ Seq.cons x s ≠ Seq.cons x t

Tactic:
by

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

Goal state before:
pp: f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h : WellFormedBasis (basis_hd :: basis_tl)
h_comp : ∀ (g : ℝ → ℝ), (basis_hd :: basis_tl).head? = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_hd :: basis_tl
⊢ (basis_hd :: basis_tl).head? = some basis_hd

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
s t : Stream'.Seq α
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ dist s t = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x y : α
s t : Stream'.Seq α
h : x ≠ y
⊢ dist (Seq.cons x s) (Seq.cons y t) = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
s : Stream'.Seq α
⊢ dist (Seq.cons x s) nil = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
s : Stream'.Seq α
⊢ dist nil (Seq.cons x s) = 1

Tactic:
by

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

Goal state before:
pp: f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_tl
h :
  ((∀ a' ∈ basis_tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ basis_hd)) ∧
      List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) basis_tl) ∧
    Tendsto basis_hd atTop atTop ∧ ∀ a ∈ basis_tl, Tendsto a atTop atTop
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ basis_hd)

Tactic:
by

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

Goal state before:
pp: basis : Basis
f : ℝ → ℝ
h : WellFormedBasis basis
h_comp : ∀ (g : ℝ → ℝ), List.head? basis = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ ∀ g ∈ basis, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
⊢ FriendlyOperation op ↔ ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t

Tactic:
by

Goal state after: