Rewrite inside IsLittleO

Stream: mathlib4

[Ian Jauslin]

Hello!
I'm trying to perform a rewrite inside an IsLittleO statement. For the sake of example, let's say I had two functions f and g, and I knew that f(h)=g(h). Suppose I also knew that f(h)=o(h) and wanted to prove that g(h)=o(h). I would like to rewrite g(h) in the goal, but it's not so easy because h is not a variable. I figured out how to do this with conv, but it doesn't seem very efficient... How should I do this?

Here is the example code with my inefficient solution.

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Asymptotics.Asymptotics

example (f g : ℂ → ℂ) (hfg : ∀ h, g h = f h) :
    Asymptotics.IsLittleO (nhds 0) (fun h ↦ f h) (fun h ↦ h)
    → Asymptotics.IsLittleO (nhds 0) (fun h ↦ g h) (fun h ↦ h) := by
  intro ho
  conv =>
    lhs
    intro h
    rw [hfg h]
  exact ho

[Eric Rodriguez]

For the case you mention, docs#funext and then the rewrite should work

[Ian Jauslin]

I see, thank you! I did rw[funext hfg] and that works perfectly. Thanks!

[David Loeffler]

simp_rw [hfg] also works.