-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
/-- Pointwise, the multiplicative indicators of closed δ-thickenings of a set eventually coincide
with the multiplicative indicator of the set as δ tends to zero. -/
@[to_additive "Pointwise, the indicators of closed δ-thickenings of a set eventually coincide
with the indicator of the set as δ tends to zero."]
lemma mulIndicator_cthickening_eventually_eq_mulIndicator_closure (f : α → β) (E : Set α) (x : α) :
    ∀ᶠ δ in 𝓝 (0 : ℝ),
      (Metric.cthickening δ 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
δ : ℝ
a✝ : δ ∈ univ
obs : x ∈ cthickening δ E
⊢ (cthickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Tactic:
rw [mulIndicator_of_mem obs f, mulIndicator_of_mem x_mem_closure f]

Result:
no goals

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

Tactic:
have obs : x ∈ cthickening δ E := closure_subset_cthickening δ E x_mem_closure

Result:
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
δ : ℝ
a✝ : δ ∈ univ
obs : x ∈ cthickening δ E
⊢ (cthickening δ 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, (cthickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Tactic:
filter_upwards [eventually_not_mem_cthickening_of_infEdist_pos x_mem_closure] with δ hδ

Result:
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure E
δ : ℝ
hδ : x ∉ cthickening δ E
⊢ (cthickening δ 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
δ : ℝ
hδ : x ∉ cthickening δ E
⊢ (cthickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Tactic:
simp only [hδ, not_false_eq_true, mulIndicator_of_not_mem, x_mem_closure]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, (cthickening δ 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, (cthickening δ 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, (cthickening δ 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, (cthickening δ E).mulIndicator f x = (closure E).mulIndicator f x

Tactic:
filter_upwards [univ_mem] with δ _

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