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 : AddCommGroup Y
inst_2 : LinearOrder Y
inst_3 : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
left :
  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)
right : 0 ≤ HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y)
⊢ 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)

Tactic:
constructor
-- 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
⊢ 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)

Tactic:
simp [add_le_add]

Premises used: add_le_add
-- 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
⊢ 0 ≤ HAdd.hAdd (α := Y) (β := Y) (max ((f₁ : (a : X) → Y) x) 0 : Y) (max ((f₂ : (a : X) → Y) x) 0 : Y)

Tactic:
simp [add_nonneg]

Premises used: add_nonneg
-- 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 [negPart_def]

Premises used: negPart_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 [negPart_def]

Premises used: negPart_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 [negPart_def]

Premises used: negPart_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 [negPart_def]

Premises used: negPart_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 [neg_add_rev, Function.locallyFinsuppWithin.max_apply,
    Function.locallyFinsuppWithin.coe_add, Function.locallyFinsuppWithin.coe_neg, Pi.add_apply,
    Pi.neg_apply, Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, sup_le_iff]

Premises used: neg_add_rev, Pi.zero_apply, Pi.add_apply, sup_le_iff, Function.locallyFinsuppWithin.coe_add, Function.locallyFinsuppWithin.coe_zero, Pi.neg_apply, Function.locallyFinsuppWithin.coe_neg, Function.locallyFinsuppWithin.max_apply
-- 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
left :
  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)
right : 0 ≤ HAdd.hAdd (α := Y) (β := Y) (max (-(f₁ : (a : X) → Y) x) 0 : Y) (max (-(f₂ : (a : X) → Y) x) 0 : Y)
⊢ 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)

Tactic:
constructor
-- 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
⊢ 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)

Tactic:
simp [add_comm, add_le_add]

Premises used: add_le_add, add_comm
-- 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
⊢ 0 ≤ HAdd.hAdd (α := Y) (β := Y) (max (-(f₁ : (a : X) → Y) x) 0 : Y) (max (-(f₂ : (a : X) → Y) x) 0 : Y)

Tactic:
simp [add_nonneg]

Premises used: add_nonneg
-- 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
n : ℕ
f : locallyFinsuppWithin U Y
h : ∀ (x : X), Eq.{u_2 + 1} (α := Y) (((n • f)⁺ : (a : X) → Y) x : Y) ((n • f⁺ : (a : X) → Y) x : Y)
⊢ (n • f)⁺ = n • f⁺

Tactic:
ext x
-- 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
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)
⊢ Eq.{u_2 + 1} (α := Y) (((n • f)⁺ : (a : X) → Y) x : Y) ((n • f⁺ : (a : X) → Y) x : Y)

Tactic:
simp only [posPart, max_apply, coe_nsmul, Pi.smul_apply, coe_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, PosPart.posPart, Function.locallyFinsuppWithin.coe_nsmul, Function.locallyFinsuppWithin.coe_zero, Function.locallyFinsuppWithin.max_apply, Pi.smul_apply
-- 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
n : ℕ
f : locallyFinsuppWithin U Y
x : X
pos :
  ∀ (h : LT.lt.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) (0 : Y)),
    max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)
neg :
  ∀ (h : ¬LT.lt.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) (0 : Y)),
    max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)
⊢ max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)

Tactic:
by_cases h : f x < 0

Premises used: DFunLike.coe
-- 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
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : LT.lt.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) (0 : Y)
⊢ max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)

Tactic:
simpa [max_eq_right_of_lt h] using nsmul_le_nsmul_right h.le n

Premises used: max_eq_right_of_lt, nsmul_le_nsmul_right, LT.lt.le
-- 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
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : ¬LT.lt.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) (0 : Y)
⊢ max (HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max ((f : (a : X) → Y) x) 0 : Y)

Tactic:
simpa [not_lt.1 h] using nsmul_nonneg (not_lt.1 h) n

