awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
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
⊢ x ∈ D.support (U := U)
have hx₁ : ¬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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ x ∈ D.support (U := U)
have 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
Tactic: tauto
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
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
⊢ IsDiscrete (D.support (U := U))
have this : 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
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ IsDiscrete (D.support (U := U))
have rw : IsDiscrete ({x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ IsDiscrete ({x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜ ∩ U)
have h : {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜᶜ ∈ codiscreteWithin U
Tactic: apply isDiscrete_of_codiscreteWithin
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)}ᶜᶜ ∈ codiscreteWithin U
have h : {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)} ∈ codiscreteWithin U
Tactic: rw [compl_compl]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ {x : X | Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)} ∈ codiscreteWithin U
have h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) (⇑D : (a : X) → Y)).Finite
Tactic: apply (supportDiscreteWithin_iff_locallyFiniteWithin D.supportWithinDomain).2
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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] (D.support (U := U))
have 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}
Tactic: convert!
    isClosed_sdiff_of_codiscreteWithin
      ((supportDiscreteWithin_iff_locallyFiniteWithin D.supportWithinDomain).2
        D.supportLocallyFiniteWithinDomain)
      hU
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ 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}
have 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}
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ 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}
have 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}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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}
⊢ 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}
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} (f + g)
have left : Function.support (f + g) ⊆ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} (f + g)
have right : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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)
⊢ x ∈ U
have left : ∀ (hx : x ∉ U), x ∉ Function.support (f + g)
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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 ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
have right : ∀ (t₁ : Set X) (ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite), ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
Tactic: obtain ⟨t₁, ht₁⟩ := hf.2 z hz
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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 ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
have right : ∀ (t₂ : Set X) (ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite), ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
Tactic: obtain ⟨t₂, ht₂⟩ := hg.2 z hz
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
have right : (t₁ ∩ t₂ ∩ Function.support (f + g)).Finite
Tactic: use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ (t₁ ∩ t₂ ∩ Function.support (f + g)).Finite
have right : t₁ ∩ t₂ ∩ Function.support (f + g) ⊆ t₁ ∩ Function.support f ∪ t₂ ∩ Function.support g
Tactic: apply Set.Finite.subset (s := (t₁ ∩ f.support) ∪ (t₂ ∩ g.support)) (ht₁.2.union ht₂.2)
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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)
⊢ a ∈ t₁ ∩ Function.support f ∪ t₂ ∩ Function.support g
have 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
Tactic: simp_all only [support_subset_iff, ne_eq, mem_setOf_eq,
        mem_inter_iff, mem_support, Pi.add_apply, mem_union, true_and]
Cleared hypotheses: hf, hg, hz, ht₁, ht₂, ha
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ ¬f a = 0 ∨ ¬g a = 0
have right : ∀ (hCon : f a = 0 ∧ g a = 0), False
Tactic: by_contra! hCon
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddMonoid Y
⊢ Membership.mem (γ := Set (X → Y))
    {f : X → Y | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite} 0
have simp : ∀ z ∈ U, ∃ (t : Set X), t ∈ 𝓝 z
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]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ Eq (α := (a : X) → Y) (⇑(∑ n ∈ s, F n) : (a : X) → Y) (∑ n ∈ s, (⇑(F n) : (a : X) → Y))
have empty : Eq (α := (a : X) → Y) (⇑(∑ n ∈ ∅, F n) : (a : X) → Y) (∑ n ∈ ∅, (⇑(F n) : (a : X) → Y))
Tactic: induction s using Finset.induction with
  | empty => simp_all
  | insert => simp_all
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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))
⊢ Eq (α := (a : X) → Y) (⇑(∑ n ∈ s, F n) : (a : X) → Y) (∑ n ∈ s, (⇑(F n) : (a : X) → Y))
have 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 a s, F n) : (a : X) → Y) (∑ n ∈ insert a s, (⇑(F n) : (a : X) → Y))
Tactic: induction s using Finset.induction with
  | empty => simp_all
  | insert => simp_all
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ Eq (α := (a : X) → Y) (⇑(∑ n ∈ s, F n) : (a : X) → Y) (∑ n ∈ s, (⇑(F n) : (a : X) → Y))
have empty : Eq (α := (a : X) → Y) (⇑(∑ n ∈ ∅, F n) : (a : X) → Y) (∑ n ∈ ∅, (⇑(F n) : (a : X) → Y))
Tactic: classical
  induction s using Finset.induction with
  | empty => simp_all
  | insert => simp_all
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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))
⊢ Eq (α := (a : X) → Y) (⇑(∑ n ∈ s, F n) : (a : X) → Y) (∑ n ∈ s, (⇑(F n) : (a : X) → Y))
have 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 a s, F n) : (a : X) → Y) (∑ n ∈ insert a s, (⇑(F n) : (a : X) → Y))
Tactic: classical
  induction s using Finset.induction with
  | empty => simp_all
  | insert => simp_all
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
ι : Type u_3
F : ι → locallyFinsuppWithin U ℤ
⊢ Eq.{u_1 + 1} (α := (a : X) → ℤ) (⇑(∑ᶠ (i : ι), F i) : (a : X) → ℤ) (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))
have this : 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]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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) → ℤ)
⊢ Eq.{u_1 + 1} (α := (a : X) → ℤ) (⇑(∑ᶠ (i : ι), F i) : (a : X) → ℤ) (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))
have pos : ∀ (h : (Function.support F).Finite),
  Eq.{u_1 + 1} (α := (a : X) → ℤ) (⇑(∑ᶠ (i : ι), F i) : (a : X) → ℤ) (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))
