awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₂ : Set.Finite.{u_3} (α := ι) (Function.support.{u_3, u_1} (M := (a : X) → ℤ) fun (i : ι) ↦ (⇑(F i) : (a : X) → ℤ))
⊢ Eq.{u_1 + 1} (α := (a : X) → ℤ) (∑ n ∈ h.toFinset (s := Function.support F), (⇑(F n) : (a : X) → ℤ))
    (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))

Tactic:
simp_all [finsum_eq_sum _ h₂]

Premises used: finsum_eq_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
⊢ Eq.{u_1 + 1} (α := (a : X) → ℤ) (⇑(∑ᶠ (i : ι), F i) : (a : X) → ℤ) (∑ᶠ (i : ι), (⇑(F i) : (a : X) → ℤ))

Tactic:
simp_all [finsum_of_infinite_support]

Premises used: finsum_of_infinite_support
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : LE Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
⊢ D₁ ≤ D₂ ↔ LE.le (α := (a : X) → Y) (⇑D₁ : (a : X) → Y) (⇑D₂ : (a : X) → Y)

Tactic:
⟨(·),(·)⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.LocallyFinsupp
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
simp : LE.le (α := (a : X) → Y) (⇑0 : (a : X) → Y) (Pi.single (M := fun (j : X) ↦ Y) x y) ↔ 0 ≤ y
⊢ LE.le (α := locallyFinsupp X Y) 0 (single x y) ↔ 0 ≤ y

Tactic:
simp only [le_def, coe_single]

Premises used: Function.locallyFinsuppWithin.le_def, Function.locallyFinsuppWithin.coe_single
-- Module: Mathlib.Topology.LocallyFinsupp
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 (α := (a : X) → Y) (⇑0 : (a : X) → Y) (Pi.single (M := fun (j : X) ↦ Y) x y) ↔ 0 ≤ y

Tactic:
apply Pi.single_nonneg

Premises used: Pi.single_nonneg
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Preorder Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
⊢ D₁ < D₂ ↔ LT.lt (α := (a : X) → Y) (⇑D₁ : (a : X) → Y) (⇑D₂ : (a : X) → Y)

Tactic:
⟨(·),(·)⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.LocallyFinsupp
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
rw : LT.lt (α := (a : X) → Y) (⇑0 : (a : X) → Y) (Pi.single (M := fun (j : X) ↦ Y) x y) ↔ 0 < y
⊢ LT.lt (α := locallyFinsupp X Y) 0 (single x y) ↔ 0 < y

Tactic:
rw [lt_def, coe_single]

Premises used: Function.locallyFinsuppWithin.coe_single, Function.locallyFinsuppWithin.lt_def
-- Module: Mathlib.Topology.LocallyFinsupp
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 (α := (a : X) → Y) (⇑0 : (a : X) → Y) (Pi.single (M := fun (j : X) ↦ Y) x y) ↔ 0 < y

Tactic:
Pi.single_pos

Premises used: Pi.single_pos
-- Module: Mathlib.Topology.LocallyFinsupp
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 (α := (a : X) → Y) (⇑0 : (a : X) → Y) (Pi.single (M := fun (j : X) ↦ Y) x y) ↔ 0 < y

Tactic:
exact Pi.single_pos

Premises used: Pi.single_pos
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
x : X
⊢ LT.lt (α := locallyFinsupp X ℕ) 0 (single x 1)

Tactic:
single_pos.2 Nat.one_pos

Premises used: Iff.mpr, Nat.one_pos, Function.locallyFinsuppWithin.single_pos
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
x : X
⊢ LT.lt (α := locallyFinsupp X ℤ) 0 (single x 1)

Tactic:
single_pos.2 Int.one_pos

Premises used: Iff.mpr, Function.locallyFinsuppWithin.single_pos, Int.one_pos
-- Module: Mathlib.Topology.LocallyFinsupp
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
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
⊢ 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

