How to prove this limit?

Stream: new members

[Junqi Liu]

import Mathlib

example (f : ℝ × ℝ → ℝ) : Filter.Tendsto (fun (n : ℕ) ↦
    (Set.Ioo (1 / ((n : ℝ) + 1)) (1 - 1 / (↑n + 1)) ×ˢ Set.Ioo (1 / ((n : ℝ) + 1)) (1 - 1 / (↑n + 1))).indicator f x)
    Filter.atTop (nhds ((Set.Ioo 0 1 ×ˢ Set.Ioo 0 1).indicator f x)) := by
  sorry

[Bjørn Kjos-Hanssen]

Prove that s.indicator f x is just (f x) * s.indicator 1 x so it suffices to prove the statement for 1; then you can write simp to get an easier goal.

[Junqi Liu]

emmmmmm. By following your suggestion I get a new goal:

import Mathlib

example : Filter.Tendsto (fun (n : ℕ) ↦
    (Set.Ioo (1 / ((n : ℝ) + 1)) (1 - 1 / (↑n + 1)) ×ˢ Set.Ioo (1 / ((n : ℝ) + 1)) (1 - 1 / (↑n + 1))).indicator 1 x)
    Filter.atTop (nhds ((Set.Ioo 0 1 ×ˢ Set.Ioo 0 1).indicator 1 x)) := by
  sorry

But I still don't know how to due with it. wuwuwu:sob:

[Bjørn Kjos-Hanssen]

Ah sorry, I guess the constant function 1 has to be spelled out more: (fun _ => 1). Then try simp.

[Junqi Liu]

I have tried simp, but it seems like I get a goal which is wrong. I don't know why.