FIlter.Tendsto atTop Help on Proof

Stream: new members

[Colin Jones ⚛️]

I need help on this proof.

import Mathlib

open BigOperators
open Filter
open Nat

variable (a b : ℝ)

example (ha : 0 < a) (hb : 0 < b) :
  Tendsto (fun x => ((1 - a * x) * (1 - a * x + b * x))⁻¹)
  (nhdsWithin a⁻¹ (Set.Ioo 0 a⁻¹)) atTop := by
  rw [tendsto_atTop]
  sorry

[Filippo A. E. Nuccio]

Are you aware of docs#Filter.eventually_iff and mem_nhdsWithin_iff_exists_mem_nhds_inter? What is your pen-and-paper proof?

[Colin Jones ⚛️]

When I plug in 1/a into the function the denominator becomes zero, therefore the function tends towards infinity. That's what I believe the atTop stands for. However, I don't know how to implement that logic in Lean 4.

In fact I am unable to prove a similar but simpler problem involving the function f(x) = 1/x.

import Mathlib

open BigOperators
open Filter
open Nat

variable (a b : ℝ)

example :
  Tendsto (fun x => 1/x) (nhdsWithin 0 (Set.Ioo (-1:ℝ) 0)) atTop := by
  refine tendsto_nhdsWithin_of_tendsto_nhds ?h
  apply?

I would think that this problem is easily solvable and would only take aesop? or apply? to solve.

[Colin Jones ⚛️]

I managed to get the second example to showing that y is an element of s.

import Mathlib

open BigOperators
open Filter
open Nat

variable (a b : ℝ)

example :
  Tendsto (fun x => 1/x) (nhdsWithin 0 (Set.Ioo (-1:ℝ) 0)) atTop := by
  refine tendsto_nhdsWithin_of_tendsto_nhds ?h
  aesop?
  refine tendsto_iff_forall_eventually_mem.mpr ?h.a
  refine fun s a => ?_
  refine Metric.eventually_nhds_iff.mpr ?h.a.a
  use 1
  norm_num
  intro y
  intro H
  apply?

But, I don't know how to proceed.

[Colin Jones ⚛️]

Would this be correct or wrong because Lean treats 1/0 as 0?

[Patrick Massot]

This has nothing to do with 1/0, your statement is wrong because atTop should be atBot.

[Patrick Massot]

Even with the correct statement, your very first line of proof reduces the proof to showing something that is wrong.

[Patrick Massot]

You need to search online for a graph of the function $x ↦ 1/x$ to see what it does near zero.

[Colin Jones ⚛️]

Okay I see where I went wrong. Can someone confirm my understanding?

atTop means it's tending to positive infinity? And, atBot means it's tending to negative infinity?

My understanding of nhdsWithin 0 (Set.Ioo (-1:ℝ) 0) was that 1/x was going to zero. Is this also correct?

[Colin Jones ⚛️]

Sorry not an rigorous mathematician just an engineer

[Patrick Massot]

Yes, atBot means negative infinity. I’m not sure what you are trying to say with the next sentence but it certainly doesn’t sound correct.

[Luigi Massacci]

Colin Jones ⚛️ said:

My understanding of nhdsWithin 0 (Set.Ioo (-1:ℝ) 0) was that 1/x was going to zero. Is this also correct?

If you mean that x (not 1/x) is going to zero (from the left) then yes. Have you read #mil ? It might help

[Colin Jones ⚛️]

Okay I figured out one of them.

example :
  Tendsto (fun (x : ℝ) => 1/x) (nhdsWithin 0 (Set.Ioo 0 1)) atTop := by
  simp only [one_div]
  aesop
  exact tendsto_inv_zero_atTop

[Colin Jones ⚛️]

Luigi Massacci said:

Colin Jones ⚛️ said:

My understanding of nhdsWithin 0 (Set.Ioo (-1:ℝ) 0) was that 1/x was going to zero. Is this also correct?

If you mean that x (not 1/x) is going to zero (from the left) then yes. Have you read #mil ? It might help

Thank you. When I tried to read MIL, I didn't understand a lot of it, but I think I'll check it out again.

[Luigi Massacci]

I don't know if there's such a thing as "too much aesop" but that might be it. Here's what I would have done:

example :
  Tendsto (fun (x : ℝ) => 1/x) (nhdsWithin 0 (Set.Ioo 0 1)) atTop := by
  simp only [one_div]
  apply (tendsto_nhdsWithin_mono_left Set.Ioo_subset_Ioi_self tendsto_inv_zero_atTop)

