awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst] (s i)
x y : X
hy : Membership.mem (γ := Set X) (⋂ (i : ι), ⋂ (_ : x ∉ s i), (s i)ᶜ) y
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | y ∈ s i} i
⊢ ∀ (i : ι) (i_1 : x ∉ s i), y ∉ s i

Tactic:
push _ ∈ _ at hy
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst] (s i)
x y : X
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | y ∈ s i} i
hy : ∀ (i : ι) (i_1 : x ∉ s i), y ∉ s i
⊢ Membership.mem (γ := Set ι) {i : ι | x ∈ s i} i

Tactic:
not_imp_not.mp (hy i) hi

Premises used: Set.Mem, setOf, Iff.mp, not_imp_not
-- Module: Mathlib.Topology.LocallyFinite
Goal:
ι : Type u_1
X : Type u_4
inst : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst] (s i)
x y : X
i : ι
hi : Membership.mem (γ := Set ι) {i : ι | y ∈ s i} i
hy : ∀ (i : ι) (i_1 : x ∉ s i), y ∉ s i
⊢ Membership.mem (γ := Set ι) {i : ι | x ∈ s i} i

Tactic:
exact not_imp_not.mp (hy i) hi

Premises used: Iff.mp, not_imp_not
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
⊢ (support.{u_1, u_2} (M := Y) fun (x : X) ↦ 0) ⊆ U

Tactic:
simp
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
z : X
hz : z ∈ U
simp_rw : ∃ (t : Set X), t ∈ 𝓝 z
⊢ ∃ t ∈ 𝓝 z, (t ∩ support.{u_1, u_2} (M := Y) fun (x : X) ↦ 0).Finite

Tactic:
simp_rw [support_fun_zero, inter_empty, finite_empty, and_true]

Premises used: Set.finite_empty, and_true, Function.support_fun_zero, Set.inter_empty
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
z : X
hz : z ∈ U
w : Set X
h : univ ∈ 𝓝 z
⊢ ∃ (t : Set X), t ∈ 𝓝 z

Tactic:
use Set.univ, univ_mem

Premises used: Set.univ, Filter.univ_mem
-- 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
f : X → Y
h : support f ⊆ U
h₁ : ∀ (x : X), x ∈ support f ↔ x ∈ U \ {x : X | f x = 0 x}
⊢ support f = U \ {x : X | f x = 0 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
f : X → Y
h : support f ⊆ U
x : X
h₁ : ¬f x = 0 → x ∈ U
⊢ x ∈ support f ↔ x ∈ U \ {x : X | f x = 0 x}

Tactic:
simp only [mem_support, ne_eq, Pi.zero_apply, mem_diff, mem_setOf_eq, iff_and_self]

Premises used: Pi.zero_apply, Set.mem_setOf_eq, ne_eq, Set.mem_diff, Function.mem_support, iff_and_self
-- 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
f : X → Y
h : support f ⊆ U
x : X
⊢ ¬f x = 0 → x ∈ U

Tactic:
(h ·)
-- 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
f : X → Y
h : support f ⊆ U
x : X
⊢ ¬f x = 0 → x ∈ U

Tactic:
exact (h ·)
-- 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
f : X → Y
h : support f ⊆ U
⊢ support f = U \ {x : X | f x = 0 x}

Tactic:
have : f.support = (U \ {x | f x = (0 : X → Y) x}) := by
    ext x
    simp only [mem_support, ne_eq, Pi.zero_apply, mem_diff, mem_setOf_eq, iff_and_self]
    exact (h ·)
-- 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
f : X → Y
h : support f ⊆ U
this : support f = U \ {x : X | f x = 0 x}
rw : (∀ᶠ (x : X) in codiscreteWithin U, f x = 0 x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
rw₁ : {x : X | f x = 0 x} ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
rw₂ : (∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | f x = 0 x})).Finite) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite
rw₃ rw₄ :
  (∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | f x = 0 x})).Finite) ↔
    ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | f x = 0 x})).Finite
⊢ f =ᶠ[codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite

Tactic:
rw [EventuallyEq, Filter.Eventually, codiscreteWithin_iff_locallyFiniteComplementWithin, this]

Premises used: Filter.Eventually, Filter.EventuallyEq, codiscreteWithin_iff_locallyFiniteComplementWithin
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
f : X → Y
h :
  ∀ (z : X) (t : Set X) (ht : t ∈ 𝓝 z),
    Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ t).Nonempty} ↔
      (t ∩ support f).Finite