Tactic:
contrapose
-- Module: Mathlib.Topology.LocallyFinsupp
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
hx : 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:
simp [notMem_support.1 fun a ↦ hx (D₁.supportWithinDomain a),
        notMem_support.1 fun a ↦ hx (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 : SemilatticeSup Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
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
⊢ ∃ 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

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 : 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
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
⊢ ∃ 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

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 : 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
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
⊢ ∃ 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:
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 : 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
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)
⊢ (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:
apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.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 : 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
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)
⊢ a ∈ t₁ ∩ D₁.support (U := U) ∪ t₂ ∩ D₂.support (U := U)

Tactic:
simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]

Premises used: Set.mem_union, Set.mem_inter_iff, ne_eq, 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 : 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)
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
⊢ ¬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:
by_contra! hCon
-- Module: Mathlib.Topology.LocallyFinsupp
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)
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:
simp_all
-- Module: Mathlib.Topology.LocallyFinsupp
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
⊢ Eq.{u_2 + 1} (α := Y) ((D₁ ⊔ D₂ : (a : X) → Y) x : Y) ((D₁ : (a : X) → Y) x ⊔ (D₂ : (a : X) → Y) 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 : SemilatticeInf Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
x : X
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
⊢ 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

Tactic:
contrapose
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeInf Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
x : X
hx : 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:
simp [notMem_support.1 fun a ↦ hx (D₁.supportWithinDomain a),
        notMem_support.1 fun a ↦ hx (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 : SemilatticeInf Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
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
⊢ ∃ 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

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 : SemilatticeInf 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
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
⊢ ∃ 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

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 : SemilatticeInf 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
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
⊢ ∃ 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:
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 : SemilatticeInf 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
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)
⊢ (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:
apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.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 : SemilatticeInf 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
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)
⊢ a ∈ t₁ ∩ D₁.support (U := U) ∪ t₂ ∩ D₂.support (U := U)

Tactic:
simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]

Premises used: Set.mem_union, Set.mem_inter_iff, ne_eq, 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 : SemilatticeInf 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)
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
⊢ ¬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:
by_contra! hCon
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeInf 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)
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:
simp_all
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : SemilatticeInf Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((D₁ ⊓ D₂ : (a : X) → Y) x : Y) ((D₁ : (a : X) → Y) x ⊓ (D₂ : (a : X) → Y) 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 : Lattice Y
inst_2 : Zero Y
⊢ ∀ (a : locallyFinsuppWithin U Y), a ≤ a

Tactic:
simp [le_def]

Premises used: Function.locallyFinsuppWithin.le_def
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Lattice Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
h₁₂ : D₁ ≤ D₂
h₂₁ : D₂ ≤ D₁
h : ∀ (x : X), Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) x : Y) ((D₂ : (a : X) → Y) x : Y)
⊢ D₁ = D₂

Tactic:
ext x
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Lattice Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
h₁₂ : D₁ ≤ D₂
h₂₁ : D₂ ≤ D₁
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) x : Y) ((D₂ : (a : X) → Y) x : Y)

Tactic:
le_antisymm (h₁₂ x) (h₂₁ x)

Premises used: le_antisymm
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Lattice Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
h₁₂ : D₁ ≤ D₂
h₂₁ : D₂ ≤ D₁
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((D₁ : (a : X) → Y) x : Y) ((D₂ : (a : X) → Y) x : Y)

Tactic:
exact le_antisymm (h₁₂ x) (h₂₁ x)

Premises used: le_antisymm
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Lattice Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ LE.le.{u_2} (α := (fun (a : X) ↦ Y) x) ((D₁ : (a : X) → Y) x : Y) ((D₁ ⊔ D₂ : (a : X) → Y) x : Y)

Tactic:
simp
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Lattice Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ LE.le.{u_2} (α := (fun (a : X) ↦ Y) x) ((D₂ : (a : X) → Y) x : Y) ((D₁ ⊔ D₂ : (a : X) → Y) x : Y)

