awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
⊢ EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b

Tactic:
have obs : (fun _ ↦ if q then a else b) =ᶠ[L] (fun i ↦ if p i then a else b) := by
      filter_upwards [h] with i hi
      simp only [hi]
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
mpr : Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)
⊢ Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)

Tactic:
apply Tendsto.congr' obs

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
pos : ∀ (hq : q), Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)
neg : ∀ (hq : ¬q), Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)
⊢ Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)

Tactic:
by_cases hq : q
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
hq : q
pos : Tendsto (fun (x : ι) ↦ a) L F
⊢ Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)

Tactic:
simp only [hq, ite_true]

Premises used: ite_true
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
hq : q
apply : LE.le (α := Filter β) (map (fun (x : ι) ↦ a) L) (𝓟 {a})
⊢ Tendsto (fun (x : ι) ↦ a) L F

Tactic:
apply le_trans _ haF

Premises used: le_trans
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
hq : q
⊢ LE.le (α := Filter β) (map (fun (x : ι) ↦ a) L) (𝓟 {a})

Tactic:
simp
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
hq : ¬q
neg : Tendsto (fun (x : ι) ↦ b) L G
⊢ Tendsto (fun (x : ι) ↦ if q then a else b) L (if q then F else G)

Tactic:
simp only [hq, ite_false]

Premises used: ite_false
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
hq : ¬q
apply : LE.le (α := Filter β) (map (fun (x : ι) ↦ b) L) (𝓟 {b})
⊢ Tendsto (fun (x : ι) ↦ b) L G

Tactic:
apply le_trans _ hbG

Premises used: le_trans
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b
hq : ¬q
⊢ LE.le (α := Filter β) (map (fun (x : ι) ↦ b) L) (𝓟 {b})

Tactic:
simp only [principal_singleton, le_pure_iff, mem_map, Set.mem_singleton_iff,
        Set.preimage_const_of_mem, univ_mem]

Premises used: Filter.le_pure_iff, Set.mem_singleton_iff, Filter.principal_singleton, Filter.univ_mem, Filter.mem_map, Set.preimage_const_of_mem
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
refine_3 :
  ∀
    (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.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
        (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
      ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
refine_1 : 𝓟 {b} ≤ 𝓝 b
refine_2 : LE.le (α := Filter β) (𝓟 {0}) (𝓝 0)
⊢ Tendsto.{u_3, u_2} (β := β) (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 : β))
                nhds_o nhds_b ?_ ?_
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
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 : ι) ↦ 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

