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)
⊢ (op s).destruct =
    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:
rw [destruct_eq_destruct_map, hT s]

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 ↦
        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)