Tactic:
simp
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Lattice Y
inst_2 : Zero Y
D₁ D₂ D₃ : locallyFinsuppWithin U Y
h₁₃ : D₁ ≤ D₃
h₂₃ : D₂ ≤ D₃
x : X
⊢ LE.le.{u_2} (α := (fun (a : X) ↦ Y) x) ((D₁ ⊔ D₂ : (a : X) → Y) x : Y) ((D₃ : (a : X) → Y) x : Y)

Tactic:
simp [h₁₃ x, h₂₃ x]
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Lattice Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ LE.le.{u_2} (α := (fun (a : X) ↦ Y) x) ((D₁ ⊓ D₂ : (a : X) → Y) x : Y) ((D₁ : (a : X) → Y) x : Y)

Tactic:
simp
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Lattice Y
inst_2 : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ LE.le.{u_2} (α := (fun (a : X) ↦ Y) x) ((D₁ ⊓ D₂ : (a : X) → Y) x : Y) ((D₂ : (a : X) → Y) x : Y)

Tactic:
simp
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Lattice Y
inst_2 : Zero Y
D₁ D₂ D₃ : locallyFinsuppWithin U Y
h₁₃ : D₁ ≤ D₂
h₂₃ : D₁ ≤ D₃
x : X
⊢ LE.le.{u_2} (α := (fun (a : X) ↦ Y) x) ((D₁ : (a : X) → Y) x : Y) ((D₂ ⊓ D₃ : (a : X) → Y) x : Y)

Tactic:
simp [h₁₃ x, h₂₃ x]
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Lattice Y
inst_2 : AddCommGroup Y
a : locallyFinsuppWithin U Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((a⁺ : (a : X) → Y) x : Y) (((a : (a : X) → Y) 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 : Lattice Y
inst_2 : AddCommGroup Y
a : locallyFinsuppWithin U Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((a⁻ : (a : X) → Y) x : Y) (((a : (a : X) → Y) 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 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
x x_1 : locallyFinsuppWithin U Y
h : x ≤ x_1
x_2 : locallyFinsuppWithin U Y
⊢ x + x_2 ≤ x_1 + x_2

Tactic:
simpa [le_def]

Premises used: Function.locallyFinsuppWithin.le_def
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
rw : (f₁ + f₂) ⊔ 0 ≤ f₁⁺ + f₂⁺
⊢ (f₁ + f₂)⁺ ≤ f₁⁺ + f₂⁺

Tactic:
rw [posPart_def]

Premises used: posPart_def
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
rw : (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂⁺
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁⁺ + f₂⁺

Tactic:
rw [posPart_def]

Premises used: posPart_def
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
rw : (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂ ⊔ 0
⊢ (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂⁺

Tactic:
rw [posPart_def]

Premises used: posPart_def
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
repeat : (f₁ + f₂) ⊔ 0 ≤ f₁ ⊔ 0 + f₂ ⊔ 0
⊢ (f₁ + f₂)⁺ ≤ f₁⁺ + f₂⁺

Tactic:
repeat rw [posPart_def]

Premises used: posPart_def
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
simp :
  HAdd.hAdd (α := Y) (β := Y) ((f₁ : (a : X) → Y) x : Y) ((f₂ : (a : X) → Y) x : Y) ≤
      HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y) ∧
    0 ≤ HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y)
⊢ LE.le.{u_2} (α := (fun (a : X) ↦ Y) x) (((f₁ + f₂) ⊔ 0 : (a : X) → Y) x : Y) ((f₁ ⊔ 0 + f₂ ⊔ 0 : (a : X) → Y) x : Y)

Tactic:
simp only [Function.locallyFinsuppWithin.max_apply, Function.locallyFinsuppWithin.coe_add,
    Pi.add_apply, Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, sup_le_iff]

Premises used: Pi.zero_apply, Pi.add_apply, sup_le_iff, Function.locallyFinsuppWithin.coe_add, Function.locallyFinsuppWithin.coe_zero, Function.locallyFinsuppWithin.max_apply