Struggling to change an expression in a function definition

Stream: new members

[Colin Jones ⚛️]

I have a problem trying to prove this statement.

import Mathlib

example (a b : ℝ) : Filter.Tendsto (fun x => (1 - a * x + b * x * (a * x) / (a * x))⁻¹ * (1 - a * x)⁻¹)
  (nhdsWithin a⁻¹ (Set.Ioo 0 a⁻¹)) (nhds (b / a)) :=
  by sorry

First I would like to reduce the (ax)/(ax) to 1 but am unsure of how to do that. Can anyone help me out?

Bonus points if someone can prove the actual statement although I do not know if this is true or not as I am updating old proofs from lean 3.

[Calle Sönne]

Colin Jones ⚛️ said:

I have a problem trying to prove this statement.

import Mathlib

example (a b : ℝ) : Filter.Tendsto (fun x => (1 - a * x + b * x * (a * x) / (a * x))⁻¹ * (1 - a * x)⁻¹)
  (nhdsWithin a⁻¹ (Set.Ioo 0 a⁻¹)) (nhds (b / a)) :=
  by sorry

First I would like to reduce the (ax)/(ax) to 1 but am unsure of how to do that. Can anyone help me out?

Bonus points if someone can prove the actual statement although I do not know if this is true or not as I am updating old proofs from lean 3.

For starters, you would need a ≠ 0, as otherwise you might be dividing by zero. Adding that assumption, maybe the lemma docs#mul_div_cancel is what you are looking for?

[Timo Carlin-Burns]

import Mathlib

example (a b : ℝ) : Filter.Tendsto (fun x => (1 - a * x + b * x * (a * x) / (a * x))⁻¹ * (1 - a * x)⁻¹)
    (nhdsWithin a⁻¹ (Set.Ioo 0 a⁻¹)) (nhds (b / a)) := by
  by_cases ha : a = 0
  . simp [ha]
  suffices Filter.Tendsto (fun x => (1 - a * x + b * x)⁻¹ * (1 - a * x)⁻¹)
      (nhdsWithin a⁻¹ (Set.Ioo 0 a⁻¹)) (nhds (b / a)) by
    apply this.congr'
    rw [eventuallyEq_nhdsWithin_iff]
    filter_upwards with x hx
    have hax : a * x ≠ 0 := by aesop
    rw [mul_div_cancel _ hax]
  sorry

[Timo Carlin-Burns]

You also need x ≠ 0, and I learned from this thread that Filter.Tendsto.congr' is one of the main ways of making use of the fact that your function is being applied only within a certain filter.

[Colin Jones ⚛️]

Sorry for not responding to this post in a while. Sorry I forgot to include that a is supposed to be greater than zero and thus not zero and so is b.

[Colin Jones ⚛️]

import Mathlib

open Filter

example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : Filter.Tendsto (fun x => (1 - a * x + b * x * (a * x) / (a * x))⁻¹ * (1 - a * x)⁻¹)
    (nhdsWithin a⁻¹ (Set.Ioo 0 a⁻¹)) (nhds (b / a)) := by
  suffices Filter.Tendsto (fun x => (1 - a * x + b * x)⁻¹ * (1 - a * x)⁻¹)
      (nhdsWithin a⁻¹ (Set.Ioo 0 a⁻¹)) (nhds (b / a)) by
    apply this.congr'
    rw [eventuallyEq_nhdsWithin_iff]
    filter_upwards with x hx
    have hax : a * x ≠ 0 := by aesop
    rw [mul_div_cancel _ hax]
  sorry

I have this so far. How do I replace the goal with the suffices goal?

[Ruben Van de Velde]

What do you mean by "replace the goal"?

[Colin Jones ⚛️]

I don't know how to make the (fun x => (1 - a * x + b * x * (a * x) / (a * x))⁻¹ * (1 - a * x)⁻¹) into (fun x => (1 - a * x + b * x)⁻¹ * (1 - a * x)⁻¹).

[Ruben Van de Velde]

Yes you do, and you have. If you put your cursor before the 's' in 'sorry', you'll see that that's your goal

[Colin Jones ⚛️]

Oh I see my bad! The sorry was screwing me up.

[Colin Jones ⚛️]

I don't think the previous example was possible because (1 - a*x)\- becomes 1/0 but is this goal possible?

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 / (a * x) * (a * x)))⁻¹)
  (nhdsWithin a⁻¹ (Set.Ioo 0 a⁻¹)) atTop := by
  suffices Tendsto (fun x => ((1 - a * x) * (1 - a * x + b * x))⁻¹)
    (nhdsWithin a⁻¹ (Set.Ioo 0 a⁻¹)) atTop by
    apply this.congr'
    rw [eventuallyEq_nhdsWithin_iff]
    filter_upwards with x hx
    have a_x_ne_zero : a*x ≠ 0 := by
      aesop
    have a_x_div : (a*x) / (a*x) = 1 := by
      aesop
    aesop
  sorry

[Colin Jones ⚛️]

I don't know if this goal is possible as I am updating an old proof from lean 3 (not associated with Mathlib). I added the atTop to the goal. Would this make a difference? I am not a mathematician so I don't know the specific details behind these definitions and their ramifications.