awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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))

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))
basis : Basis
h_basis : WellFormedBasis basis
h_pos : ∀ f ∈ basis, 0 < f x
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
cons :
  ∀ (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) []))
cons₁ :
  ∀ (basis_hd : ℝ → ℝ) (basis_tl : List (ℝ → ℝ)) (h_basis : WellFormedBasis (basis_hd :: basis_tl))
    (h_pos : ∀ f ∈ basis_hd :: basis_tl, 0 < f x),
    List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp)
          (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) (exp1 :: exps1) (exp2 :: exps2)) (basis_hd :: basis_tl)) =
      HMul.hMul (α := ℝ)
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (exp1 :: exps1) (basis_hd :: basis_tl)))
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (exp2 :: exps2) (basis_hd :: basis_tl)))
⊢ List.prod
      (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp)
        (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) (exp1 :: exps1) (exp2 :: exps2)) 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) (exp2 :: exps2) basis))

Tactic:
cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      simp only [List.zipWith_cons_cons, List.prod_cons] at ih ⊢
      have h1 : exps1.length = exps2.length := by grind
      have h2 : ∀ f ∈ basis_tl, 0 < f x := by grind
      have h3 : 0 < basis_hd x := h_pos _ (by simp)
      rw [ih h_basis.tail h1 h2, Real.rpow_add h3]
      grind

Premises used: List.zipWith_cons_cons, List.prod_cons
-- 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))
m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : (exp1 :: exps1).length = List.length m2
h_pos : ∀ f ∈ basis, 0 < f x
cons :
  ∀ (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))
cons₁ :
  ∀ (exp2 : ℝ) (exps2 : List ℝ) (h_length : (exp1 :: exps1).length = (exp2 :: exps2).length),
    List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp)
          (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) (exp1 :: exps1) (exp2 :: exps2)) 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) (exp2 :: exps2) basis))
⊢ List.prod
      (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp)
        (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) (exp1 :: exps1) m2) 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) m2 basis))

Tactic:
cases m2 with
    | nil => simp at h_length
    | cons exp2 exps2 =>
    cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      simp only [List.zipWith_cons_cons, List.prod_cons] at ih ⊢
      have h1 : exps1.length = exps2.length := by grind
      have h2 : ∀ f ∈ basis_tl, 0 < f x := by grind
      have h3 : 0 < basis_hd x := h_pos _ (by simp)
      rw [ih h_basis.tail h1 h2, Real.rpow_add h3]
      grind

Premises used: List.zipWith_cons_cons, List.prod_cons
-- 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
x : ℝ
h_pos : ∀ f ∈ basis, 0 < f x
nil :
  ∀ {m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis)
    (h_length : List.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) [] 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))
cons :
  ∀ (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)))
    {m2 : UnitMonomial} {basis : Basis} (h_basis : WellFormedBasis basis)
    (h_length : (exp1 :: 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) (exp1 :: exps1) m2) 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) m2 basis))
⊢ List.prod
      (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) m1 m2) basis) =
    HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m1 basis))
      (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))

Tactic:
induction m1 generalizing m2 basis with
  | nil =>
    symm at h_length
    simp_all
  | cons exp1 exps1 ih =>
    cases m2 with
    | nil => simp at h_length
    | cons exp2 exps2 =>
    cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      simp only [List.zipWith_cons_cons, List.prod_cons] at ih ⊢
      have h1 : exps1.length = exps2.length := by grind
      have h2 : ∀ f ∈ basis_tl, 0 < f x := by grind
      have h3 : 0 < basis_hd x := h_pos _ (by simp)
      rw [ih h_basis.tail h1 h2, Real.rpow_add h3]
      grind