⊢ (∀ (x : X),
      ∃ t ∈ 𝓝 x,
        Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ t).Nonempty}) ↔
    LocallyFiniteSupport f

Tactic:
peel with z t ht
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
f : X → Y
z : X
t : Set X
ht : t ∈ 𝓝 z
⊢ t ∩ support f =
    image (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
      {i : (↑(support f) : Type u_1) | (↑i : X) ∈ t}

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
f : X → Y
z : X
t : Set X
ht : t ∈ 𝓝 z
⊢ t ∩ support f =
    image (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
      {i : (↑(support f) : Type u_1) | (↑i : X) ∈ t}

Tactic:
have aux1 : t ∩ f.support = {i : f.support | ↑i ∈ t} := by aesop
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
f : X → Y
z : X
t : Set X
ht : t ∈ 𝓝 z
aux1 :
  t ∩ support f =
    image (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
      {i : (↑(support f) : Type u_1) | (↑i : X) ∈ t}
⊢ InjOn.{u_1, u_1} (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
    {i : (↑(support f) : Type u_1) | (↑i : X) ∈ t}

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
f : X → Y
z : X
t : Set X
ht : t ∈ 𝓝 z
aux1 :
  t ∩ support f =
    image (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
      {i : (↑(support f) : Type u_1) | (↑i : X) ∈ t}
⊢ InjOn.{u_1, u_1} (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
    {i : (↑(support f) : Type u_1) | (↑i : X) ∈ t}

Tactic:
have aux2 : InjOn Subtype.val {i : f.support | ↑i ∈ t} := by aesop
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
f : X → Y
z : X
t : Set X
ht : t ∈ 𝓝 z
aux1 :
  t ∩ support f =
    image (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
      {i : (↑(support f) : Type u_1) | (↑i : X) ∈ t}
aux2 :
  InjOn.{u_1, u_1} (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
    {i : (↑(support f) : Type u_1) | (↑i : X) ∈ t}
⊢ Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ t).Nonempty} ↔
    (t ∩ support f).Finite

Tactic:
simp only [singleton_inter_nonempty, aux1, finite_image_iff aux2]

Premises used: Set.finite_image_iff, Set.singleton_inter_nonempty
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
f : X → Y
h : LocallyFiniteSupport f
⊢ LocallyFinite (X := X) fun (s : (↑(support f) : Type u_1)) ↦ {(↑s : X)}

Tactic:
(LocallyFiniteSupport.iff_locallyFinite_support f).mpr h

Premises used: Iff.mpr, LocallyFiniteSupport.iff_locallyFinite_support
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
W : Set X
inst_1 : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
⊢ Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty}

Tactic:
have := LocallyFinite.finite_nonempty_inter_compact
    (LocallyFiniteSupport.locallyFinite_support f h) hW
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
W : Set X
inst_1 : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty}
α : Type u_1
s t : Set α
⊢ image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      {i : (↑s : Type u_1) | ({(↑i : α)} ∩ t).Nonempty} =
    t ∩ s

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
W : Set X
inst_1 : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty}
⊢ ∀ {α : Type u_1} (s t : Set α),
    image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        {i : (↑s : Type u_1) | ({(↑i : α)} ∩ t).Nonempty} =
      t ∩ s

Tactic:
have lem {α : Type u_1} (s t : Set α) : {i : s | ({↑i} ∩ t).Nonempty} = (t ∩ s) := by aesop
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
W : Set X
inst_1 : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty}
lem :
  ∀ {α : Type u_1} (s t : Set α),
    image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        {i : (↑s : Type u_1) | ({(↑i : α)} ∩ t).Nonempty} =
      t ∩ s
rw :
  Set.Finite.{u_1} (α := X)
    (image (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
      {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty})
⊢ (W ∩ support f).Finite

Tactic:
rw [← lem f.support W]

Premises used: Function.support
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
W : Set X
inst_1 : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty}
lem :
  ∀ {α : Type u_1} (s t : Set α),
    image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        {i : (↑s : Type u_1) | ({(↑i : α)} ∩ t).Nonempty} =
      t ∩ s
⊢ Set.Finite.{u_1} (α := X)
    (image (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
      {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty})

Tactic:
Finite.image Subtype.val this

Premises used: Set.Finite.image, Subtype.val
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
W : Set X
inst_1 : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : Set.Finite.{u_1} (α := (↑(support f) : Type u_1)) {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty}
lem :
  ∀ {α : Type u_1} (s t : Set α),
    image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        {i : (↑s : Type u_1) | ({(↑i : α)} ∩ t).Nonempty} =
      t ∩ s
⊢ Set.Finite.{u_1} (α := X)
    (image (α := { x : X // x ∈ support f }) (Subtype.val (p := fun (x : X) ↦ x ∈ support f))
      {i : (↑(support f) : Type u_1) | ({(↑i : X)} ∩ W).Nonempty})

Tactic:
exact Finite.image Subtype.val this

Premises used: Set.Finite.image, Subtype.val
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
f : locallyFinsupp X Y
x : X
⊢ Membership.mem (γ := Set X) univ x

Tactic:
trivial
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
x x_1 : locallyFinsuppWithin U Y
toFun : X → Y
supportWithinDomain' : support toFun ⊆ U
supportLocallyFiniteWithinDomain' : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support toFun).Finite
toFun_1 : X → Y
supportWithinDomain'_1 : support toFun_1 ⊆ U
supportLocallyFiniteWithinDomain'_1 : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support toFun_1).Finite
⊢ Eq (α := (a : X) → Y)
      ((fun (D : locallyFinsuppWithin U Y) ↦ D.toFun (U := U))
        (mk (U := U) toFun supportWithinDomain' supportLocallyFiniteWithinDomain'))
      ((fun (D : locallyFinsuppWithin U Y) ↦ D.toFun (U := U))
        (mk (U := U) toFun_1 supportWithinDomain'_1 supportLocallyFiniteWithinDomain'_1)) →
    mk (U := U) toFun supportWithinDomain' supportLocallyFiniteWithinDomain' =
      mk (U := U) toFun_1 supportWithinDomain'_1 supportLocallyFiniteWithinDomain'_1

Tactic:
simp
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
D : locallyFinsuppWithin U Y
⊢ D.support (U := U) ⊆ U

Tactic:
D.supportWithinDomain'

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 : Zero Y
D : locallyFinsuppWithin U Y
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ D.support (U := U)).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
D₁ D₂ : locallyFinsuppWithin U Y
h : ∀ (a : X), Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) a : Y) ((D₂ : (a : X) → Y) a : Y)
⊢ D₁ = D₂

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
⊢ Injective (β := (a : X) → Y) fun (x : locallyFinsuppWithin U Y) ↦ (⇑x : (a : X) → Y)

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x : X
y : Y
z : X
hz : z ∈ Function.support.{u_1, u_2} (M := Y) (Pi.single (M := fun (a : X) ↦ Y) x y)
⊢ Membership.mem (γ := Set X) univ z

Tactic:
tauto
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x : X
y : Y
x_1 : X
h : Membership.mem (γ := Set X) univ x_1
⊢ (univ ∩ Function.support.{u_1, u_2} (M := Y) (Pi.single (M := fun (a : X) ↦ Y) x y)).Finite

Tactic:
simpa using (finite_singleton x).subset Pi.support_single_subset

Premises used: Set.Finite.subset, Pi.support_single_subset, Set.finite_singleton
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x₁ x₂ : X
y : Y
simp_rw : toFun (U := univ) (single x₁ y) x₂ = if x₂ = x₁ then y else 0
simp_rw₁ : Pi.single (M := fun (a : X) ↦ Y) x₁ y x₂ = if x₂ = x₁ then y else 0
⊢ (single x₁ y : (a : X) → Y) x₂ = if x₂ = x₁ then y else 0

Tactic:
simp_rw [DFunLike.coe, single, Pi.single_apply]

Premises used: Function.locallyFinsuppWithin.single, Pi.single_apply, DFunLike.coe
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x₁ x₂ : X
y : Y
simp_rw : toFun (U := univ) (single x₁ y) x₂ = if x₂ = x₁ then y else 0
simp_rw₁ : Pi.single (M := fun (a : X) ↦ Y) x₁ y x₂ = if x₂ = x₁ then y else 0
⊢ (single x₁ y : (a : X) → Y) x₂ = if x₂ = x₁ then y else 0

Tactic:
classical
  simp_rw [DFunLike.coe, single, Pi.single_apply]

Premises used: Function.locallyFinsuppWithin.single, Pi.single_apply, DFunLike.coe
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x : X
⊢ Eq (α := locallyFinsupp X Y) (single x 0) 0

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x : X
y : Y
h :
  ∀ (x_1 : X), Eq.{u_2 + 1} (α := Y) ((single x y : (a : X) → Y) x_1 : Y) (Pi.single (M := fun (j : X) ↦ Y) x y x_1 : Y)
⊢ Eq (α := (a : X) → Y) (⇑(single x y) : (a : X) → Y) (Pi.single (M := fun (j : X) ↦ Y) x y)

Tactic:
ext
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
x : X
y : Y
x_1 : X
⊢ Eq.{u_2 + 1} (α := Y) ((single x y : (a : X) → Y) x_1 : Y) (Pi.single (M := fun (j : X) ↦ Y) x y x_1 : Y)

Tactic:
simp [Pi.single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
z : X
D : locallyFinsuppWithin U Y
hz : z ∉ U
⊢ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) z : Y) (0 : Y)

Tactic:
notMem_support.mp fun a ↦ hz (D.supportWithinDomain a)

Premises used: Function.notMem_support, Function.locallyFinsuppWithin.supportWithinDomain, Iff.mp
-- 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
apply :
  ∀ z ∈ U,
    ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x})).Finite