unfortunately you can't use "?" when aesop is non-finishing, but you can use show_term instead:

example :
  Tendsto (fun (x : ℝ) => 1/x) (nhdsWithin 0 (Set.Ioo 0 1)) atTop := by
  simp only [one_div]
  show_term aesop
  exact tendsto_inv_zero_atTop

Modulo some machine stuff, the relevant lemma it's applying is only nhdsWithin_Ioo_eq_nhdsWithin_Ioi, so you can erase the (almost) pointless aesop call this way, for example:

example :
  Tendsto (fun (x : ℝ) => 1/x) (nhdsWithin 0 (Set.Ioo 0 1)) atTop := by
  simp only [one_div]
  rw [nhdsWithin_Ioo_eq_nhdsWithin_Ioi zero_lt_one]
  exact tendsto_inv_zero_atTop

having said that, I don't know why you wanted this theorem, but if it's as an exercise, I'd say you are cheating: tendsto_inv_zero_atTop is essentially what you have to prove. You just proved that "1/x → +∞ as x → 0⁺ (with x < 1)" by using "1/x → +∞ as x → 0⁺ ". Up to you to decided if that is morally sound

[Colin Jones ⚛️]

Yes I figured that out too. I'm okay with proving the theorem that way as long as I'm using Mathlib as the source.

The main problem is this proof:

import Mathlib

open BigOperators
open Filter
open Nat
open Set

variable (a b : ℝ)

example (ha : 0 < a) (hb : 0 < b) :
  Tendsto (fun (x:ℝ) => ((1 - a * x) * (1 - a * x + b * x))⁻¹)
         (nhdsWithin (a⁻¹) (Ioo 0 (a⁻¹))) atTop := by sorry

Which I just cannot figure out? Can someone help solve this goal for me?

[Colin Jones ⚛️]

It should be written correctly too as 1/[(1 - ax)(1 - ax + bx)] does tend towards positive infinity from the left of 1/a.

[Colin Jones ⚛️]

I made some progress but am unsure of what open set I should use to prove the above

import Mathlib

open BigOperators
open Filter
open Nat
open Set

variable (a b : ℝ)

example (ha : 0 < a) (hb : 0 < b) :
  Tendsto (fun (x:ℝ) => (1 - a * x)⁻¹)
         (nhdsWithin (a⁻¹) (Ioo 0 (a⁻¹))) atTop := by
  rw [nhdsWithin_Ioo_eq_nhdsWithin_Iio]
  rw [@tendsto_atTop]
  intro C
  rw [@eventually_nhdsWithin_iff]
  rw [@eventually_nhds_iff]
  use Set.Ioo 0 C⁻¹
  constructor
  intro x hx hx1
  have h : 0 < x ∧ x < C⁻¹ := by aesop
  obtain ⟨h1, h2⟩ := h
sorry

[Kevin Buzzard]

At the sorry you have 3 goals. This is not how Lean code should look. Every time the number of goals becomes greater than 1 you should put these dots \. and start working in different "threads", one per goal.

You seem to be working on the first goal, but the local context for your second goal is this:

a b : ℝ
ha : 0 < a
hb : 0 < b
C : ℝ
⊢ IsOpen (Ioo 0 C⁻¹) ∧ a⁻¹ ∈ Ioo 0 C⁻¹

So this says "let a and b be arbitrary positive real numbers and let C be an arbitrary real number (here "arbitrary" means "we don't know anything about it other than the fact that it's a real number"). Then (something), and 0<a^{-1}<C^{-1}". This is clearly not true because for example we could have a=1 and C=-1, or a=0.000000000001 and C=37 or whatever. So at some point in your proof you've taken a wrong turn. Also, you seem to have a b which plays no role anywhere.

I am not an expert on how to manipulate neighbourhoods in Lean, they don't really show up in my code. But my understanding of the statement you've written is that it says that as $x$ tends to $1/a$ from below, then $1/(1-ax)$ tends to $+\infty$ and this sounds right ($ax$ will be tending to $1$ from below, so $1-ax$ will be tending to $0$ from above, so its reciprocal will be tending to $+\infty$. So at some point you've applied a tactic which turned a correct thing into an incorrect thing.

I'm just thinking aloud here. Looking at the proof, the rewrites are unlikely to be the problem, because you can usually just rewrite backwards to get back to where you came from, and you can't go from false to true. And the intro won't be the problem either because that's also a reversible tactic. So it's going to be the use, right? That looks highly suspicious because if C is negative then Set.Ioo 0 C⁻¹ is going to be the empty set so a⁻¹ ∈ Ioo 0 C⁻¹ is never going to be true. At this point you already have two goals (so you've already committed a style sin) so let's go back to see where that appeared.