Premises used: List.zipWith_cons_cons, List.prod_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
basis : Basis
h_basis : WellFormedBasis basis
⊢ EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) []) basis))
    fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) [] basis))⁻¹

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis))⁻¹
h_basis : WellFormedBasis []
⊢ EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps)) []))
    fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) []))⁻¹

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis))⁻¹
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
cons :
  ∀ (x : ℝ),
    0 < basis_hd x ∧
        Eq (α := ℝ)
          ((fun (a : ℝ) ↦
              (List.prod
                  (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis_tl) :
                ℝ))
            x)
          ((fun (a : ℝ) ↦ ((List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis_tl))⁻¹ : ℝ)) x) →
      Eq (α := ℝ)
        ((fun (a : ℝ) ↦
            (List.prod
                (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps))
                  (basis_hd :: basis_tl)) :
              ℝ))
          x)
        ((fun (a : ℝ) ↦
            ((List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)))⁻¹ :
              ℝ))
          x)
⊢ EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps))
          (basis_hd :: basis_tl)))
    fun (a : ℝ) ↦
    (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)))⁻¹

Tactic:
apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis.head_eventually_pos, Tactic.ComputeAsymptotics.WellFormedBasis.tail, Filter.Eventually.and, Filter.Eventually.mono
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis))⁻¹
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
x : ℝ
cons :
  ∀ (h_pos : 0 < basis_hd x)
    (ih :
      Eq (α := ℝ)
        ((fun (a : ℝ) ↦
            (List.prod
                (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis_tl) :
              ℝ))
          x)
        ((fun (a : ℝ) ↦ ((List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis_tl))⁻¹ : ℝ)) x)),
    Eq (α := ℝ)
      ((fun (a : ℝ) ↦
          (List.prod
              (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps))
                (basis_hd :: basis_tl)) :
            ℝ))
        x)
      ((fun (a : ℝ) ↦
          ((List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)))⁻¹ :
            ℝ))
        x)
⊢ 0 < basis_hd x ∧
      Eq (α := ℝ)
        ((fun (a : ℝ) ↦
            (List.prod
                (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis_tl) :
              ℝ))
          x)
        ((fun (a : ℝ) ↦ ((List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis_tl))⁻¹ : ℝ)) x) →
    Eq (α := ℝ)
      ((fun (a : ℝ) ↦
          (List.prod
              (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps))
                (basis_hd :: basis_tl)) :
            ℝ))
        x)
      ((fun (a : ℝ) ↦
          ((List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)))⁻¹ :
            ℝ))
        x)

Tactic:
⟨h_pos, ih⟩
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
exp : ℝ
exps : List ℝ
ih_1 :
  ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis))⁻¹
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
x : ℝ
h_pos : 0 < basis_hd x
ih :
  Eq (α := ℝ)
    ((fun (a : ℝ) ↦
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis_tl) :
          ℝ))
      x)
    ((fun (a : ℝ) ↦ ((List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis_tl))⁻¹ : ℝ)) x)
cons :
  basis_hd x ^ (-exp) *
      List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis_tl) =
    (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps basis_tl))⁻¹ * (basis_hd x ^ exp)⁻¹
⊢ Eq (α := ℝ)
    ((fun (a : ℝ) ↦
        (List.prod
            (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps))
              (basis_hd :: basis_tl)) :
          ℝ))
      x)
    ((fun (a : ℝ) ↦
        ((List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)))⁻¹ : ℝ))
      x)

Tactic:
simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]

Premises used: List.map_cons, List.zipWith_cons_cons, mul_inv_rev, List.prod_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
exp : ℝ
exps : List ℝ
ih_1 :
  ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis))⁻¹
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
x : ℝ
h_pos : 0 < basis_hd x
ih :
  Eq (α := ℝ)
    ((fun (a : ℝ) ↦
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis_tl) :
          ℝ))
      x)
    ((fun (a : ℝ) ↦ ((List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis_tl))⁻¹ : ℝ)) x)
⊢ basis_hd x ^ (-exp) *
      List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis_tl) =
    (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps basis_tl))⁻¹ * (basis_hd x ^ exp)⁻¹

Tactic:
grind [Real.rpow_neg h_pos.le]

Premises used: LT.lt.le, Real.rpow_neg
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis))⁻¹
basis : Basis
h_basis : WellFormedBasis basis
cons :
  ∀ (h_basis : WellFormedBasis []),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps)) []))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) []))⁻¹
