awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
⊢ Tendsto (b ^ exp) atTop atTop

Tactic:
exact (tendsto_rpow_atTop h_exp).comp h_tendsto

Premises used: tendsto_rpow_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
b : ℝ → ℝ
exp : ℝ
⊢ Majorized 0 b exp

Tactic:
fun _ _ ↦ Asymptotics.isLittleO_zero _ _

Premises used: Asymptotics.isLittleO_zero, Filter.atTop, HPow.hPow, Tactic.ComputeAsymptotics.Majorized
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f b : ℝ → ℝ
exp : ℝ
h : Majorized f b exp
c : ℝ
⊢ Majorized (c • f) b exp

Tactic:
fun exp h_exp ↦ (h exp h_exp).const_mul_left _

Premises used: Asymptotics.IsLittleO.const_mul_left, Tactic.ComputeAsymptotics.Majorized
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
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
order order₁ order₂ order₃ : ¬exp' > f_exp → False
order₄ order₅ order₆ order₇ order₈ order₉ order₁₀ order₁₁ : exp' ≤ f_exp → False
⊢ exp' > f_exp

Tactic:
order
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
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
order order₁ order₂ order₃ : ¬exp' > g_exp → False
order₄ order₅ order₆ order₇ order₈ order₉ order₁₀ order₁₁ : exp' ≤ g_exp → False
⊢ exp' > g_exp

Tactic:
order
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
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
⊢ (f + g) =o[atTop] (b ^ exp')

Tactic:
exact (hf _ (by order)).add (hg _ (by order))

Premises used: Asymptotics.IsLittleO.add
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
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
dsimp : f_exp + (exp - f_exp - g_exp) / 2 > f_exp
⊢ f_exp + ε > f_exp

Tactic:
dsimp [ε]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
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
linarith : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → 2 / 2 = 1
linarith₁ : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → GT.gt (α := ℝ) 2 0
linarith₃ :
  f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp →
    f_exp + g_exp - exp + (2 * f_exp + (1 * exp - 1 * f_exp - 1 * g_exp) - 2 * f_exp) = 0
⊢ f_exp + (exp - f_exp - g_exp) / 2 > f_exp

Tactic:
linarith
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
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 =o[atTop] (b ^ (f_exp + ε))

Tactic:
specialize hf (f_exp + ε) (by dsimp [ε]; linarith)

Premises used: HAdd.hAdd
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
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 + ε))
dsimp : g_exp + (exp - f_exp - g_exp) / 2 > g_exp
⊢ g_exp + ε > g_exp

Tactic:
dsimp [ε]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
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 + ε))
linarith : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → 2 / 2 = 1
linarith₁ : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → GT.gt (α := ℝ) 2 0
linarith₃ :
  g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp →
    f_exp + g_exp - exp + (2 * g_exp + (1 * exp - 1 * f_exp - 1 * g_exp) - 2 * g_exp) = 0
⊢ g_exp + (exp - f_exp - g_exp) / 2 > g_exp

Tactic:
linarith
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
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 =o[atTop] (b ^ (g_exp + ε))

Tactic:
specialize hg (g_exp + ε) (by dsimp [ε]; linarith)

Premises used: HAdd.hAdd
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g b : ℝ → ℝ
f_exp g_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 + ε))
hg : g =o[atTop] (b ^ (g_exp + ε))
apply : (fun (t : ℝ) ↦ b t ^ (f_exp + ε) * b t ^ (g_exp + ε)) =ᶠ[atTop] b ^ exp
⊢ (f * g) =o[atTop] (b ^ exp)

Tactic:
apply (hf.mul hg).trans_eventuallyEq (g₁ := fun t ↦ b t ^ (f_exp + ε) * b t ^ (g_exp + ε))

Premises used: Asymptotics.IsLittleO.mul, Asymptotics.IsLittleO.trans_eventuallyEq
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g b : ℝ → ℝ
f_exp g_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 + ε))
hg : g =o[atTop] (b ^ (g_exp + ε))
apply : ∀ (x : ℝ), 0 < b x → (fun (t : ℝ) ↦ b t ^ (f_exp + ε) * b t ^ (g_exp + ε)) x = (b ^ exp) x
⊢ (fun (t : ℝ) ↦ b t ^ (f_exp + ε) * b t ^ (g_exp + ε)) =ᶠ[atTop] b ^ exp