Tactic:
heart
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
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
h : 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0
⊢ Tendsto.{u_3, u_2} (β := β) (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
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
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
pos : ∀ (hxA : x ∈ A), 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0
neg : ∀ (hxA : x ∉ A), 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0
⊢ 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0

Tactic:
by_cases hxA : x ∈ A
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
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
hxA : x ∈ A
⊢ 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0

Tactic:
simp [hxA]
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
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
hxA : x ∉ A
⊢ 𝓝 (A.indicator (fun (x : α) ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0

Tactic:
simp [hxA]
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
refine_1 : ∀ x ∈ 𝓝 b, b ∈ x
⊢ 𝓟 {b} ≤ 𝓝 b

Tactic:
simp only [principal_singleton, le_def, mem_pure]

Premises used: Filter.principal_singleton, Filter.le_def, Filter.mem_pure
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
⊢ ∀ x ∈ 𝓝 b, b ∈ x

Tactic:
fun s s_nhds ↦ mem_of_mem_nhds s_nhds

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
⊢ ∀ x ∈ 𝓝 b, b ∈ x

Tactic:
exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
refine_2 : ∀ (x : Set β), Membership.mem (γ := Filter β) (𝓝 0) x → 0 ∈ x
⊢ LE.le (α := Filter β) (𝓟 {0}) (𝓝 0)

Tactic:
simp only [principal_singleton, le_def, mem_pure]

Premises used: Filter.principal_singleton, Filter.le_def, Filter.mem_pure
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
⊢ ∀ (x : Set β), Membership.mem (γ := Filter β) (𝓝 0) x → 0 ∈ x

Tactic:
fun s s_nhds ↦ mem_of_mem_nhds s_nhds

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
⊢ ∀ (x : Set β), Membership.mem (γ := Filter β) (𝓝 0) x → 0 ∈ x

Tactic:
exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
x : α
refine_1 : 𝓟 {b} ≤ 𝓝 b
refine_2 : LE.le (α := Filter β) (𝓟 {0}) (𝓝 0)
refine_3 :
  ∀
    (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.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
        (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
      ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
refine_1₁ : 𝓟 {b} ≤ 𝓝 b
refine_2₁ : LE.le (α := Filter β) (𝓟 {0}) (𝓝 0)
refine_3₁ refine_3₂ :
  ∀
    (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.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
        (𝓝 (A.indicator (fun (x : α) ↦ b) x)) ↔
      ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
refine_1₂ : 𝓟 {b} ≤ 𝓝 b
refine_2₂ : LE.le (α := Filter β) (𝓟 {0}) (𝓝 0)
refine_1₃ : 𝓟 {b} ≤ 𝓝 b
refine_2₃ refine_2₄ : LE.le (α := Filter β) (𝓟 {0}) (𝓝 0)
⊢ Tendsto.{u_3, u_2} (β := β) (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:
classical
  have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β))
                nhds_o nhds_b ?_ ?_
  · convert! heart
    by_cases hxA : x ∈ A <;> simp [hxA]
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds

Premises used: mem_of_mem_nhds, Filter.principal_singleton, Filter.le_def, Filter.mem_pure
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
simp_rw :
  (∀ (x : α),
      Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
        (𝓝 (A.indicator (fun (x : α) ↦ b) x))) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Tendsto (β := (x : α) → β) (fun (i : ι) ↦ (As i).indicator fun (x : α) ↦ b) L (𝓝 (A.indicator fun (x : α) ↦ b)) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
simp_rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
h :
  ∀ (a : α),
    Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) a) L
        (𝓝 (A.indicator (fun (x : α) ↦ b) a)) ↔
      ∀ᶠ (i : ι) in L, a ∈ As i ↔ a ∈ A
⊢ (∀ (x : α),
      Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) x) L
        (𝓝 (A.indicator (fun (x : α) ↦ b) x))) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
⊢ ∀ (a : α),
    Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) a) L
        (𝓝 (A.indicator (fun (x : α) ↦ b) a)) ↔
      ∀ᶠ (i : ι) in L, a ∈ As i ↔ a ∈ A

Tactic:
tendsto_indicator_const_apply_iff_eventually' L b nhds_b nhds_o

Premises used: tendsto_indicator_const_apply_iff_eventually'
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
⊢ ∀ (a : α),
    Tendsto.{u_3, u_2} (β := β) (fun (i : ι) ↦ (As i).indicator (fun (x : α) ↦ b) a) L
        (𝓝 (A.indicator (fun (x : α) ↦ b) a)) ↔
      ∀ᶠ (i : ι) in L, a ∈ As i ↔ a ∈ A

Tactic:
exact tendsto_indicator_const_apply_iff_eventually' L b nhds_b nhds_o

