awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
this : D.support (U := U) = {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
rw : IsDiscrete ({x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U)
⊢ IsDiscrete (D.support (U := U))

Tactic:
rw [this]
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
this : D.support (U := U) = {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
h : {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜᶜ ∈ codiscreteWithin U
⊢ IsDiscrete ({x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U)

Tactic:
apply isDiscrete_of_codiscreteWithin

Premises used: isDiscrete_of_codiscreteWithin
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
this : D.support (U := U) = {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
h : {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)} ∈ codiscreteWithin U
⊢ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜᶜ ∈ codiscreteWithin U

Tactic:
rw [compl_compl]

Premises used: compl_compl
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
this : D.support (U := U) = {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) (⇑D : (a : X) → Y)).Finite
⊢ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)} ∈ codiscreteWithin U

Tactic:
apply (supportDiscreteWithin_iff_locallyFiniteWithin D.supportWithinDomain).2

Premises used: Iff.mpr, supportDiscreteWithin_iff_locallyFiniteWithin, Function.locallyFinsuppWithin.supportWithinDomain
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
this : D.support (U := U) = {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) (⇑D : (a : X) → Y)).Finite

Tactic:
D.supportLocallyFiniteWithinDomain

Premises used: Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
this : D.support (U := U) = {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) (⇑D : (a : X) → Y)).Finite

Tactic:
exact D.supportLocallyFiniteWithinDomain

Premises used: Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst] U
⊢ IsClosed[inst] (U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x})

Tactic:
isClosed_sdiff_of_codiscreteWithin
      ((supportDiscreteWithin_iff_locallyFiniteWithin D.supportWithinDomain).2
        D.supportLocallyFiniteWithinDomain)
      hU

Premises used: Iff.mpr, Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain, isClosed_sdiff_of_codiscreteWithin, supportDiscreteWithin_iff_locallyFiniteWithin, Function.locallyFinsuppWithin.supportWithinDomain
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst] U
h : D.support (U := U) = U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x}
⊢ IsClosed[inst] (D.support (U := U))

Tactic:
convert!
    isClosed_sdiff_of_codiscreteWithin
      ((supportDiscreteWithin_iff_locallyFiniteWithin D.supportWithinDomain).2
        D.supportLocallyFiniteWithinDomain)
      hU

Premises used: Iff.mpr, Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain, isClosed_sdiff_of_codiscreteWithin, supportDiscreteWithin_iff_locallyFiniteWithin, Function.locallyFinsuppWithin.supportWithinDomain
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst] U
h :
  ∀ (x : X),
    x ∈ D.support (U := U) ↔
      x ∈ U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x}
⊢ D.support (U := U) = U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x}

Tactic:
ext x
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst] U
x : X
h :
  x ∈ D.support (U := U) → x ∈ U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x}
h₁ :
  x ∈ U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x} → x ∈ D.support (U := U)
⊢ x ∈ D.support (U := U) ↔ x ∈ U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x}

Tactic:
constructor
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst] U
x : X
hx : x ∈ D.support (U := U)
⊢ x ∈ U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x}

Tactic:
simp_all [D.supportWithinDomain hx]

Premises used: Function.locallyFinsuppWithin.supportWithinDomain
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T1Space X
inst_2 : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst] U
x : X
hx : x ∈ U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x}
⊢ x ∈ D.support (U := U)

Tactic:
simp_all
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : T2Space X
inst_2 : Zero Y
D : locallyFinsuppWithin U Y
hU : IsCompact U
⊢ D.support (U := U).Finite

Tactic:
(hU.of_isClosed_subset (D.closedSupport hU.isClosed)
    D.supportWithinDomain).finite D.discreteSupport

Premises used: Function.locallyFinsuppWithin.discreteSupport, IsCompact.of_isClosed_subset, Function.locallyFinsuppWithin.supportWithinDomain, Function.locallyFinsuppWithin.closedSupport, IsCompact.finite, IsCompact.isClosed
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
f g : X → Y
hf :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} f
hg :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} g
left : Function.support (f + g) ⊆ U
right : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
⊢ Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} (f + g)

Tactic:
constructor
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
f g : X → Y
hf :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} f
hg :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} g
x : X
hx : x ∈ Function.support (f + g)
left : ∀ (hx : x ∉ U), x ∉ Function.support (f + g)
⊢ x ∈ U