Tactic:
apply h_pos.mono

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g b : ℝ → ℝ
f_exp g_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 + ε))
hg : g =o[atTop] (b ^ (g_exp + ε))
t : ℝ
hx : 0 < b t
dsimp : exp = f_exp + (exp - f_exp - g_exp) / 2 + (g_exp + (exp - f_exp - g_exp) / 2)
⊢ exp = f_exp + ε + (g_exp + ε)

Tactic:
dsimp [ε]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g b : ℝ → ℝ
f_exp g_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 + ε))
hg : g =o[atTop] (b ^ (g_exp + ε))
t : ℝ
hx : 0 < b t
⊢ exp = f_exp + (exp - f_exp - g_exp) / 2 + (g_exp + (exp - f_exp - g_exp) / 2)

Tactic:
ring_nf
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g b : ℝ → ℝ
f_exp g_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 + ε))
hg : g =o[atTop] (b ^ (g_exp + ε))
t : ℝ
hx : 0 < b t
rw : b t ^ (f_exp + ε) * b t ^ (g_exp + ε)
| b t ^ exp

Tactic:
rw [show exp = (f_exp + ε) + (g_exp + ε) by dsimp [ε]; ring_nf, Real.rpow_add hx]

Premises used: Real.rpow_add
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g b : ℝ → ℝ
f_exp g_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 + ε))
hg : g =o[atTop] (b ^ (g_exp + ε))
t : ℝ
hx : 0 < b t
conv_rhs : b t ^ (f_exp + ε) * b t ^ (g_exp + ε) = b t ^ exp
conv_rhs₁ : b t ^ (f_exp + ε) * b t ^ (g_exp + ε) = b t ^ (f_exp + ε) * b t ^ (g_exp + ε)
⊢ b t ^ (f_exp + ε) * b t ^ (g_exp + ε) = b t ^ exp

Tactic:
conv_rhs => rw [show exp = (f_exp + ε) + (g_exp + ε) by dsimp [ε]; ring_nf, Real.rpow_add hx]

Premises used: Real.rpow_add
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g basis_hd : ℝ → ℝ
exp_1 : ℝ
hf : Majorized f basis_hd exp_1
hg : IsBigO (F := ℝ) atTop g fun (x : ℝ) ↦ 1
exp : ℝ
h_exp : exp > exp_1
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ (basis_hd ^ exp) x * 1

Tactic:
IsLittleO.mul_isBigO (hf _ h_exp) hg

Premises used: Asymptotics.IsLittleO.mul_isBigO
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g basis_hd : ℝ → ℝ
exp_1 : ℝ
hf : Majorized f basis_hd exp_1
hg : IsBigO (F := ℝ) atTop g fun (x : ℝ) ↦ 1
exp : ℝ
h_exp : exp > exp_1
h : basis_hd ^ exp = fun (x : ℝ) ↦ (basis_hd ^ exp) x * 1
⊢ (f * g) =o[atTop] (basis_hd ^ exp)

Tactic:
convert! IsLittleO.mul_isBigO (hf _ h_exp) hg using 1

Premises used: Asymptotics.IsLittleO.mul_isBigO
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g basis_hd : ℝ → ℝ
exp_1 : ℝ
hf : Majorized f basis_hd exp_1
hg : IsBigO (F := ℝ) atTop g fun (x : ℝ) ↦ 1
exp : ℝ
h_exp : exp > exp_1
h : basis_hd ^ exp = fun (x : ℝ) ↦ basis_hd x ^ exp
⊢ basis_hd ^ exp = fun (x : ℝ) ↦ (basis_hd ^ exp) x * 1

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g basis_hd : ℝ → ℝ
exp_1 : ℝ
hf : Majorized f basis_hd exp_1
hg : IsBigO (F := ℝ) atTop g fun (x : ℝ) ↦ 1
exp : ℝ
h_exp : exp > exp_1
⊢ basis_hd ^ exp = fun (x : ℝ) ↦ basis_hd x ^ exp

