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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
⊢ dist
      (match some (a, c, b') with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b')))
      (match some (a, c, b') with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (g b'))) ≤
    2⁻¹ * dist f g

Tactic:
simp

Goal state after:
case some
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
⊢ dist (op c (f b')) (op c (g b')) ≤ dist f g
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

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

Tactic:
simp

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

Goal state before:
pp: case nil
h : WellFormedBasis []
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ [], 0 < f x

Tactic:
simp

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

Goal state before:
pp: case h.none
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
hb : F b = none
⊢ match none with
  | none =>
    (match none with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      nil
  | some (a, c, b') =>
    (match none with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      Seq.cons a
        (op c
          (match F b' with
          | none => nil
          | some (a, c, b') => Seq.cons a (op c (f b'))))

Tactic:
simp

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ basis_hd :: basis_tl ≠ []

Tactic:
simp

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

Goal state before:
pp: case h.some.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
⊢ f b' = T f b'

Tactic:
hf

Goal state after:
case h.some.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
⊢ f b' = f b'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
⊢ ∃ f,
    ∀ (b : β),
      match F b with
      | none => f b = nil
      | some (a, c, b') => f b = Seq.cons a (op c (f b'))

Tactic:
by
  let T : (β →ᵤ Seq α) → (β →ᵤ Seq α) := fun f b =>
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
  have hT : LipschitzWith 2⁻¹ T := by
    rw [lipschitzWith_iff_dist_le_mul]
    intro f g
    rw [UniformFun.dist_le (by positivity)]
    intro b
    simp only [UniformFun.toFun, UniformFun.ofFun, Equiv.coe_fn_symm_mk, NNReal.coe_inv,
      NNReal.coe_ofNat, T]
    cases F b with
    | none => simp
    | some v =>
      obtain ⟨a, c, b'⟩ := v
      simp
      calc
        _ ≤ dist (f b') (g b') := by
          have := h.friend c
          rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at this
          specialize this (f b') (g b')
          simpa using this
        _ ≤ _ := by
          simp only [UniformFun.dist_def]
          apply le_ciSup (f := fun b ↦ dist (f b) (g b))
          have : ∃ C, ∀ (a b : Seq α), dist a b ≤ C := by
            rw [← Metric.boundedSpace_iff]
            infer_instance
          obtain ⟨C, hC⟩ := this
          use C
          simp [upperBounds]
          grind
  obtain ⟨f, hf⟩ := exists_fixed_point_of_contractible T hT
  use f
  intro b
  rw [← hf]
  simp only [T]
  cases hb : F b with
  | none =>
    simp
  | some v =>
    obtain ⟨a, c, b'⟩ := v
    simp only [cons_eq_cons, true_and]
    congr
    change f b' = T f b'
    rw [hf]

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹ * dist s t
⊢ 2⁻¹ * dist s t ≤ 2⁻¹

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case nil.nil
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
⊢ nil.destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' nil.tail))
      (match nil.head with
      | none =>
        match nil.destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, ⟨fun x ↦ t_tl, ⋯⟩)
      | some s_hd =>
        match (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
simp

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

Goal state before:
pp: case nil.cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
x✝ : α
s✝ : Stream'.Seq α
⊢ (Seq.cons x✝ s✝).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' nil.tail))
      (match nil.head with
      | none =>
        match (Seq.cons x✝ s✝).destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, ⟨fun x ↦ t_tl, ⋯⟩)
      | some s_hd =>
        match (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
simp

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

Goal state before:
pp: case nil
basis : Basis
⊢ [].Sublist nil.getBasis

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case cons.nil.nil
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = nil
ht : op (Seq.cons s_hd s_tl) = nil
this : nil.head = nil.head
⊢ nil.destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s_tl))
      (match nil.destruct with
      | none => none
      | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
simp

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

Goal state before:
pp: case nil
c : ℝ
h_basis : WellFormedBasis []
⊢ (const [] c).Approximates

Tactic:
simp

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

Goal state before:
pp: c : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ (mk Multiseries.nil ((fun x ↦ c) - basis_hd ^ 0 * (const basis_tl c).toFun)).Approximates

Tactic:
simp

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

Goal state before:
pp: c : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ basis_hd ∈ basis_hd :: basis_tl

Tactic:
simp

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

Goal state before:
pp: case nil
r : ℝ
n : Fin [].length
h_basis : WellFormedBasis []
⊢ (monomialRpow [] (↑n) r).Approximates

Tactic:
simp

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

Goal state before:
pp: r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ (mk Multiseries.nil (basis_hd ^ r - basis_hd ^ r * one.toFun)).Approximates

Tactic:
simp

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

Goal state before:
pp: case h
basis_hd : ℝ → ℝ
basis_tl : Basis
op✝ : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑opf (↑op' s.tail)))
              (T s.head)
op : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h_op : motive op
T :
  Option (ℝ × MultiseriesExpansion basis_tl) →
    Option (ℝ × MultiseriesExpansion basis_tl × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Multiseries basis_hd basis_tl),
    destruct (op s) =
      Option.map
        (fun x ↦
          match x with
          | (exp, coef, opf, op') => (exp, coef, ↑opf (↑op' s.tail)))
        (T s.head)
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ Option.map
      (fun x ↦
        match x with
        | (exp, coef, tl) => ((exp, coef), tl))
      (Option.map
        (fun x ↦
          match x with
          | (exp, coef, opf, op') => (exp, coef, ↑opf (↑op' (tail s))))
        (T (head s))) =
    Option.map
      (fun x ↦
        match x with
        | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
      ((fun hd? ↦
          Option.map
            (fun x ↦
              match x with
              | (exp, coef, opf, op') => ((exp, coef), opf, op'))
            (T hd?))
        s.head)

Tactic:
simp

Goal state after:
case h
basis_hd : ℝ → ℝ
basis_tl : Basis
op✝ : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑opf (↑op' s.tail)))
              (T s.head)
op : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h_op : motive op
T :
  Option (ℝ × MultiseriesExpansion basis_tl) →
    Option (ℝ × MultiseriesExpansion basis_tl × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Multiseries basis_hd basis_tl),
    destruct (op s) =
      Option.map
        (fun x ↦
          match x with
          | (exp, coef, opf, op') => (exp, coef, ↑opf (↑op' s.tail)))
        (T s.head)
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ Option.map ((fun x ↦ ((x.1, x.2.1), x.2.2)) ∘ fun x ↦ (x.1, x.2.1, ↑x.2.2.1 (↑x.2.2.2 (tail s)))) (T (head s)) =
    Option.map ((fun x ↦ (x.1, ↑x.2.1 (↑x.2.2 s.tail))) ∘ fun x ↦ ((x.1, x.2.1), x.2.2)) (T s.head)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ basis_hd ∈ basis_hd :: basis_tl

Tactic:
simp

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

Goal state before:
pp: r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
m : Fin basis_tl.length
⊢ (mk Multiseries.nil (basis_tl[↑m] ^ r - basis_hd ^ 0 * (monomialRpow basis_tl (↑m) r).toFun)).Approximates

Tactic:
simp

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

Goal state before:
pp: r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
m : Fin basis_tl.length
⊢ basis_tl[↑m] ∈ basis_tl

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
s t : Stream'.Seq α
hn : dist s t ≤ 2⁻¹ ^ 0
⊢ dist (op s) (op t) ≤ 2⁻¹ ^ 0

Tactic:
simp

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

Goal state before:
pp: case e'_3
basis : Basis
n : ℕ
h : n < List.length basis
n' : Fin (List.length basis) := ⟨n, h⟩
⊢ basis[n] = basis[n'] ^ 1

Tactic:
simp

Goal state after:
case e'_3
basis : Basis
n : ℕ
h : n < List.length basis
n' : Fin (List.length basis) := ⟨n, h⟩
⊢ basis[n] = basis[↑n']
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis : Basis
n : Fin (List.length basis)
⊢ (monomial basis ↑n).toFun = basis[n]

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.nil
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis},
    WellFormedBasis basis →
      exps1.length = List.length m2 →
        (∀ f ∈ basis, 0 < f x) →
          (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) exps1 m2) basis).prod =
            (List.zipWith (fun exp b ↦ b x ^ exp) exps1 basis).prod *
              (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
h_basis : WellFormedBasis []
h_pos : ∀ f ∈ [], 0 < f x
⊢ (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) (exp1 :: exps1) (exp2 :: exps2)) []).prod =
    (List.zipWith (fun exp b ↦ b x ^ exp) (exp1 :: exps1) []).prod *
      (List.zipWith (fun exp b ↦ b x ^ exp) (exp2 :: exps2) []).prod

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis},
    WellFormedBasis basis →
      exps1.length = List.length m2 →
        (∀ f ∈ basis, 0 < f x) →
          (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) exps1 m2) basis).prod =
            (List.zipWith (fun exp b ↦ b x ^ exp) exps1 basis).prod *
              (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod
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

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

Goal state before:
pp: case h
basis_hd : ℝ → ℝ
basis_tl : Basis
op✝ : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
              (T s.head)
op : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h_op : motive op
T :
  Option (ℝ × MultiseriesExpansion basis_tl) →
    Option (ℝ × MultiseriesExpansion basis_tl × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Multiseries basis_hd basis_tl),
    destruct (op s) =
      Option.map
        (fun x ↦
          match x with
          | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ Option.map
      (fun x ↦
        match x with
        | (exp, coef, tl) => ((exp, coef), tl))
      (Option.map
        (fun x ↦
          match x with
          | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf (tail s))))
        (T (head s))) =
    Option.map
      (fun x ↦
        match x with
        | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
      ((fun hd? ↦
          Option.map
            (fun x ↦
              match x with
              | (exp, coef, opf, op') => ((exp, coef), opf, op'))
            (T hd?))
        s.head)

Tactic:
simp

Goal state after:
case h
basis_hd : ℝ → ℝ
basis_tl : Basis
op✝ : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
              (T s.head)
op : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h_op : motive op
T :
  Option (ℝ × MultiseriesExpansion basis_tl) →
    Option (ℝ × MultiseriesExpansion basis_tl × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Multiseries basis_hd basis_tl),
    destruct (op s) =
      Option.map
        (fun x ↦
          match x with
          | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ Option.map ((fun x ↦ ((x.1, x.2.1), x.2.2)) ∘ fun x ↦ (x.1, x.2.1, ↑x.2.2.2 (↑x.2.2.1 (tail s)))) (T (head s)) =
    Option.map ((fun x ↦ (x.1, ↑x.2.2 (↑x.2.1 s.tail))) ∘ fun x ↦ ((x.1, x.2.1), x.2.2)) (T s.head)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: 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.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) m1 m2) basis).prod =
    (List.zipWith (fun exp b ↦ b x ^ exp) m1 basis).prod * (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod

Tactic:
induction m1 generalizing m2 basis with

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case nil
basis : Basis
h_basis : WellFormedBasis basis
⊢ (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) []) basis).prod) =ᶠ[atTop] fun a ↦
    (List.zipWith (fun exp b ↦ b a ^ exp) [] basis).prod⁻¹

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.nil
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) exps) basis).prod) =ᶠ[atTop] fun a ↦
        (List.zipWith (fun exp b ↦ b a ^ exp) exps basis).prod⁻¹