Tactic:
contrapose hx
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
f g : X → Y
hf :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} f
hg :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} g
x : X
hx : x ∉ U
⊢ x ∉ Function.support (f + g)

Tactic:
simp [notMem_support.1 fun a ↦ hx (hf.1 a), notMem_support.1 fun a ↦ hx (hg.1 a)]

Premises used: Function.notMem_support, And.left, Iff.mp
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
f g : X → Y
hf :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} f
hg :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} g
z : X
hz : z ∈ U
right :
  ∀ (t₁ : Set X) (ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite), ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite

Tactic:
obtain ⟨t₁, ht₁⟩ := hf.2 z hz

Premises used: And.right
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
f g : X → Y
hf :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} f
hg :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} g
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
right :
  ∀ (t₂ : Set X) (ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite), ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite

Tactic:
obtain ⟨t₂, ht₂⟩ := hg.2 z hz

Premises used: And.right
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
f g : X → Y
hf :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} f
hg :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} g
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
right : (t₁ ∩ t₂ ∩ Function.support (f + g)).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite

Tactic:
use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1

Premises used: Filter.inter_mem, And.left
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
f g : X → Y
hf :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} f
hg :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} g
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
right : t₁ ∩ t₂ ∩ Function.support (f + g) ⊆ t₁ ∩ Function.support f ∪ t₂ ∩ Function.support g
⊢ (t₁ ∩ t₂ ∩ Function.support (f + g)).Finite

Tactic:
apply Set.Finite.subset (s := (t₁ ∩ f.support) ∪ (t₂ ∩ g.support)) (ht₁.2.union ht₂.2)

Premises used: Set.Finite.union, Set.Finite.subset, And.right
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
f g : X → Y
hf :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} f
hg :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} g
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
a : X
ha : a ∈ t₁ ∩ t₂ ∩ Function.support (f + g)
right :
  ∀ (hf : (∀ (x : X), ¬f x = 0 → x ∈ U) ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite)
    (hg : (∀ (x : X), ¬g x = 0 → x ∈ U) ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support g).Finite) (hz : z ∈ U)
    (ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite) (ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite)
    (ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬f a + g a = 0), ¬f a = 0 ∨ ¬g a = 0
⊢ a ∈ t₁ ∩ Function.support f ∪ t₂ ∩ Function.support g

Tactic:
simp_all only [support_subset_iff, ne_eq, mem_setOf_eq,
        mem_inter_iff, mem_support, Pi.add_apply, mem_union, true_and]

Premises used: Set.mem_union, Set.mem_inter_iff, Set.mem_setOf_eq, ne_eq, Pi.add_apply, Function.support_subset_iff, Function.mem_support, true_and
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
f g : X → Y
z : X
t₁ t₂ : Set X
a : X
hf : (∀ (x : X), ¬f x = 0 → x ∈ U) ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite
hg : (∀ (x : X), ¬g x = 0 → x ∈ U) ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support g).Finite
hz : z ∈ U
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬f a + g a = 0
right : ∀ (hCon : f a = 0 ∧ g a = 0), False
⊢ ¬f a = 0 ∨ ¬g a = 0

Tactic:
by_contra! hCon
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
f g : X → Y
z : X
t₁ t₂ : Set X
a : X
hf : (∀ (x : X), ¬f x = 0 → x ∈ U) ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite
hg : (∀ (x : X), ¬g x = 0 → x ∈ U) ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support g).Finite
hz : z ∈ U
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬f a + g a = 0
hCon : f a = 0 ∧ g a = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
simp : ∀ z ∈ U, ∃ (t : Set X), t ∈ 𝓝 z
⊢ Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} 0

Tactic:
simp only [support_subset_iff, ne_eq, mem_setOf_eq, Pi.zero_apply, not_true_eq_false,
      IsEmpty.forall_iff, implies_true, support_zero, inter_empty, finite_empty, and_true,
      true_and]

Premises used: Set.finite_empty, and_true, Pi.zero_apply, not_true_eq_false, Set.mem_setOf_eq, ne_eq, Function.support_subset_iff, Function.support_zero, implies_true, Set.inter_empty, true_and, IsEmpty.forall_iff
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
⊢ ∀ z ∈ U, ∃ (t : Set X), t ∈ 𝓝 z

Tactic:
fun _ _ ↦ ⟨⊤, univ_mem⟩