Tactic:
rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
basis : Basis
h : ∀ (x : ℝ), toFun [] basis x = 1 x
⊢ toFun [] basis = 1

Tactic:
ext x
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
basis : Basis
x : ℝ
⊢ toFun [] basis x = 1 x

Tactic:
simp [toFun]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.toFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
m : UnitMonomial
h : ∀ (x : ℝ), m.toFun [] x = 1 x
⊢ m.toFun [] = 1

Tactic:
ext x
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
m : UnitMonomial
x : ℝ
⊢ m.toFun [] x = 1 x

Tactic:
simp [toFun]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.toFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
exp : ℝ
tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h : ∀ (x : ℝ), toFun (exp :: tl) (basis_hd :: basis_tl) x = (basis_hd ^ exp * tl.toFun basis_tl) x
⊢ toFun (exp :: tl) (basis_hd :: basis_tl) = basis_hd ^ exp * tl.toFun basis_tl

Tactic:
ext x
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
exp : ℝ
tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
x : ℝ
⊢ toFun (exp :: tl) (basis_hd :: basis_tl) x = (basis_hd ^ exp * tl.toFun basis_tl) x

Tactic:
simp [toFun]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.toFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
basis : Basis
h : ∀ (x : ℝ), toLogFun [] basis x = 0 x
⊢ toLogFun [] basis = 0

Tactic:
ext x
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
basis : Basis
x : ℝ
⊢ toLogFun [] basis x = 0 x

Tactic:
simp [toLogFun]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.toLogFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
m : UnitMonomial
h : ∀ (x : ℝ), m.toLogFun [] x = 0 x
⊢ m.toLogFun [] = 0

Tactic:
ext x
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
m : UnitMonomial
x : ℝ
⊢ m.toLogFun [] x = 0 x

Tactic:
simp [toLogFun]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.toLogFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
exp : ℝ
tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h : ∀ (x : ℝ), toLogFun (exp :: tl) (basis_hd :: basis_tl) x = (exp • log ∘ basis_hd + tl.toLogFun basis_tl) x
⊢ toLogFun (exp :: tl) (basis_hd :: basis_tl) = exp • log ∘ basis_hd + tl.toLogFun basis_tl

Tactic:
ext x
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
exp : ℝ
tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
x : ℝ
⊢ toLogFun (exp :: tl) (basis_hd :: basis_tl) x = (exp • log ∘ basis_hd + tl.toLogFun basis_tl) x

Tactic:
simp [toLogFun]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.toLogFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
m1 m2 : UnitMonomial
h : List.length m1 = List.length m2
⊢ List.length (m1.mul m2) = List.length m1

Tactic:
simp [mul, h]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.mul
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
m : UnitMonomial
⊢ List.length m.inv = List.length m

Tactic:
simp [inv]

Premises used: Tactic.ComputeAsymptotics.UnitMonomial.inv
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
m1 m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m1 = List.length m2
apply : ∀ (x : ℝ), (∀ f ∈ basis, 0 < f x) → (m1.mul m2).toFun basis x = (m1.toFun basis * m2.toFun basis) x
⊢ (m1.mul m2).toFun basis =ᶠ[atTop] m1.toFun basis * m2.toFun basis

Tactic:
apply h_basis.eventually_pos.mono

Premises used: Filter.Eventually.mono, Tactic.ComputeAsymptotics.WellFormedBasis.eventually_pos
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x : ℝ
m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length (α := ℝ) [] = List.length m2
h_pos : ∀ f ∈ basis, 0 < f x
⊢ List.length m2 = List.length (α := ℝ) []

Tactic:
symm at h_length
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x : ℝ
m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length (α := ℝ) [] = List.length m2
h_pos : ∀ f ∈ basis, 0 < f x
h_length₁ : List.length m2 = List.length (α := ℝ) []
⊢ ∀ f ∈ basis, 0 < f x

Tactic:
symm at h_length
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x : ℝ
m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m2 = List.length (α := ℝ) []
h_pos : ∀ f ∈ basis, 0 < f x
⊢ List.prod
      (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) [] m2) basis) =
    HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) [] basis))
      (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))

