-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem thickenedIndicatorAux_tendsto_indicator_closure {δseq : ℕ → ℝ}
    (δseq_lim : Tendsto δseq atTop (𝓝 0)) (E : Set α) :
    Tendsto (fun n => thickenedIndicatorAux (δseq n) E) atTop
      (𝓝 (indicator (closure E) fun _ => (1 : ℝ≥0∞)))

Proof state:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ Tendsto (fun i => 1) atTop (𝓝 1)

Tactic:
exact tendsto_const_nhds

Result:
no goals

Proof state:
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
E : Set α
x : α
x_mem_closure : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Tactic:
specialize δseq_lim ε ε_pos

Result:
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δseq_lim : ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Proof state:
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δseq_lim : ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Tactic:
simp only [dist_zero_right, Real.norm_eq_abs, eventually_atTop] at δseq_lim

Result:
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δseq_lim : ∃ a, ∀ b ≥ a, |δseq b| < ε
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Proof state:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∉ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Tactic:
rcases exists_real_pos_lt_infEdist_of_not_mem_closure x_mem_closure with ⟨ε, ⟨ε_pos, ε_lt⟩⟩

Result:
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Proof state:
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Tactic:
rw [Metric.tendsto_nhds] at δseq_lim

Result:
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
E : Set α
x : α
x_mem_closure : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Proof state:
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ b ≥ N, |δseq b| < ε
⊢ ∀ i ≥ N, thickenedIndicatorAux (δseq i) E x = 0

Tactic:
intro n n_large

Result:
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ b ≥ N, |δseq b| < ε
n : ℕ
n_large : n ≥ N
⊢ thickenedIndicatorAux (δseq n) E x = 0

Proof state:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))

Tactic:
simp_rw [thickenedIndicatorAux_one_of_mem_closure _ E x_mem_closure]

Result:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ Tendsto (fun i => 1) atTop (𝓝 ((closure E).indicator (fun x => 1) x))

Proof state:
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ b ≥ N, |δseq b| < ε
n : ℕ
n_large : n ≥ N
key : x ∉ thickening ε E
⊢ thickenedIndicatorAux ε E x ≤ 0

Tactic:
exact (thickenedIndicatorAux_zero ε_pos E key).le

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ Tendsto (fun n => thickenedIndicatorAux (δseq n) E) atTop (𝓝 ((closure E).indicator fun x => 1))

Tactic:
rw [tendsto_pi_nhds]

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))

Tactic:
intro x

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))

Tactic:
by_cases x_mem_closure : x ∈ closure E

Result:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))

case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∉ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ (closure E).indicator (fun x => 1) x = 1

Tactic:
simp only [x_mem_closure, indicator_of_mem]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∉ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))

Tactic:
rw [show (closure E).indicator (fun _ => (1 : ℝ≥0∞)) x = 0 by
    simp only [x_mem_closure, indicator_of_not_mem, not_false_iff]]

Result:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∉ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)