Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
next : β
h : F b = some (exp, coef, c, next)
⊢ Seq.gcorec
      (fun a ↦
        Option.map
          (fun x ↦
            match x with
            | (exp, coef, c, next) => ((exp, coef), c, next))
          (F a))
      op b =
    cons exp coef
      (op c
        (Seq.gcorec
          (fun a ↦
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, c, next) => ((exp, coef), c, next))
              (F a))
          op next))

Tactic:
rw [Seq.gcorec_some]

Goal state after:
β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
next : β
h : F b = some (exp, coef, c, next)
⊢ Seq.cons ?m.36
      (op ?m.37
        (Seq.gcorec
          (fun a ↦
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, c, next) => ((exp, coef), c, next))
              (F a))
          op ?m.38)) =
    cons exp coef
      (op c
        (Seq.gcorec
          (fun a ↦
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, c, next) => ((exp, coef), c, next))
              (F a))
          op next))

β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
next : β
h : F b = some (exp, coef, c, next)
⊢ Option.map
      (fun x ↦
        match x with
        | (exp, coef, c, next) => ((exp, coef), c, next))
      (F b) =
    some (?m.36, ?m.37, ?m.38)

β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
next : β
h : F b = some (exp, coef, c, next)
⊢ ℝ × MultiseriesExpansion basis_tl

β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
next : β
h : F b = some (exp, coef, c, next)
⊢ γ

β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
next : β
h : F b = some (exp, coef, c, next)
⊢ β