Unable to `rw` iff lemmas

Stream: new members

[Gareth Ma]

Why does the first fail and second not?

import Mathlib.Analysis.SpecialFunctions.Pow.Real

set_option autoImplicit false

open Nat hiding log sqrt
open Real Filter Asymptotics Topology

example (f : ℕ → ℝ) : f =o[atTop] (1 : ℕ → ℝ) := by
  /- rw [isLittleO_one_iff] /- fails -/ -/
  apply (isLittleO_one_iff _).mpr

[Ruben Van de Velde]

Because the lemma is about fun _ => 1 and your example is about 1 : _ → _

[Ruben Van de Velde]

Those are equal, but not syntactically so

[Ruben Van de Velde]

import Mathlib.Analysis.SpecialFunctions.Pow.Real

set_option autoImplicit false

open Nat hiding log sqrt
open Real Filter Asymptotics Topology

example (f : ℕ → ℝ) : f =o[atTop] (1 : ℕ → ℝ) := by
  rw [Pi.one_def]
  rw [isLittleO_one_iff]
  sorry

[Gareth Ma]

Which one is preferred in Mathlib?

[Ruben Van de Velde]

I have one data point here and that is isLittleO_one_iff :)