-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem thickenedIndicator_tendsto_indicator_closure {δseq : ℕ → ℝ} (δseq_pos : ∀ n, 0 < δseq n)
    (δseq_lim : Tendsto δseq atTop (𝓝 0)) (E : Set α) :
    Tendsto (fun n : ℕ => ((↑) : (α →ᵇ ℝ≥0) → α → ℝ≥0) (thickenedIndicator (δseq_pos n) E)) atTop
      (𝓝 (indicator (closure E) fun _ => (1 : ℝ≥0)))

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

Tactic:
refine (congr_fun (comp_indicator_const 1 ENNReal.toNNReal zero_toNNReal) x).symm

Result:
no goals

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

Tactic:
intro x

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

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

Tactic:
rw [tendsto_pi_nhds] at *

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

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

Tactic:
by_cases x_mem : x ∈ closure E <;> simp [x_mem]

Result:
no goals

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

Tactic:
have key := thickenedIndicatorAux_tendsto_indicator_closure δseq_lim E

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

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

Tactic:
rw [show indicator (closure E) (fun _ => (1 : ℝ≥0)) x =
      (indicator (closure E) (fun _ => (1 : ℝ≥0∞)) x).toNNReal
    by refine (congr_fun (comp_indicator_const 1 ENNReal.toNNReal zero_toNNReal) x).symm]

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

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

Tactic:
refine Tendsto.comp (tendsto_toNNReal ?_) (key x)

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