Premises used: tendsto_indicator_const_apply_iff_eventually'
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
x : α
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
⊢ Tendsto.{u_3, u_2} (β := β) (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:
apply tendsto_indicator_const_apply_iff_eventually' _ b

Premises used: tendsto_indicator_const_apply_iff_eventually'
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
x : α
⊢ {0}ᶜ ∈ 𝓝 b

Tactic:
simp only [compl_singleton_mem_nhds_iff, ne_eq, NeZero.ne, not_false_eq_true]

Premises used: compl_singleton_mem_nhds_iff, ne_eq, not_false_eq_true, NeZero.ne
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
x : α
⊢ Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ

Tactic:
simp only [compl_singleton_mem_nhds_iff, ne_eq, (NeZero.ne b).symm, not_false_eq_true]

Premises used: compl_singleton_mem_nhds_iff, Ne.symm, ne_eq, not_false_eq_true, NeZero.ne
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
⊢ Tendsto (β := (x : α) → β) (fun (i : ι) ↦ (As i).indicator fun (x : α) ↦ b) L (𝓝 (A.indicator fun (x : α) ↦ b)) ↔
    ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
apply tendsto_indicator_const_iff_forall_eventually' _ b

Premises used: tendsto_indicator_const_iff_forall_eventually'
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
⊢ {0}ᶜ ∈ 𝓝 b

Tactic:
simp only [compl_singleton_mem_nhds_iff, ne_eq, NeZero.ne, not_false_eq_true]

Premises used: compl_singleton_mem_nhds_iff, ne_eq, not_false_eq_true, NeZero.ne
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
⊢ Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ

Tactic:
simp only [compl_singleton_mem_nhds_iff, ne_eq, (NeZero.ne b).symm, not_false_eq_true]

Premises used: compl_singleton_mem_nhds_iff, Ne.symm, ne_eq, not_false_eq_true, NeZero.ne
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
rw : (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun (x : ι) ↦ i ∈ As x) L (pure (i ∈ A))
⊢ Tendsto (β := (x : α) → β) (fun (i : ι) ↦ (As i).indicator fun (x : α) ↦ b) L (𝓝 (A.indicator fun (x : α) ↦ b)) ↔
    Tendsto.{u_3, u_1} (β := (x : α) → Prop) (fun (i : ι) (x : α) ↦ x ∈ As i) L
      (pi (α := fun (x : α) ↦ Prop) fun (x : α) ↦ pure (x ∈ A))

Tactic:
rw [tendsto_indicator_const_iff_forall_eventually' _ b nhds_b nhds_o, tendsto_pi]

Premises used: tendsto_indicator_const_iff_forall_eventually', Filter.tendsto_pi
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
simp_rw : (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, (i ∈ As x) = (i ∈ A)
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun (x : ι) ↦ i ∈ As x) L (pure (i ∈ A))

Tactic:
simp_rw [tendsto_pure]

Premises used: Filter.tendsto_pure
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : Membership.mem (γ := Filter β) (𝓝 0) {b}ᶜ
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, (i ∈ As x) = (i ∈ A)

Tactic:
aesop
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
rw : (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun (x : ι) ↦ i ∈ As x) L (pure (i ∈ A))
⊢ Tendsto (β := (x : α) → β) (fun (i : ι) ↦ (As i).indicator fun (x : α) ↦ b) L (𝓝 (A.indicator fun (x : α) ↦ b)) ↔
    Tendsto.{u_3, u_1} (β := (x : α) → Prop) (fun (i : ι) (x : α) ↦ x ∈ As i) L
      (pi (α := fun (x : α) ↦ Prop) fun (x : α) ↦ pure (x ∈ A))

Tactic:
rw [tendsto_indicator_const_iff_forall_eventually _ b, tendsto_pi]

Premises used: tendsto_indicator_const_iff_forall_eventually, Filter.tendsto_pi
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
simp_rw : (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, (i ∈ As x) = (i ∈ A)
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun (x : ι) ↦ i ∈ As x) L (pure (i ∈ A))

Tactic:
simp_rw [tendsto_pure]

Premises used: Filter.tendsto_pure
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
α : Type u_1
A : Set α
β : Type u_2
inst : Zero β
inst_1 : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst_2 : T1Space β
b : β
inst_3 : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, (i ∈ As x) = (i ∈ A)

Tactic:
aesop
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ x ⤳ y

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ pure x ≤ 𝓝 y

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ ∀ (a : x ⤳ y), pure x ≤ 𝓝 y

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ ∀ (a : x ⤳ y), pure x ≤ 𝓝 y

Tactic:
tfae_have 1 → 2 := (pure_le_nhds _).trans

Premises used: pure_le_nhds, LE.le.trans
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
⊢ pure x ≤ 𝓝 y

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
⊢ ∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
tfae_1_to_2 : ∀ (a : x ⤳ y), pure x ≤ 𝓝 y
⊢ ∀ (a : pure x ≤ 𝓝 y) (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false