cons₁ :
  ∀ (basis_hd : ℝ → ℝ) (basis_tl : List (ℝ → ℝ)) (h_basis : WellFormedBasis (basis_hd :: basis_tl)),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod
          (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps))
            (basis_hd :: basis_tl)))
      fun (a : ℝ) ↦
      (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)))⁻¹
⊢ EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps)) basis))
    fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) basis))⁻¹

Tactic:
cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono
      intro x ⟨h_pos, ih⟩
      simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]
      grind [Real.rpow_neg h_pos.le]

Premises used: List.map_cons, List.zipWith_cons_cons, mul_inv_rev, List.prod_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
nil :
  ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) []) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) [] basis))⁻¹
cons :
  ∀ (exp : ℝ) (exps : List ℝ)
    (ih :
      ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
        EventuallyEq (β := ℝ) atTop
          (fun (a : ℝ) ↦
            List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis))
          fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis))⁻¹)
    {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod
          (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps)) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) basis))⁻¹
⊢ EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) m) basis))
    fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) m basis))⁻¹

Tactic:
induction m generalizing basis with
  | nil => simp
  | cons exp exps ih =>
    cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono
      intro x ⟨h_pos, ih⟩
      simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]
      grind [Real.rpow_neg h_pos.le]

Premises used: List.map_cons, Real.exp, List.zipWith_cons_cons, mul_inv_rev, List.prod_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
coef : ℝ
basis : Basis
h : ∀ (x : ℝ), { coef := coef, unit := [] : Monomial }.toFun basis x = coef
⊢ { coef := coef, unit := [] : Monomial }.toFun basis = fun (x : ℝ) ↦ coef

Tactic:
ext x
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
coef : ℝ
basis : Basis
x : ℝ
⊢ { coef := coef, unit := [] : Monomial }.toFun basis x = coef

Tactic:
simp [toFun]

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

Tactic:
ext x
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
coef exp : ℝ
m : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
x : ℝ
h : coef * (basis_hd x ^ exp * m.toFun basis_tl x) = basis_hd x ^ exp * (coef * m.toFun basis_tl x)
⊢ { coef := coef, unit := exp :: m : Monomial }.toFun (basis_hd :: basis_tl) x =
    (basis_hd ^ exp * { coef := coef, unit := m : Monomial }.toFun basis_tl) x

Tactic:
simp [toFun]

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

Tactic:
ring
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
basis : Basis
h_coef : t.coef = 0
⊢ t.toFun basis = 0

Tactic:
simp [toFun, h_coef]

Premises used: Tactic.ComputeAsymptotics.Monomial.toFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
basis : Basis
exps : List ℝ
⊢ { coef := 0, unit := exps : Monomial }.toFun basis = 0

Tactic:
zero_coef_toFun _ rfl

Premises used: Tactic.ComputeAsymptotics.Monomial.zero_coef_toFun, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
basis : Basis
h : ∀ (x : ℝ), t.toFun basis x = (-t.neg.toFun basis) x
⊢ t.toFun basis = -t.neg.toFun basis

Tactic:
ext x
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t : Monomial
basis : Basis
x : ℝ
⊢ t.toFun basis x = (-t.neg.toFun basis) x

Tactic:
simp [neg, toFun]

Premises used: Tactic.ComputeAsymptotics.Monomial.neg, Tactic.ComputeAsymptotics.Monomial.toFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Goal:
t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
simp :
  (t1.coef * t2.coef) • (t1.unit.mul t2.unit).toFun basis =ᶠ[atTop]
    t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)
⊢ (t1.mul t2).toFun basis =ᶠ[atTop] t1.toFun basis * t2.toFun basis

Tactic:
simp only [toFun, mul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]

Premises used: Algebra.mul_smul_comm, Tactic.ComputeAsymptotics.Monomial.toFun, Tactic.ComputeAsymptotics.Monomial.mul, Algebra.smul_mul_assoc