h_basis : WellFormedBasis []
⊢ (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) (exp :: exps)) []).prod) =ᶠ[atTop] fun a ↦
    (List.zipWith (fun exp b ↦ b a ^ exp) (exp :: exps) []).prod⁻¹

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
h_length : [].length = List.length basis_tl
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ basis_hd ∈ basis_hd :: basis_tl

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: hd : ℝ
tl : List ℝ
ih :
  ∀ {basis_hd : ℝ → ℝ} {basis_tl : Basis},
    tl.length = List.length basis_tl → WellFormedBasis (basis_hd :: basis_tl) → Majorized (toFun tl basis_tl) basis_hd 0
basis_hd basis_tl_hd : ℝ → ℝ
basis_tl_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl_hd :: basis_tl_tl)
h_length : tl.length = basis_tl_tl.length
⊢ basis_tl_hd ∈ basis_tl_hd :: basis_tl_tl

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: hd : ℝ
tl : List ℝ
ih :
  ∀ {basis_hd : ℝ → ℝ} {basis_tl : Basis},
    tl.length = List.length basis_tl → WellFormedBasis (basis_hd :: basis_tl) → Majorized (toFun tl basis_tl) basis_hd 0
basis_hd basis_tl_hd : ℝ → ℝ
basis_tl_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl_hd :: basis_tl_tl)
h_length : tl.length = basis_tl_tl.length
exp : ℝ
h_exp : exp > 0
⊢ 1 > 0

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: hd : ℝ
tl : List ℝ
ih :
  ∀ {basis_hd : ℝ → ℝ} {basis_tl : Basis},
    tl.length = List.length basis_tl → WellFormedBasis (basis_hd :: basis_tl) → Majorized (toFun tl basis_tl) basis_hd 0