OK the second goal appeared in the first line of your proof, because you didn't provide a proof that $a^{-1}>0$. So you could replace the first line of your proof with

  rw [nhdsWithin_Ioo_eq_nhdsWithin_Iio (by positivity)]

and now you only have one goal. Now let's get back to this use.

[Kevin Buzzard]

Deleting the junk b, at this point the tactic state is

a : ℝ
ha: 0 < a
C : ℝ
⊢ ∃ t, (∀ x ∈ t, x ∈ Iio a⁻¹ → C ≤ (1 - a * x)⁻¹) ∧ IsOpen t ∧ a⁻¹ ∈ t

So you need to use a set t with the following three properties:
(3) $a^{-1}\in t$;
(2) $t$ is open;
(1) Every element of $t$ which is less than $a^{-1}$ has the property that $C\leq 1/(1-ax).$

[Kevin Buzzard]

(sorry for multiple messages, I seem to have hit a Zulip bug?)

[Kevin Buzzard]

From my mental picture, this open set is going to be of the form $(p.q)$ (to satisfy (2)), where
(a) $p$ is going to be positive and very very close to, but less than, $a^{-1}$ (to satisfy (1)), and
(b) $q$ is going to be anything at all bigger than $a^{-1}$ (to satisfy (3)).

[Kevin Buzzard]

(huh, the next para of my message refuses to send!) Bug reported here

[Kevin Buzzard]

So $q$ can just be $a^{-1}+1$, and the big question is how to make (a) work. Because $1/(1-ax)$ is getting bigger as $x$ increases to $a$ from below, if we can make sure that $C\leq 1/(1-ap)$ then this is going to work. Because $p$ is just a tiny bit less than $a^{-1}$, $ap$ will be a tiny bit less than 1, so $(1-ap)$ will be positive, so we can multiply both sides by $(1-ap)$ and reduce our problem to finding a $p$ such that $C(1-ap)\leq 1$.

[Kevin Buzzard]

Doing the algebra we see $C-Cap\leq 1$ so $C-1\leq Cap$ and now we have to be a bit careful because we want to divide by $C$ to isolate $p$ but don't know the sign of $C$ so we can't control the inequality.

[Kevin Buzzard]

Oh, I guess if $C\leq 0$ then we already won, because if $0<p<a^{-1}$ then $(1-ap)$ will be positive so $C(1-ap)$ will be $\leq 0$ and so certainly $\leq 1$. But if $C>0$ then we have to think some more, because if $C$ is a million billion trillion then we need to guarantee that $(1-ap)$ is tiny to make up for it. Let's go back to $C-1\leq Cap$ and divide through by $Ca$ to get $p\geq (C-1)/Ca$.

[Kevin Buzzard]

So you want to define $p$ to be $a^{-1}/2$ if $C\leq 1$ and $(C-1)/Ca$ if $C>1$ and then everything should work.

As I say, I don't work with filters like this at all and I kind of feel like your proof is making leaps and bounds in the wrong direction. I thought the whole point of filters was to spare us from having to do this kind of thing. But I might be wrong -- you might have to ultimately end up doing this kind of calculation however you approach it (you shouldn't have to do though, you should just be using stuff like monotonicity etc I suspect). I also feel like there should be a tactic to do all of this; if you guys are sitting on some cash then you might want to hire someone who has more of a maths background and can write a bespoke tactic which will prove these kinds of examples for you automatically. It might be a great project for a computer science undergraduate, for example.

[Colin Jones ⚛️]

Thank you for your response, Kevin. I do wish there was a tactic to do this all. I did complete the proof but it is extraordinarily long, although, hopefully a little organized and readable.

I changed the approach from which I did the proof and instead of sets used the Metric.eventually_nhds_iff way.

import Mathlib

open BigOperators
open Filter
open Nat
open Set

variable (a b : ℝ)