Premises used: nsmul_nonneg, not_lt, Iff.mp
-- 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
n : ℕ
f : locallyFinsuppWithin U Y
h : ∀ (x : X), Eq.{u_2 + 1} (α := Y) (((n • f)⁻ : (a : X) → Y) x : Y) ((n • f⁻ : (a : X) → Y) x : Y)
⊢ (n • f)⁻ = n • f⁻

Tactic:
ext x
-- 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
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h :
  max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)
⊢ Eq.{u_2 + 1} (α := Y) (((n • f)⁻ : (a : X) → Y) x : Y) ((n • f⁻ : (a : X) → Y) x : Y)

Tactic:
simp only [negPart, max_apply, coe_neg, coe_nsmul, Pi.neg_apply, Pi.smul_apply, coe_zero,
    Pi.zero_apply]

Premises used: Pi.zero_apply, Function.locallyFinsuppWithin.coe_nsmul, Function.locallyFinsuppWithin.coe_zero, Pi.neg_apply, Function.locallyFinsuppWithin.coe_neg, NegPart.negPart, Function.locallyFinsuppWithin.max_apply, Pi.smul_apply
-- 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
n : ℕ
f : locallyFinsuppWithin U Y
x : X
pos :
  ∀ (h : LT.lt.{u_2} (α := Y) (-(f : (a : X) → Y) x : Y) (0 : Y)),
    max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 =
      HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)
neg :
  ∀ (h : ¬LT.lt.{u_2} (α := Y) (-(f : (a : X) → Y) x : Y) (0 : Y)),
    max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 =
      HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)
⊢ max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)

Tactic:
by_cases h : -f x < 0

Premises used: DFunLike.coe
-- 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
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : LT.lt.{u_2} (α := Y) (-(f : (a : X) → Y) x : Y) (0 : Y)
⊢ max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)

Tactic:
simpa [max_eq_right_of_lt h] using nsmul_le_nsmul_right h.le n

Premises used: max_eq_right_of_lt, nsmul_le_nsmul_right, LT.lt.le
-- 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
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : ¬LT.lt.{u_2} (α := Y) (-(f : (a : X) → Y) x : Y) (0 : Y)
⊢ max (-HSMul.hSMul (β := Y) n ((f : (a : X) → Y) x : Y)) 0 = HSMul.hSMul (β := Y) n (max (-(f : (a : X) → Y) x) 0 : Y)

Tactic:
simpa [not_lt.1 h] using nsmul_nonneg (not_lt.1 h) n

Premises used: nsmul_nonneg, not_lt, Iff.mp
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
⊢ ∃ (z : X), Ne (α := ℤ) ((D : (a : X) → ℤ) z : ℤ) (0 : ℤ)

Tactic:
simpa [D.ext_iff] using (ne_of_lt h).symm

Premises used: Function.locallyFinsuppWithin.ext_iff, Ne.symm, ne_of_lt
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
obtain : ∀ (z : X) (hz : Ne (α := ℤ) ((D : (a : X) → ℤ) z : ℤ) (0 : ℤ)), ∃ (e : X), single e 1 ≤ D
⊢ ∃ (e : X), single e 1 ≤ D

Tactic:
obtain ⟨z, hz⟩ : ∃ z, D z ≠ 0 := by simpa [D.ext_iff] using (ne_of_lt h).symm
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
z : X
hz : Ne (α := ℤ) ((D : (a : X) → ℤ) z : ℤ) (0 : ℤ)
⊢ ∃ (e : X), single e 1 ≤ D

Tactic:
⟨z, fun e ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
z : X
hz : Ne (α := ℤ) ((D : (a : X) → ℤ) z : ℤ) (0 : ℤ)
refine : ∀ (e : X), LE.le (α := (fun (a : X) ↦ ℤ) e) ((single z 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)
⊢ ∃ (e : X), single e 1 ≤ D

Tactic:
refine ⟨z, fun e ↦ ?_⟩
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
z : X
hz : Ne (α := ℤ) ((D : (a : X) → ℤ) z : ℤ) (0 : ℤ)
e : X
inl :
  ∀ (hz : Ne (α := ℤ) ((D : (a : X) → ℤ) e : ℤ) (0 : ℤ)),
    LE.le (α := (fun (a : X) ↦ ℤ) e) ((single e 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)
inr : ∀ (he : e ≠ z), LE.le (α := (fun (a : X) ↦ ℤ) e) ((single z 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)
⊢ LE.le (α := (fun (a : X) ↦ ℤ) e) ((single z 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)

Tactic:
obtain (rfl | he) := eq_or_ne e z

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
e : X
hz : Ne (α := ℤ) ((D : (a : X) → ℤ) e : ℤ) (0 : ℤ)
⊢ LE.le (α := (fun (a : X) ↦ ℤ) e) ((single e 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)

Tactic:
simpa [single_apply] using Int.lt_iff_le_and_ne.mpr ⟨h.le e, hz.symm⟩

Premises used: Iff.mpr, LT.lt.le, Function.locallyFinsuppWithin.single_apply, Ne.symm, Int.lt_iff_le_and_ne, And.intro
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
z : X
hz : Ne (α := ℤ) ((D : (a : X) → ℤ) z : ℤ) (0 : ℤ)
e : X
he : e ≠ z
⊢ LE.le (α := (fun (a : X) ↦ ℤ) e) ((single z 1 : (a : X) → ℤ) e : ℤ) ((D : (a : X) → ℤ) e : ℤ)

Tactic:
simpa [he, single_apply] using h.le e

Premises used: LT.lt.le, Function.locallyFinsuppWithin.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
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ X → Y

Tactic:
exact fun z ↦ if hz : z ∈ V then D z else 0

Premises used: Membership.mem, dite, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ X → Y

Tactic:
classical
    exact fun z ↦ if hz : z ∈ V then D z else 0
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
hx :
  Membership.mem (γ := Set X)
    (Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0) x
⊢ x ∈ V ∧ ¬Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)

Tactic:
simp_rw [dite_eq_ite, mem_support, ne_eq, ite_eq_right_iff, Classical.not_imp] at hx

Premises used: ne_eq, ite_eq_right_iff, Classical.not_imp, Function.mem_support, dite_eq_ite
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
hx : x ∈ V ∧ ¬Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)
⊢ x ∈ V

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
hx : x ∈ V ∧ ¬Eq.{u_2 + 1} (α := Y) ((D : (a : X) → Y) x : Y) (0 : Y)
⊢ x ∈ V

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
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) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0).Finite
⊢ ∃ t ∈ 𝓝 z,
    (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0).Finite

Tactic:
obtain ⟨t, ht⟩ := D.supportLocallyFiniteWithinDomain z (h 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 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support (U := U)).Finite
right : (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0).Finite
⊢ ∃ t ∈ 𝓝 z,
    (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0).Finite

Tactic:
use t, ht.1

Premises used: And.left
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support (U := U)).Finite
right :
  (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0) ⊆
    t ∩ D.support (U := U)
⊢ (t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0).Finite

Tactic:
apply Set.Finite.subset (s := t ∩ D.support) ht.2

Premises used: 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 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support (U := U)).Finite
a : X
right :
  (a ∈ t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0) →
    a ∈ t ∩ D.support (U := U)
⊢ (a ∈ t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0) →
    a ∈ t ∩ D.support (U := U)

Tactic:
_
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
hz : z ∈ V
t : Set X
ht : t ∈ 𝓝 z ∧ (t ∩ D.support (U := U)).Finite
a : X
h_1 : a ∈ t ∩ Function.support.{u_1, u_2} (M := Y) fun (z : X) ↦ if hz : z ∈ V then (D : (a : X) → Y) z else 0
⊢ a ∈ t ∩ 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 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
z : X
⊢ Eq.{u_2 + 1} (α := Y) ((D.restrict (U := U) (V := V) h : (a : X) → Y) z : Y)
    (if z ∈ V then (D : (a : X) → Y) z else 0 : Y)

Tactic:
rfl

Premises used: dite, rfl, ite
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
_ : x ∈ V → Eq.{u_2 + 1} (α := Y) ((D.restrict (U := U) (V := V) h : (a : X) → Y) x : Y) ((D : (a : X) → Y) x : Y)
⊢ x ∈ V → Eq.{u_2 + 1} (α := Y) ((D.restrict (U := U) (V := V) h : (a : X) → Y) x : Y) ((D : (a : X) → Y) x : Y)

Tactic:
_
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
h_1 : x ∈ V
⊢ Eq.{u_2 + 1} (α := Y) ((D.restrict (U := U) (V := V) h : (a : X) → Y) x : Y) ((D : (a : X) → Y) x : Y)

Tactic:
simp_all [restrict_apply]

Premises used: Function.locallyFinsuppWithin.restrict_apply
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
x : X
hx : x ∈ Vᶜ
⊢ Eq.{u_2 + 1} (α := Y) ((D.restrict (U := U) (V := V) h : (a : X) → Y) x : Y) (0 x : Y)

Tactic:
simp_all
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
U V : Set X
hV : V ⊆ U
h : ∀ (a : X), Eq.{u_2 + 1} (α := Y) ((restrict (U := U) (V := V) 0 hV : (a : X) → Y) a : Y) ((0 : (a : X) → Y) a : Y)
⊢ Eq (α := locallyFinsuppWithin V Y) (restrict (U := U) (V := V) 0 hV) 0

Tactic:
ext
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
U V : Set X
hV : V ⊆ U
a : X
h : Eq.{u_2 + 1} (α := Y) (if a ∈ V then (0 : (a : X) → Y) a else 0 : Y) ((0 : (a : X) → Y) a : Y)
⊢ Eq.{u_2 + 1} (α := Y) ((restrict (U := U) (V := V) 0 hV : (a : X) → Y) a : Y) ((0 : (a : X) → Y) a : Y)

Tactic:
rw [restrict_apply]

Premises used: Function.locallyFinsuppWithin.restrict_apply
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Zero Y
U V : Set X
hV : V ⊆ U
a : X
⊢ Eq.{u_2 + 1} (α := Y) (if a ∈ V then (0 : (a : X) → Y) a else 0 : Y) ((0 : (a : X) → Y) a : Y)

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
V : Set X
h : V ⊆ U
h₁ : ∀ (x : X), Eq.{u_2 + 1} (α := Y) ((restrict (U := U) (V := V) 0 h : (a : X) → Y) x : Y) ((0 : (a : X) → Y) x : Y)
⊢ Eq (α := locallyFinsuppWithin V Y) (restrict (U := U) (V := V) 0 h) 0

Tactic:
ext x
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
V : Set X
h : V ⊆ U
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((restrict (U := U) (V := V) 0 h : (a : X) → Y) x : Y) ((0 : (a : X) → Y) x : Y)

Tactic:
simp [restrict_apply]

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

Tactic:
ext x
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
pos :
  ∀ (hx : x ∈ V),
    Eq.{u_2 + 1} (α := Y) (((D₁ + D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
      ((D₁.restrict (U := U) (V := V) h + D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
neg :
  ∀ (hx : x ∉ V),
    Eq.{u_2 + 1} (α := Y) (((D₁ + D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
      ((D₁.restrict (U := U) (V := V) h + D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
⊢ Eq.{u_2 + 1} (α := Y) (((D₁ + D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h + D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)

Tactic:
by_cases hx : x ∈ V
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
hx : x ∈ V
⊢ Eq.{u_2 + 1} (α := Y) (((D₁ + D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h + D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)

Tactic:
simp [restrict_apply, hx]

Premises used: Function.locallyFinsuppWithin.restrict_apply