basis_hd basis_tl_hd : ℝ → ℝ
basis_tl_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl_hd :: basis_tl_tl)
h_length : tl.length = basis_tl_tl.length
exp : ℝ
h_exp : exp > 0
⊢ basis_tl_hd ∈ basis_tl_hd :: basis_tl_tl

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case nil
x : ℝ
basis : Basis
h_basis : WellFormedBasis basis
hx : ∀ f ∈ basis, 0 < f x
⊢ 0 < toFun [] basis x

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.nil
x exp : ℝ
exps : List ℝ
ih : ∀ {basis : Basis}, WellFormedBasis basis → (∀ f ∈ basis, 0 < f x) → 0 < toFun exps basis x
h_basis : WellFormedBasis []
hx : ∀ f ∈ [], 0 < f x
⊢ 0 < toFun (exp :: exps) [] x

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: x exp : ℝ
exps : List ℝ
ih : ∀ {basis : Basis}, WellFormedBasis basis → (∀ f ∈ basis, 0 < f x) → 0 < toFun exps basis x
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
hx : ∀ f ∈ basis_hd :: basis_tl, 0 < f x
⊢ basis_hd ∈ basis_hd :: basis_tl

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case nil
x : ℝ
basis : Basis
h_basis : WellFormedBasis basis
hx : ∀ f ∈ basis, 0 < f x
⊢ 0 < toFun [] basis x ∧ (log ∘ toFun [] basis) x = toLogFun [] basis x

Tactic:
simp

Goal state after: