-- Mathlib/Topology/IndicatorConstPointwise.lean
lemma tendsto_indicator_const_apply_iff_eventually' (b : β)
    (nhd_b : {0}ᶜ ∈ 𝓝 b) (nhd_o : {b}ᶜ ∈ 𝓝 0) (x : α) :
    Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b) x) L (𝓝 (A.indicator (fun (_ : α) ↦ b) x))
      ↔ ∀ᶠ i in L, (x ∈ As i ↔ x ∈ A)

Proof state:
case h.e'_1.h.e'_5
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
heart :
  Tendsto (fun i => if (fun i => x ∈ As i) i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔
    ∀ᶠ (i : ι) in L, (fun i => x ∈ As i) i ↔ x ∈ A
⊢ 𝓝 (A.indicator (fun x => b) x) = if x ∈ A then 𝓝 b else 𝓝 0

Tactic:
by_cases hxA : x ∈ A <;> simp [hxA]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ ∀ x ∈ 𝓝 0, 0 ∈ x

Tactic:
exact fun s s_nhd ↦ mem_of_mem_nhds s_nhd

Result:
no goals

Proof state:
case refine_1
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ ∀ x ∈ 𝓝 b, b ∈ x

Tactic:
exact fun s s_nhd ↦ mem_of_mem_nhds s_nhd

Result:
no goals

Proof state:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ Tendsto (fun i => (As i).indicator (fun x => b) x) L (𝓝 (A.indicator (fun x => b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β))
              nhd_o nhd_b ?_ ?_

Result:
case refine_3
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
heart :
  Tendsto (fun i => if (fun i => x ∈ As i) i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔
    ∀ᶠ (i : ι) in L, (fun i => x ∈ As i) i ↔ x ∈ A
⊢ Tendsto (fun i => (As i).indicator (fun x => b) x) L (𝓝 (A.indicator (fun x => b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

case refine_1
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ 𝓟 {b} ≤ 𝓝 b

case refine_2
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ 𝓟 {0} ≤ 𝓝 0

Proof state:
case refine_1
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ 𝓟 {b} ≤ 𝓝 b

Tactic:
simp only [principal_singleton, le_def, mem_pure]

Result:
case refine_1
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ ∀ x ∈ 𝓝 b, b ∈ x

Proof state:
case refine_2
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ 𝓟 {0} ≤ 𝓝 0

Tactic:
simp only [principal_singleton, le_def, mem_pure]

Result:
case refine_2
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
⊢ ∀ x ∈ 𝓝 0, 0 ∈ x

Proof state:
case refine_3
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
heart :
  Tendsto (fun i => if (fun i => x ∈ As i) i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔
    ∀ᶠ (i : ι) in L, (fun i => x ∈ As i) i ↔ x ∈ A
⊢ Tendsto (fun i => (As i).indicator (fun x => b) x) L (𝓝 (A.indicator (fun x => b) x)) ↔
    ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
convert heart

Result:
case h.e'_1.h.e'_5
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhd_b : {0}ᶜ ∈ 𝓝 b
nhd_o : {b}ᶜ ∈ 𝓝 0
x : α
heart :
  Tendsto (fun i => if (fun i => x ∈ As i) i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔
    ∀ᶠ (i : ι) in L, (fun i => x ∈ As i) i ↔ x ∈ A
⊢ 𝓝 (A.indicator (fun x => b) x) = if x ∈ A then 𝓝 b else 𝓝 0