⊢ EventuallyEq.{u_1, u_2} (β := Y) (codiscreteWithin U) (⇑D : (a : X) → Y) 0

Tactic:
apply codiscreteWithin_iff_locallyFiniteComplementWithin.2

Premises used: Iff.mpr, codiscreteWithin_iff_locallyFiniteComplementWithin
-- 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
h : ∀ (x : X), x ∈ D.support (U := U) ↔ x ∈ U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}
⊢ D.support (U := U) = U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}

Tactic:
ext x
-- 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
x : X
h : ¬Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y) → x ∈ U
⊢ x ∈ D.support (U := U) ↔ x ∈ U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}

Tactic:
simp only [mem_support, ne_eq, Pi.zero_apply, Set.mem_diff, Set.mem_setOf_eq, iff_and_self]

Premises used: Pi.zero_apply, Set.mem_setOf_eq, ne_eq, Set.mem_diff, Function.mem_support, iff_and_self
-- 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
x : X
⊢ ¬Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y) → x ∈ U

Tactic:
(support_subset_iff.1 D.supportWithinDomain) x

Premises used: Function.support_subset_iff, Function.locallyFinsuppWithin.supportWithinDomain, Iff.mp
-- 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
x : X
⊢ ¬Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y) → x ∈ U

Tactic:
exact (support_subset_iff.1 D.supportWithinDomain) x

