{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℂ E] →
      {motive : WeakFEPair E → Sort u} →
        (t : WeakFEPair E) →
          ((f g : ℝ → E) →
              (k : ℝ) →
                (ε : ℂ) →
                  (f₀ g₀ : E) →
                    (hf_int : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) →
                      (hg_int : MeasureTheory.LocallyIntegrableOn g (Set.Ioi 0) MeasureTheory.volume) →
                        (hk : 0 < k) →
                          (hε : ε ≠ 0) →
                            (h_feq : ∀ x ∈ Set.Ioi 0, f (1 / x) = (ε * ↑(x ^ k)) • g x) →
                              (hf_top : ∀ (r : ℝ), (fun x => f x - f₀) =O[Filter.atTop] fun x => x ^ r) →
                                (hg_top : ∀ (r : ℝ), (fun x => g x - g₀) =O[Filter.atTop] fun x => x ^ r) →
                                  motive
                                    { f := f, g := g, k := k, ε := ε, f₀ := f₀, g₀ := g₀, hf_int := hf_int,
                                      hg_int := hg_int, hk := hk, hε := hε, h_feq := h_feq, hf_top := hf_top,
                                      hg_top := hg_top }) →
            motive t