-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
/-- Pointwise, the multiplicative indicators of δ-thickenings of a set eventually coincide
with the multiplicative indicator of the set as δ>0 tends to zero. -/
@[to_additive "Pointwise, the indicators of δ-thickenings of a set eventually coincide
with the indicator of the set as δ>0 tends to zero."]
lemma mulIndicator_thickening_eventually_eq_mulIndicator_closure (f : α → β) (E : Set α) (x : α) :
    ∀ᶠ δ in 𝓝[>] (0 : ℝ),
      (Metric.thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Proof state:
case neg
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Tactic:
have obs := eventually_not_mem_thickening_of_infEdist_pos x_mem_closure

Result:
case neg
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure E
obs : ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Proof state:
case pos
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Tactic:
filter_upwards [self_mem_nhdsWithin] with δ δ_pos

Result:
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
δ : ℝ
δ_pos : δ ∈ Ioi 0
⊢ (thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Proof state:
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Tactic:
by_cases x_mem_closure : x ∈ closure E

Result:
case pos
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

case neg
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Proof state:
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
δ : ℝ
δ_pos : δ ∈ Ioi 0
⊢ (thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Tactic:
simp only [closure_subset_thickening δ_pos E x_mem_closure, mulIndicator_of_mem, x_mem_closure]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure E
obs : ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Tactic:
filter_upwards [mem_nhdsWithin_of_mem_nhds obs, self_mem_nhdsWithin]
  with δ x_notin_thE _

Result:
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure E
obs : ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
δ : ℝ
x_notin_thE : x ∉ thickening δ E
a✝ : δ ∈ Ioi 0
⊢ (thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Proof state:
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure E
obs : ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
δ : ℝ
x_notin_thE : x ∉ thickening δ E
a✝ : δ ∈ Ioi 0
⊢ (thickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Tactic:
simp only [x_notin_thE, not_false_eq_true, mulIndicator_of_not_mem, x_mem_closure]

Result:
no goals