Tactic: by_cases h : F.support.Finite
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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) → ℤ))
⊢ Eq.{u_1 + 1} (α := (a : X) → ℤ) (⇑(∑ᶠ (i : ι), F i) : (a : X) → ℤ) (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))
have neg : ∀ (h : ¬(Function.support F).Finite),
  Eq.{u_1 + 1} (α := (a : X) → ℤ) (⇑(∑ᶠ (i : ι), F i) : (a : X) → ℤ) (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))
Tactic: by_cases h : F.support.Finite
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
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
⊢ Eq.{u_1 + 1} (α := (a : X) → ℤ) (⇑(∑ᶠ (i : ι), F i) : (a : X) → ℤ) (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))
have pos : Eq.{u_1 + 1} (α := (a : X) → ℤ) (∑ n ∈ h.toFinset (s := Function.support F), (⇑(F n) : (a : X) → ℤ))
  (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))
Tactic: rw [finsum_eq_sum F h, Function.locallyFinsuppWithin.coe_sum]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := (a : X) → ℤ) (∑ n ∈ h.toFinset (s := Function.support F), (⇑(F n) : (a : X) → ℤ))
    (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))
have h₂ : 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
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
inst_3 : Preorder Y
x : X
y : Y
⊢ LE.le (α := locallyFinsupp X Y) 0 (single x y) ↔ 0 ≤ y
have simp : LE.le (α := (a : X) → Y) (⇑0 : (a : X) → Y) (Pi.single (M := fun (j : X) ↦ Y) x y) ↔ 0 ≤ y
Tactic: simp only [le_def, coe_single]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : Zero Y
inst_3 : Preorder Y
x : X
y : Y
⊢ LT.lt (α := locallyFinsupp X Y) 0 (single x y) ↔ 0 < y
have rw : LT.lt (α := (a : X) → Y) (⇑0 : (a : X) → Y) (Pi.single (M := fun (j : X) ↦ Y) x y) ↔ 0 < y
Tactic: rw [lt_def, coe_single]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeSup Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ Membership.mem (γ := Set X)
      (Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊔ (D₂ : (a : X) → Y) z) x →
    x ∈ U
have contrapose : x ∉ U → x ∉ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊔ (D₂ : (a : X) → Y) z
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeSup Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊔ (D₂ : (a : X) → Y) z).Finite
have obtain : ∀ (t₁ : Set X) (ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite),
  ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊔ (D₂ : (a : X) → Y) z).Finite
Tactic: obtain ⟨t₁, ht₁⟩ := D₁.supportLocallyFiniteWithinDomain z hz
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeSup Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊔ (D₂ : (a : X) → Y) z).Finite
have obtain : ∀ (t₂ : Set X) (ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support (U := U)).Finite),
  ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊔ (D₂ : (a : X) → Y) z).Finite
Tactic: obtain ⟨t₂, ht₂⟩ := D₂.supportLocallyFiniteWithinDomain z hz
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeSup Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support (U := U)).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊔ (D₂ : (a : X) → Y) z).Finite
have right : (t₁ ∩ t₂ ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊔ (D₂ : (a : X) → Y) z).Finite
Tactic: use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeSup Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support (U := U)).Finite
⊢ (t₁ ∩ t₂ ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊔ (D₂ : (a : X) → Y) z).Finite
have right : (t₁ ∩ t₂ ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊔ (D₂ : (a : X) → Y) z) ⊆
  t₁ ∩ D₁.support (U := U) ∪ t₂ ∩ D₂.support (U := U)
Tactic: apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.support)) (ht₁.2.union ht₂.2)
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeSup Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support (U := U)).Finite
a : X
ha : a ∈ t₁ ∩ t₂ ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ (D₁ : (a : X) → Y) z ⊔ (D₂ : (a : X) → Y) z
⊢ a ∈ t₁ ∩ D₁.support (U := U) ∪ t₂ ∩ D₂.support (U := U)
have right : ∀ (ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) a ⊔ (D₂ : (a : X) → Y) a : Y) (0 : Y)),
  ¬Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) a : Y) (0 : Y) ∨ ¬Eq.{u_2 + 1} (α := Y) ((D₂ : (a : X) → Y) a : Y) (0 : Y)
Tactic: simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeSup Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support (U := U)).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support (U := U)).Finite
a : X
ha : (a ∈ t₁ ∧ a ∈ t₂) ∧ ¬Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) a ⊔ (D₂ : (a : X) → Y) a : Y) (0 : Y)
⊢ ¬Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) a : Y) (0 : Y) ∨ ¬Eq.{u_2 + 1} (α := Y) ((D₂ : (a : X) → Y) a : Y) (0 : Y)
have right : ∀
  (hCon :
    Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) a : Y) (0 : Y) ∧
      Eq.{u_2 + 1} (α := Y) ((D₂ : (a : X) → Y) a : Y) (0 : Y)),
  False
Tactic: by_contra! hCon