Theorem: exercise6_2 (LeanCourse/Assignments/Assignment6.lean)

State before:
ι : Type u_1
L : Filter ι
s : ι → Set ℝ
t : Set ℝ
f : ℝ → ℝ
ha : ∀ (x : ℝ), f x ≠ 0
⊢ (∀ (x : ℝ), ∀ᶠ (i : ι) in L, x ∈ s i ↔ x ∈ t) ↔ Tendsto (fun i => indicator (s i) f) L (𝓝 (indicator t f))
Tactic:
rw [tendsto_pi_nhds]
State after:
ι : Type u_1
L : Filter ι
s : ι → Set ℝ
t : Set ℝ
f : ℝ → ℝ
ha : ∀ (x : ℝ), f x ≠ 0
⊢ (∀ (x : ℝ), ∀ᶠ (i : ι) in L, x ∈ s i ↔ x ∈ t) ↔
    ∀ (x : ℝ), Tendsto (fun i => indicator (s i) f x) L (𝓝 (indicator t f x))

State before:
ι : Type u_1
L : Filter ι
s : ι → Set ℝ
t : Set ℝ
f : ℝ → ℝ
ha : ∀ (x : ℝ), f x ≠ 0
⊢ (∀ (x : ℝ), ∀ᶠ (i : ι) in L, x ∈ s i ↔ x ∈ t) ↔
    ∀ (x : ℝ), Tendsto (fun i => indicator (s i) f x) L (𝓝 (indicator t f x))
Tactic:
sorry
State after:
no goals