Premises used: Exists.intro, Top.top, Filter.univ_mem
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
⊢ ∀ z ∈ U, ∃ (t : Set X), t ∈ 𝓝 z

Tactic:
exact fun _ _ ↦ ⟨⊤, univ_mem⟩
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
D : locallyFinsuppWithin U Y
⊢ Membership.mem (γ := AddSubmonoid (X → Y)) (locallyFinsuppWithin.addSubmonoid U) (⇑D : (a : X) → Y)

Tactic:
⟨D.supportWithinDomain, D.supportLocallyFiniteWithinDomain⟩

Premises used: Set.Mem, Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain, setOf, And.intro, Function.locallyFinsuppWithin.supportWithinDomain
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddGroup Y
f : X → Y
hf :
  Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} f
⊢ Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} (-f)

Tactic:
simp_all
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddGroup Y
D : locallyFinsuppWithin U Y
⊢ Membership.mem (γ := AddSubgroup (X → Y)) (locallyFinsuppWithin.addSubgroup U) (⇑D : (a : X) → Y)

Tactic:
⟨D.supportWithinDomain, D.supportLocallyFiniteWithinDomain⟩

Premises used: Set.Mem, Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain, setOf, And.intro, Function.locallyFinsuppWithin.supportWithinDomain
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
⊢ Eq (α := (a : X) → Y) (⇑0 : (a : X) → Y) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (⇑(D₁ + D₂) : (a : X) → Y) = HAdd.hAdd (α := (a : X) → Y) (⇑D₁ : (a : X) → Y) (⇑D₂ : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddGroup Y
D : locallyFinsuppWithin U Y
⊢ Eq (α := (a : X) → Y) (⇑(-D) : (a : X) → Y) (-(⇑D : (a : X) → Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddGroup Y
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (⇑(D₁ - D₂) : (a : X) → Y) = HSub.hSub (α := (a : X) → Y) (⇑D₁ : (a : X) → Y) (⇑D₂ : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
D : locallyFinsuppWithin U Y
n : ℕ
⊢ (⇑(n • D) : (a : X) → Y) = HSMul.hSMul (β := (a : X) → Y) n (⇑D : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddGroup Y
D : locallyFinsuppWithin U Y
n : ℤ
⊢ (⇑(n • D) : (a : X) → Y) = HSMul.hSMul (β := (a : X) → Y) n (⇑D : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommMonoid Y
ι : Type u_3
F : ι → locallyFinsuppWithin U Y
⊢ Eq (α := (a : X) → Y) (⇑(∑ n ∈ ∅, F n) : (a : X) → Y) (∑ n ∈ ∅, (⇑(F n) : (a : X) → Y))

Tactic:
simp_all
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommMonoid Y
ι : Type u_3
F : ι → locallyFinsuppWithin U Y
a : ι
s : Finset ι
h : a ∉ s
h_1 : Eq (α := (a : X) → Y) (⇑(∑ n ∈ s, F n) : (a : X) → Y) (∑ n ∈ s, (⇑(F n) : (a : X) → Y))
⊢ Eq (α := (a : X) → Y) (⇑(∑ n ∈ insert a s, F n) : (a : X) → Y) (∑ n ∈ insert a s, (⇑(F n) : (a : X) → Y))

Tactic:
simp_all
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommMonoid Y
ι : Type u_3
s : Finset ι
F : ι → locallyFinsuppWithin U Y
empty : Eq (α := (a : X) → Y) (⇑(∑ n ∈ ∅, F n) : (a : X) → Y) (∑ n ∈ ∅, (⇑(F n) : (a : X) → Y))
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      Eq (α := (a : X) → Y) (⇑(∑ n ∈ s, F n) : (a : X) → Y) (∑ n ∈ s, (⇑(F n) : (a : X) → Y)) →
        Eq (α := (a : X) → Y) (⇑(∑ n ∈ Insert.insert a s, F n) : (a : X) → Y)
          (∑ n ∈ Insert.insert a s, (⇑(F n) : (a : X) → Y))
⊢ Eq (α := (a : X) → Y) (⇑(∑ n ∈ s, F n) : (a : X) → Y) (∑ n ∈ s, (⇑(F n) : (a : X) → Y))

Tactic:
induction s using Finset.induction with
  | empty => simp_all
  | insert => simp_all

Premises used: Insert.insert
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommMonoid Y
ι : Type u_3
s : Finset ι
F : ι → locallyFinsuppWithin U Y
empty : Eq (α := (a : X) → Y) (⇑(∑ n ∈ ∅, F n) : (a : X) → Y) (∑ n ∈ ∅, (⇑(F n) : (a : X) → Y))
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      Eq (α := (a : X) → Y) (⇑(∑ n ∈ s, F n) : (a : X) → Y) (∑ n ∈ s, (⇑(F n) : (a : X) → Y)) →
        Eq (α := (a : X) → Y) (⇑(∑ n ∈ Insert.insert a s, F n) : (a : X) → Y)
          (∑ n ∈ Insert.insert a s, (⇑(F n) : (a : X) → Y))
⊢ Eq (α := (a : X) → Y) (⇑(∑ n ∈ s, F n) : (a : X) → Y) (∑ n ∈ s, (⇑(F n) : (a : X) → Y))

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp_all
  | insert => simp_all

Premises used: Insert.insert
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
⊢ Function.support F = Function.support.{u_3, u_1} (M := (a : X) → ℤ) fun (i : ι) ↦ (⇑(F i) : (a : X) → ℤ)

Tactic:
simp [Set.ext_iff, DFunLike.ext_iff, funext_iff]

Premises used: funext_iff, DFunLike.ext_iff, Set.ext_iff
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
⊢ Function.support F = Function.support.{u_3, u_1} (M := (a : X) → ℤ) fun (i : ι) ↦ (⇑(F i) : (a : X) → ℤ)

Tactic:
have : F.support = (fun i ↦ (F i : X → ℤ)).support := by
    simp [Set.ext_iff, DFunLike.ext_iff, funext_iff]
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
this : Function.support F = Function.support.{u_3, u_1} (M := (a : X) → ℤ) fun (i : ι) ↦ (⇑(F i) : (a : X) → ℤ)
pos :
  ∀ (h : (Function.support F).Finite),
    Eq.{u_1 + 1} (α := (a : X) → ℤ) (⇑(∑ᶠ (i : ι), F i) : (a : X) → ℤ) (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))
neg :
  ∀ (h : ¬(Function.support F).Finite),
    Eq.{u_1 + 1} (α := (a : X) → ℤ) (⇑(∑ᶠ (i : ι), F i) : (a : X) → ℤ) (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))
⊢ Eq.{u_1 + 1} (α := (a : X) → ℤ) (⇑(∑ᶠ (i : ι), F i) : (a : X) → ℤ) (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))

Tactic:
by_cases h : F.support.Finite

Premises used: Set.Finite, Function.support
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
this : Function.support F = Function.support.{u_3, u_1} (M := (a : X) → ℤ) fun (i : ι) ↦ (⇑(F i) : (a : X) → ℤ)
h : (Function.support F).Finite
pos :
  Eq.{u_1 + 1} (α := (a : X) → ℤ) (∑ n ∈ h.toFinset (s := Function.support F), (⇑(F n) : (a : X) → ℤ))
    (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))
⊢ Eq.{u_1 + 1} (α := (a : X) → ℤ) (⇑(∑ᶠ (i : ι), F i) : (a : X) → ℤ) (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))

Tactic:
rw [finsum_eq_sum F h, Function.locallyFinsuppWithin.coe_sum]

Premises used: finsum_eq_sum, Function.locallyFinsuppWithin.coe_sum
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
this : Function.support F = Function.support.{u_3, u_1} (M := (a : X) → ℤ) fun (i : ι) ↦ (⇑(F i) : (a : X) → ℤ)
h : (Function.support F).Finite
⊢ Set.Finite.{u_3} (α := ι) (Function.support.{u_3, u_1} (M := (a : X) → ℤ) fun (i : ι) ↦ (⇑(F i) : (a : X) → ℤ))

Tactic:
simp_all
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
this : Function.support F = Function.support.{u_3, u_1} (M := (a : X) → ℤ) fun (i : ι) ↦ (⇑(F i) : (a : X) → ℤ)
h : (Function.support F).Finite
⊢ Set.Finite.{u_3} (α := ι) (Function.support.{u_3, u_1} (M := (a : X) → ℤ) fun (i : ι) ↦ (⇑(F i) : (a : X) → ℤ))

Tactic:
have h₂ : (fun i ↦ (F i : X → ℤ)).support.Finite := by simp_all