awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
simp_rw : f x * f' x = 0 x
simp_rw₁ : f x * 0 x = 0 x
simp_rw₂ : f x * 0 = 0
⊢ (f * f') x = 0 x

Tactic:
simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]

Premises used: Pi.mul_apply, Pi.zero_apply, MulZeroClass.mul_zero
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0

Tactic:
exact hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.Algebra.Support
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : AddGroup β
inst_2 : Lattice β
inst_3 : AddLeftMono β
f : α → β
hf : HasCompactSupport f
⊢ HasCompactSupport |f|

Tactic:
hf.comp_left (g := abs) abs_zero

Premises used: abs, abs_zero, HasCompactSupport.comp_left
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
obtain :
  ∀ (n : Set X) (hn : n ∈ 𝓝 x)
    (hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}),
    ∃ (is : Finset ι),
      ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
⊢ ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)

Tactic:
obtain ⟨n, hn, hnf⟩ := hlf x
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
⊢ ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)

Tactic:
⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩

Premises used: Set.iInter, Compl.compl, Filter.inter_mem, Inter.inter, And.intro, Exists.intro, mulTSupport, Set.inter_subset_right
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
refine_1 : ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x
refine_2 : ⋂ i ∈ is, U i ∈ 𝓝 x
refine_3 :
  ∀ (z : X) (hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i),
    (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
⊢ ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)

Tactic:
refine
      ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
⊢ ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x

Tactic:
(biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
        (Set.notMem_subset (hso j) (Finset.mem_filter.mp hj).2)

Premises used: Iff.mpr, isClosed_mulTSupport, IsClosed.compl_mem_nhds, Filter.biInter_finset_mem, And.right, Iff.mp, Finset.mem_filter, Set.notMem_subset
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
⊢ ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x

Tactic:
exact (biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
        (Set.notMem_subset (hso j) (Finset.mem_filter.mp hj).2)

Premises used: Iff.mpr, isClosed_mulTSupport, IsClosed.compl_mem_nhds, Filter.biInter_finset_mem, And.right, Iff.mp, Finset.mem_filter, Set.notMem_subset
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
⊢ ⋂ i ∈ is, U i ∈ 𝓝 x

Tactic:
(biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2

Premises used: Iff.mpr, Filter.biInter_finset_mem, And.right, IsOpen.mem_nhds, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
⊢ ⋂ i ∈ is, U i ∈ 𝓝 x

Tactic:
exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2

Premises used: Iff.mpr, Filter.biInter_finset_mem, And.right, IsOpen.mem_nhds, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ z ∈ n ∩ ((⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i)

Tactic:
rw [inter_assoc] at hz

Premises used: Set.inter_assoc
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hz : z ∈ n ∩ ((⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i)
⊢ z ∈ n

Tactic:
mem_of_mem_inter_left hz

Premises used: Set.mem_of_mem_inter_left
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hz : z ∈ n ∩ ((⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i)
⊢ z ∈ n

Tactic:
exact mem_of_mem_inter_left hz

Premises used: Set.mem_of_mem_inter_left
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ z ∈ n

Tactic:
have hzn : z ∈ n := by
        rw [inter_assoc] at hz
        exact mem_of_mem_inter_left hz
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
hzn : z ∈ n
⊢ Membership.mem (γ := Set X) (⋂ j ∈ js, (mulTSupport (f j))ᶜ) z

Tactic:
replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : Membership.mem (γ := Set X) (⋂ j ∈ js, (mulTSupport (f j))ᶜ) z
⊢ ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ

Tactic:
simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter,
        and_imp] at hz

Premises used: and_imp, Set.Finite.mem_toFinset, Set.mem_setOf_eq, Set.mem_iInter, Finset.mem_filter
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
this :
  (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆
    (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)
⊢ (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)

Tactic:
hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_

Premises used: setOf, Set.Finite.toFinset, Finset.subset_coe_filter_of_subset_forall
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
this :
  (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆
    (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)
refine : ∀ (i : ι) (hi : Membership.mem (γ := Set ι) (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) i), x ∈ U i
⊢ (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)

Tactic:
refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_

Premises used: Set.Finite.toFinset, Finset.subset_coe_filter_of_subset_forall
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
this :
  (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆
    (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) i
⊢ x ∉ U i → z ∈ (mulTSupport (f i))ᶜ

Tactic:
specialize hz i ⟨z, ⟨hi, hzn⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
this :
  (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆
    (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) i
hz : x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
contrapose : ∀ (hz : x ∉ U i), ¬(x ∉ U i → z ∈ (mulTSupport (f i))ᶜ)
⊢ x ∈ U i

Tactic:
contrapose hz
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
this :
  (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆
    (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) i
hz : x ∉ U i
⊢ ¬(x ∉ U i → z ∈ (mulTSupport (f i))ᶜ)

Tactic:
simp [hz, subset_mulTSupport (f i) hi]

Premises used: subset_mulTSupport
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
refine_3 :
  (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆
    (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)
⊢ (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)

Tactic:
suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset by
        refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
        specialize hz i ⟨z, ⟨hi, hzn⟩⟩
        contrapose hz
        simp [hz, subset_mulTSupport (f i) hi]
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) i
refine_3 : (mulSupport (f i) ∩ n).Nonempty
⊢ i ∈ (↑(hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty})) : Set ι)

Tactic:
simp only [Finite.coe_toFinset, mem_setOf_eq]

Premises used: Set.Finite.coe_toFinset, Set.mem_setOf_eq
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) i
⊢ (mulSupport (f i) ∩ n).Nonempty

Tactic:
⟨z, ⟨hi, hzn⟩⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
is : Finset ι := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
i : ι
hi : Membership.mem (γ := Set ι) (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) i
⊢ (mulSupport (f i) ∩ n).Nonempty

Tactic:
exact ⟨z, ⟨hi, hzn⟩⟩
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
M : Type u_7
ι : Type u_9
inst : TopologicalSpace X
inst_1 : One M
f : ι → X → M
⊢ (LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)) ↔
    LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulTSupport (f i)

Tactic:
⟨LocallyFinite.closure, fun H ↦ H.subset fun _ ↦ subset_closure⟩

Premises used: subset_closure, LocallyFinite.subset, LocallyFinite.closure, Iff.intro
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
inst_1 : Zero R
inst_2 : Zero M
inst_3 : SMulWithZero R M
s : ι → X → R
h_1 : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ support (s i)
f : ι → X → M
i : ι
x : X
h : s i x = 0
rw : s i x • f i x = 0
rw₁ : HSMul.hSMul.{u_8, u_7, u_7} (α := R) 0 (f i x) = 0
rw₂ rw₃ : Eq.{u_7 + 1} (α := M) 0 0
⊢ (s i • f i) x = 0

Tactic:
rw [Pi.smul_apply', h, zero_smul]

Premises used: Pi.smul_apply', zero_smul
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
inst_1 : Zero M
inst_2 : SMulZeroClass R M
f : ι → X → M
h_1 : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ support (f i)
s : ι → X → R
i : ι
x : X
h : f i x = 0
rw : s i x • f i x = 0
rw₁ : HSMul.hSMul (β := M) (s i x) 0 = 0
rw₂ rw₃ : Eq.{u_7 + 1} (α := M) 0 0
⊢ (s i • f i) x = 0

Tactic:
rw [Pi.smul_apply', h, smul_zero]

Premises used: Pi.smul_apply', smul_zero