Tactic:
simp_all
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : exps1.length = List.length m2)
    (h_pos : ∀ f ∈ basis, 0 < f x),
    List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) exps1 m2)
          basis) =
      HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis))
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))
basis : Basis
h_basis : WellFormedBasis basis
h_pos : ∀ f ∈ basis, 0 < f x
h_length : (exp1 :: exps1).length = List.length (α := ℝ) []
⊢ List.prod
      (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp)
        (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) (exp1 :: exps1) []) basis) =
    HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (exp1 :: exps1) basis))
      (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) [] basis))

Tactic:
simp at h_length
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : exps1.length = List.length m2)
    (h_pos : ∀ f ∈ basis, 0 < f x),
    List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) exps1 m2)
          basis) =
      HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis))
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
h_basis : WellFormedBasis []
h_pos : ∀ (f : ℝ → ℝ), Membership.mem (γ := Basis) [] f → 0 < f x
⊢ List.prod
      (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp)
        (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) (exp1 :: exps1) (exp2 :: exps2)) []) =
    HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (exp1 :: exps1) []))
      (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (exp2 :: exps2) []))

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : exps1.length = List.length m2)
    (h_pos : ∀ f ∈ basis, 0 < f x),
    List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) exps1 m2)
          basis) =
      HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis))
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_pos : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
⊢ exps1.length = exps2.length

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : exps1.length = List.length m2)
    (h_pos : ∀ f ∈ basis, 0 < f x),
    List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) exps1 m2)
          basis) =
      HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis))
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_pos : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
⊢ exps1.length = exps2.length

Tactic:
have h1 : exps1.length = exps2.length := by grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : exps1.length = List.length m2)
    (h_pos : ∀ f ∈ basis, 0 < f x),
    List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) exps1 m2)
          basis) =
      HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis))
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_pos : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
h1 : exps1.length = exps2.length
⊢ ∀ f ∈ basis_tl, 0 < f x

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : exps1.length = List.length m2)
    (h_pos : ∀ f ∈ basis, 0 < f x),
    List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) exps1 m2)
          basis) =
      HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis))
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_pos : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
h1 : exps1.length = exps2.length
⊢ ∀ f ∈ basis_tl, 0 < f x

Tactic:
have h2 : ∀ f ∈ basis_tl, 0 < f x := by grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : exps1.length = List.length m2)
    (h_pos : ∀ f ∈ basis, 0 < f x),
    List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) exps1 m2)
          basis) =
      HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis))
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_pos : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
h1 : exps1.length = exps2.length
h2 : ∀ f ∈ basis_tl, 0 < f x
⊢ basis_hd ∈ basis_hd :: basis_tl

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : exps1.length = List.length m2)
    (h_pos : ∀ f ∈ basis, 0 < f x),
    List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) exps1 m2)
          basis) =
      HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis))
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_pos : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
h1 : exps1.length = exps2.length
h2 : ∀ f ∈ basis_tl, 0 < f x
⊢ 0 < basis_hd x

Tactic:
have h3 : 0 < basis_hd x := h_pos _ (by simp)
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis) (h_length : exps1.length = List.length m2)
    (h_pos : ∀ f ∈ basis, 0 < f x),
    List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) exps1 m2)
          basis) =
      HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis))
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_pos : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
h1 : exps1.length = exps2.length
h2 : ∀ f ∈ basis_tl, 0 < f x
h3 : 0 < basis_hd x
cons :
  basis_hd x ^ exp1 * basis_hd x ^ exp2 *
      HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis_tl))
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps2 basis_tl)) =
    basis_hd x ^ exp1 * List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis_tl) *
      (basis_hd x ^ exp2 * List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps2 basis_tl))
⊢ basis_hd x ^ (exp1 + exp2) *
      List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) exps1 exps2)
          basis_tl) =
    basis_hd x ^ exp1 * List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps1 basis_tl) *
      (basis_hd x ^ exp2 * List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps2 basis_tl))

Tactic:
rw [ih h_basis.tail h1 h2, Real.rpow_add h3]

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis.tail, Real.rpow_add