awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (hypothesis)
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
⊢ 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))
have h1 : exps1.length = exps2.length
Tactic: have h1 : exps1.length = exps2.length := by grind
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (hypothesis)
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
⊢ 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))
have h2 : ∀ f ∈ basis_tl, 0 < f x
Tactic: have h2 : ∀ f ∈ basis_tl, 0 < f x := by grind
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (hypothesis)
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 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))
have h3 : 0 < basis_hd x
Tactic: have h3 : 0 < basis_hd x := h_pos _ (by simp)
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
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 + 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))
have 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))
Tactic: rw [ih h_basis.tail h1 h2, Real.rpow_add h3]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
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
⊢ 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))
have 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) []))
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
Cleared hypotheses: basis, h_basis, h_pos
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
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) []))
⊢ 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))
have 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)))
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
Cleared hypotheses: basis, h_basis, h_pos
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
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
⊢ 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))
have 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))
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
Cleared hypotheses: m2, h_length
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
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))
⊢ 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))
have 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))
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
Cleared hypotheses: m2, h_length
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
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
⊢ 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))
have 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))
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
Cleared hypotheses: m1, m2, basis, h_basis, h_length, h_pos
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
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))
⊢ 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))
have 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))
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
Cleared hypotheses: m1, m2, basis, h_basis, h_length, h_pos
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
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)
⊢ 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)))⁻¹
have 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)
Tactic: apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
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 : ℝ
⊢ 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)
have 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)
Tactic: ⟨h_pos, ih⟩