Premises used: Function.support_subset_iff, Function.locallyFinsuppWithin.supportWithinDomain, Iff.mp
-- 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
⊢ D.support (U := U) = U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}

Tactic:
have : D.support = (U \ {x | D x = (0 : X → Y) x}) := by
    ext x
    simp only [mem_support, ne_eq, Pi.zero_apply, Set.mem_diff, Set.mem_setOf_eq, iff_and_self]
    exact (support_subset_iff.1 D.supportWithinDomain) x
-- 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) = U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}
rw : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ D.support (U := U)).Finite
⊢ ∀ z ∈ U,
    ∃ t ∈ 𝓝 z, (t ∩ (U \ {x : X | (fun (x : X) ↦ Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)) x})).Finite

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) = U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ D.support (U := U)).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) = U \ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 x : Y)}
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ D.support (U := U)).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 : Zero Y
inst_2 : T1Space X
D : locallyFinsuppWithin U Y
h : ∀ (x : X), x ∈ D.support (U := U) ↔ x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
⊢ D.support (U := U) = {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U

Tactic:
ext x
-- 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
x : X
h : x ∈ D.support (U := U) → x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
h₁ : x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U → x ∈ D.support (U := U)
⊢ x ∈ D.support (U := U) ↔ x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U

Tactic:
constructor
-- 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
x : X
hx : x ∈ D.support (U := U)
⊢ Membership.mem (γ := Set X) {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ x

Tactic:
tauto
-- 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
x : X
⊢ x ∈ D.support (U := U) → x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U

Tactic:
exact fun hx ↦ ⟨by tauto, D.supportWithinDomain hx⟩
-- 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
x : X
hx : x ∈ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U
⊢ ¬Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y) ∧ x ∈ U

Tactic:
rw [mem_inter_iff, mem_compl_iff, mem_setOf_eq] at hx

Premises used: Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_compl_iff
-- 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
x : X
hx : ¬Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y) ∧ x ∈ U
h :
  Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y) →
    ¬Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y) → x ∈ U → False
⊢ x ∈ D.support (U := U)

Tactic:
tauto
-- 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
⊢ D.support (U := U) = {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U

Tactic:
have : D.support = {x | D x = 0}ᶜ ∩ U := by
    ext x
    constructor
    · exact fun hx ↦ ⟨by tauto, D.supportWithinDomain hx⟩
    · intro hx
      rw [mem_inter_iff, mem_compl_iff, mem_setOf_eq] at hx
      tauto