example (ha : 0 < a) :
  Tendsto (fun (x:ℝ) => (1 - a * x)⁻¹)
         (nhdsWithin (a⁻¹) (Ioo 0 (a⁻¹))) atTop := by
  have a_inv_a : a*a⁻¹ = 1 := by
    rw [← division_def]
    exact div_self (ne_of_gt ha)
  rw [nhdsWithin_Ioo_eq_nhdsWithin_Iio (by positivity)]
  rw [@tendsto_atTop]
  intro b
  rw [@eventually_nhdsWithin_iff]
  rw [@Metric.eventually_nhds_iff]
  have hb : b ≤ 0 ∨ 0 < b := by exact le_or_lt b 0
  rcases hb with hb1 | hb2
  · use 3
    norm_num
    intro y hy hy1
    have step1 : a*y < 1 := by
      calc
        a*y < a*a⁻¹ := by rel [hy1]
        _   = 1 := by rw [← division_def]; assumption
    have step2 : 1 - a*y > 0 := by
      rename_i b_1
      simp_all only [gt_iff_lt, sub_pos]
    have step3 : 0 < (1 - a*y)⁻¹ := by
      rename_i b_1
      simp_all only [gt_iff_lt, sub_pos, inv_pos]
    linarith
  · use a⁻¹*b⁻¹
    constructor
    rename_i b_1
    simp_all only [one_div, mul_inv_rev, gt_iff_lt, inv_pos, mul_pos_iff_of_pos_left]
    intro y hy hy1
    dsimp [Dist.dist] at hy
    rw [abs_sub_lt_iff] at hy
    rcases hy with ⟨hl, hr⟩
    have hr' : -y < a⁻¹*b⁻¹ - a⁻¹ := by
      rw [lt_sub_iff_add_lt, add_comm]
      rw [Mathlib.Tactic.RingNF.add_neg]
      exact hr
    have hr' : a⁻¹ - a⁻¹*b⁻¹ < y := by
      rw [← neg_neg y, ← lt_neg]
      rename_i b_1
      simp_all only [mem_Iio, neg_lt_sub_iff_lt_add, neg_sub]
    have step_a : a*(a⁻¹ - a⁻¹*b⁻¹) = 1 - b⁻¹ := by
      rw [mul_sub]
      rw [a_inv_a]
      simp only [sub_right_inj]
      rw [← mul_assoc]
      rename_i b_1 hr'_1
      simp_all only [mem_Iio, neg_lt_sub_iff_lt_add, one_mul]
    have step_y : 0 < 1-a*y := by
      aesop
      rw [← propext (lt_div_iff' ha)]
      rw [one_div]
      assumption
    have step1 : 1 - b⁻¹ < a*y := by
      rw [← step_a]
      exact (mul_lt_mul_left ha).mpr hr'
    have step2 : -a*y < -(1 - b⁻¹) := by
      rw [← neg_neg (a*y), lt_neg] at step1
      simp_all only [mem_Iio, neg_lt_sub_iff_lt_add, sub_pos, neg_sub, neg_mul]
    have step3 : 1 - a*y < b⁻¹ := by
      rw [show 1 - a*y < b⁻¹ ↔ - a*y < -1 + b⁻¹ by simp only [neg_mul, lt_neg_add_iff_add_lt, add_neg_lt_iff_lt_add]; exact
        sub_lt_iff_lt_add]
      rw [show -(1 - b⁻¹) = -1 + b⁻¹ by ring] at step2
      assumption
    have step4 : (1 - a*y)⁻¹ > b := by
      rw [show 1 - a*y < b⁻¹ ↔ 1/b⁻¹ < 1/(1-a*y) by exact Iff.symm (_root_.one_div_lt_one_div (inv_pos.mpr hb2) step_y)] at step3
      rw [div_inv_eq_mul, one_mul, one_div] at step3
      assumption
    exact LT.lt.le step4

[Kevin Buzzard]

My guess is that there will be an extremely short proof of the form: as x tends to a^-1 from below, ax tends to 1 from below, so 1-ax tends to 0 from above, so 1/(1-ax) tends to +infty. That would be how I'd attempt to prove your theorem although as I say I don't know my way around this part of the library. My approach seems far less painful than yours though.

[Colin Jones ⚛️]

Yes that would be a lot nicer to prove, but I haven't found a way to do switch the goal to something analogous to 1/x goes to infinity from the right of zero

[Colin Jones ⚛️]

I found a theorem that switches atTop to proving the inverse of the function tends to zero, but it won't let me apply it to the goal statement (unsurprisingly because apply? couldn't find it).

import Mathlib

open BigOperators
open Filter
open Nat
open Set

variable (a b : ℝ)

example (ha : 0 < a) :
  Tendsto (fun (x:ℝ) => (1 - a * x)⁻¹)
         (nhdsWithin (a⁻¹) (Ioo 0 (a⁻¹))) atTop := by

    apply Filter.Tendsto.inv_tendsto_atTop

[Colin Jones ⚛️]

Oh wait I'm silly the theorem only goes one way.

[Colin Jones ⚛️]

Okay I found the way to essentially turn the goal into (1 - ax) tends to zero as x -> 1/a

example (ha : 0 < a) :
  Tendsto (fun (x:ℝ) => (1 - a * x)⁻¹)
         (nhdsWithin (a⁻¹) (Ioo 0 (a⁻¹))) atTop := by
    have abs_a : |a| = a := by exact abs_of_pos ha
    refine Filter.Tendsto.inv_tendsto_zero ?_
    refine Metric.tendsto_nhdsWithin_nhdsWithin.mpr ?_
    intro e he
    dsimp [Dist.dist]
    norm_num
    use e / a
    constructor
    exact div_pos he ha
    intro x hx hx1 hx2
    constructor
    · calc
        a*x < a*a⁻¹ := by gcongr
        _   = 1 := by rw [show a*a⁻¹ = a/a by ring]; exact div_self (ne_of_gt ha)
    · rw [@abs_sub_comm]
      rw [show |x - a⁻¹| < e / a ↔ a*|x - a⁻¹| < a*(e / a) by exact Iff.symm (mul_lt_mul_left ha)] at hx2
      rw [show a*(e/a) = e by rw [@mul_div_left_comm]; rw [div_self (ne_of_gt ha)]; rw [mul_one]] at hx2
      rw [show a * |x - a⁻¹| < e ↔ |a*(x - a⁻¹)| < e by rw [abs_mul, abs_a]] at hx2
      rw [show |a*(x - a⁻¹)| < e ↔ |a*x - a*a⁻¹| < e by rw [mul_sub]] at hx2
      rw [show 1 = a*a⁻¹ by rw [← one_div]; rw [mul_one_div]; exact Eq.symm (div_self (ne_of_gt ha))]
      assumption

[Kevin Buzzard]

Just looking at your code makes me wince because you have an exact in the middle of it, which indicates that you are writing tactics where there is more than one goal. You should structure your proofs using \..

[Colin Jones ⚛️]

Haha, sorry! I did it in a rush

[Kevin Buzzard]

This is definitely looking better! I'm sure a limits expert can mangle it down to a few lines, but all those rws at the end can definitely be tidied up (you go a little bit around the houses).

example (ha : 0 < a) : Tendsto (fun (x:ℝ) => (1 - a * x)⁻¹)
    (nhdsWithin (a⁻¹) (Ioo 0 (a⁻¹))) atTop := by
  refine Filter.Tendsto.inv_tendsto_zero ?_
  refine Metric.tendsto_nhdsWithin_nhdsWithin.mpr ?_
  intro e he
  dsimp [Dist.dist]
  norm_num
  use e / a, by positivity -- kill the > 0 goal with the positivity tactic
  intro x _ hx1 hx2
  constructor
  · calc
      a*x < a*a⁻¹ := by gcongr
      _   = 1 := mul_inv_cancel ha.ne' -- ha.ne' is the cheap way to get a != 0 from 0 < a; the power of dot notation
  · rw [abs_sub_comm]
    rw [lt_div_iff ha] at hx2
    nth_rw 2 [← abs_of_pos ha] at hx2
    rwa [← abs_mul, sub_mul, inv_mul_cancel ha.ne', mul_comm] at hx2

You can go straight from a < b / c to a * c < b in one move, you don't have to do what you did.

[Colin Jones ⚛️]

Here's a solution to my original question.

import Mathlib

open BigOperators
open Filter
open Nat
open Set

variable (a b : ℝ)

example (ha : 0 < a) (hb : 0 < b) :
  Tendsto (fun (x:ℝ) => ((1 - a * x) * (1 - a * x + b * x))⁻¹)
         (nhdsWithin (a⁻¹) (Ioo 0 (a⁻¹))) atTop := by
  have one_sub_a : Tendsto (fun x => 1 - a*x) (nhds a⁻¹) (nhds 0) := by
    rw [show (0:ℝ) = 1 - 1 by simp]
    apply Filter.Tendsto.sub
    · exact tendsto_const_nhds
    · rw [show 1 = a*a⁻¹ by rw [← division_def]; exact Eq.symm (div_self (ne_of_gt ha))]
      apply Filter.Tendsto.const_mul
      exact fun ⦃U⦄ a => a
  refine Filter.Tendsto.inv_tendsto_zero ?_
  rw [nhdsWithin]
  apply Filter.Tendsto.inf
  rw [show 0 = 0*(0 + b*a⁻¹) by simp]
  apply Filter.Tendsto.mul
  · exact one_sub_a
  · apply Filter.Tendsto.add
    · exact one_sub_a
    · apply Filter.Tendsto.const_mul
      exact fun ⦃U⦄ a => a
  refine tendsto_principal_principal.mpr ?h₂.a
  intro x hx
  rw [mem_Ioi]
  have ha : a*x < 1 := by
    rw [show 1 = a*a⁻¹ by rw [← one_div]; simp [*]; exact Eq.symm (div_self (ne_of_gt ha))]
    simp_all only [mem_Ioo]
    refine (div_lt_iff' ha).mp ?_
    rw [mul_comm, show x*a/a = x*(a/a) by ring]
    rw [show (a/a) = 1 by apply div_self (ne_of_gt ha)]
    simp
    apply hx.2
  have hb : 0 < b*x := by
    simp_all only [mem_Ioo, gt_iff_lt, mul_pos_iff_of_pos_left]
  have step1 : 0 < 1 - a*x := by
    exact sub_pos.mpr ha
  have step2 : 0 < (1 - a*x + b*x) := by
    exact add_pos step1 hb
  exact Real.mul_pos step1 step2

[Kevin Buzzard]

Well done! Perhaps someone like @Anatole Dedecker will now tell us how this sort of thing is supposed to be done? Or is the answer really just "we need a tactic"?

[Luigi Massacci]

The Isabelle tactic pointed to here should be able to handle that if I read the paper correctly

[Anatole Dedecker]

Here is my solution. There are probably some ways to avoid doing all the side goals by hand but I'm used to it. Of course we would really like a tactic to make such manipulations trivial!

import Mathlib

open BigOperators Filter Nat Set Topology

variable (a b : ℝ)

example (ha : 0 < a) (hb : 0 < b) :
  Tendsto (fun x ↦ ((1 - a * x) * (1 - a * x + b * x))⁻¹)
         (𝓝[Ioo 0 (a⁻¹)] a⁻¹) atTop := by
  simp_rw [mul_inv]
  have fact₁ : Tendsto (fun x ↦ 1 - a * x) (𝓝[Ioo 0 (a⁻¹)] a⁻¹) (𝓝[>] 0) := by
    refine tendsto_nhdsWithin_iff.mpr ⟨tendsto_nhdsWithin_of_tendsto_nhds ?_, ?_⟩
    · rw [show 0 = 1 - a * a⁻¹ by rw [mul_inv_cancel ha.ne.symm, sub_self]]
      exact Continuous.tendsto (by fun_prop) _
    · filter_upwards [eventually_mem_nhdsWithin] with x (hx : 0 < x ∧ x < a⁻¹)
      simpa [mul_inv_cancel ha.ne.symm] using mul_lt_mul' le_rfl hx.2 hx.1.le ha
  have fact₂ : Tendsto (fun x ↦ 1 - a * x + b * x) (𝓝[Ioo 0 (a⁻¹)] a⁻¹) (𝓝 (b * a⁻¹)) := by
    refine tendsto_nhdsWithin_of_tendsto_nhds ?_
    rw [show b * a⁻¹ = 1 - a * a⁻¹ + b * a⁻¹ by rw [mul_inv_cancel ha.ne.symm, sub_self, zero_add]]
    exact Continuous.tendsto (by fun_prop) _
  exact fact₁.inv_tendsto_zero.atTop_mul
    (inv_pos.mpr <| mul_pos hb <| inv_pos.mpr ha)
    (fact₂.inv₀ (mul_pos hb <| inv_pos.mpr ha).ne.symm)

[Anatole Dedecker]

Note that having to talk about 𝓝[Ioo 0 (a⁻¹)] a⁻¹ in the statement is a bit weird, but it's very useful in the proof. It would probably be more idiomatic to do something like

example (ha : 0 < a) (hb : 0 < b) :
  Tendsto (fun x ↦ ((1 - a * x) * (1 - a * x + b * x))⁻¹)
         (𝓝[<] a⁻¹) atTop := by
  simp_rw [mul_inv, ← nhdsWithin_Ioo_eq_nhdsWithin_Iio (inv_pos.mpr ha)]
  -- the rest of the proof is unchanged