mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : Option α →₀ M
⊢ (fun P ↦ (embDomain Embedding.some P.2).update none P.1) ((fun P ↦ (P none, P.some)) P) = P

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
⊢ s.mulIndicator f a ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
⊢ s.indicator f ≤ {a | 0 ≤ f a}.indicator f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : M × (α →₀ M)
⊢ (fun P ↦ (P none, P.some)) ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) P) = P

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ (optionElim y f) none = y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
x : α
⊢ (optionElim y f) (Option.some x) = f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
a : Option α
⊢ (optionElim y f) a = a.elim y ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
a : Option α
⊢ (optionElim y f) a = Option.elim' y (⇑f) a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ (optionElim y f).some = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : Option α →₀ M
⊢ optionElim (f none) f.some = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
⊢ optionElim y 0 = single none y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ 1 ≤ ⨅ i, (s i).mulIndicator f x

Tactic:
simp only [← h1, le_iInf_iff, bot_le, forall_const]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ 1 ≤ ⨅ i, (s i).mulIndicator f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
⊢ (optionElim y f) none = 0 none

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
h : y ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
⊢ (⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
⊢ (optionElim y f) (Option.some a) = 0 (Option.some a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
h : f ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
⊢ (f.prod fun x x_1 ↦ 1) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
⊢ f.prod g = ∏ x ∈ s, g x (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
a : α
b : M
h : α → M → N
h_zero : h a 0 = 1
⊢ ∏ x ∈ {a}, h x ((single a b) x) = h a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
M' : Type u_9
N : Type u_10
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : M → M'
hf : f 0 = 0
g : α →₀ M
h : α → M' → N
h0 : ∀ (a : α), h a 0 = 1
x✝¹ : α
x✝ : x✝¹ ∈ g.support
H : x✝¹ ∉ (mapRange f hf g).support
⊢ h x✝¹ ((mapRange f hf g) x✝¹) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
⊢ ∃ i, a ∈ s i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (f.prod fun x v ↦ if a = x then b x v else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (f.sum fun x v ↦ if a = x then v else 0) = f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ optionElim y f ≠ 0 ↔ f ≠ 0 ∨ y ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : Zero N
f : α →₀ N
a : α
⊢ (if a ∈ f.support then f a else 0) = f a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ optionElim y f ≠ 0 ↔ f ≠ 0 ∨ y ≠ 0

Tactic:
by
  constructor
  · intro h
    contrapose! h
    rcases h with ⟨rfl, rfl⟩
    rw [optionElim_zero, single_zero]
  · intro h
    cases h with
    | inl h => exact optionElim_ne_zero_of_right y f h
    | inr h => exact optionElim_ne_zero_of_left y f h

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (f.prod fun x v ↦ if x = a then b x v else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (f.sum fun x v ↦ if x = a then v else 0) = f a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : α → M
g : α → M → N
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
hg : ∀ (a : α), g a 0 = 1
⊢ ∀ x ∈ s, x ∉ (onFinset s f hf).support → g x ((onFinset s f hf) x) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
⊢ ⨆ i, (s i).mulIndicator (f i) = (⋃ i, s i).mulIndicator (⨆ i, f i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
⊢ (s.indicator fun i ↦ f i * g i) = fun i ↦ s.indicator f i * s.indicator g i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ s.indicator (fun j ↦ f j * g j) i = s.indicator f i * g i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ s.indicator (fun j ↦ f j * g j) i = f i * s.indicator g i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f : ι → M₀
a : M₀
i : ι
⊢ s.indicator (fun x ↦ f x * a) i = s.indicator f i * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f : ι → M₀
a : M₀
i : ι
⊢ s.indicator (fun x ↦ a * f x) i = a * s.indicator f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f1 f2 : α →₀ M
g1 g2 : α → M → N
h : ∀ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = g2 x (f2 x)
h1 : ∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1
h2 : ∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1
⊢ f1.prod g1 = f2.prod g2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
⊢ f.prod g = g a (f a)

Tactic:
refine Finset.prod_eq_single a (fun b hb₁ hb₂ => ?_) (fun h => ?_)

Goal state after:
case refine_1
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
b : α
hb₁ : b ∈ f.support
hb₂ : b ≠ a
⊢ g b (f b) = 1

case refine_2
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
h : a ∉ f.support
⊢ g a (f a) = 1
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1
h₁ : f a = 0 → g a 0 = 1
⊢ f.prod g = g a (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : Unique α
f : α →₀ M
g : α → M → N
h₁ : f default = 0 → g default 0 = 1
a : α
⊢ f a ≠ 0 → a ≠ default → g a (f a) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ (s ∩ t).indicator (fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s✝ : Multiset M
a✝ : α
a : M
s : Multiset M
ih : single a✝ s.sum = (Multiset.map (single a✝) s).sum
⊢ single a✝ (a ::ₘ s).sum = (Multiset.map (single a✝) (a ::ₘ s)).sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s t : Set ι
x✝ : ι
⊢ (s ∩ t).indicator 1 x✝ = (s.indicator 1 * t.indicator 1) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b ∈ s, f b) = ∑ b ∈ s, single a (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝² : DecidableEq β
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
⊢ (f.sum g).support ⊆ f.support.biUnion fun a ↦ (g a (f a)).support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (s.sum f).support ⊆ s.biUnion fun x ↦ (f x).support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
x✝ : d = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s : Set ι
i : ι
inst✝ : Nontrivial M₀
⊢ s.indicator 1 i = 0 ↔ ¬i ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s : Set ι
i : ι
inst✝ : Nontrivial M₀
⊢ s.indicator 1 i = 1 ↔ i ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
⊢ d a = 1 ∧ ∀ (i : α), i ≠ a → d i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
f g : ι → M₀
x : ι
hfg : x ∈ support fun x ↦ f x * g x
hf : f x = 0
⊢ (fun x ↦ f x * g x) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
f g : ι → M₀
x : ι
hfg : x ∈ support fun x ↦ f x * g x
hg : g x = 0
⊢ (fun x ↦ f x * g x) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
f g : ι → M₀
x : ι
⊢ (x ∈ support fun x ↦ f x * g x) ↔ x ∈ support f ∩ support g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
f : ι → M₀
hf : ∀ (x : ι), f x ≠ 0
g : ι → M₀
⊢ (support fun x ↦ f x * g x) = support g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
f g : ι → M₀
hg : ∀ (x : ι), g x ≠ 0
⊢ (support fun x ↦ f x * g x) = support f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MonoidWithZero M₀
inst✝ : IsReduced M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
⊢ (support fun a ↦ f a ^ n) = support f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
G₀ : Type u_3
inst✝ : GroupWithZero G₀
f g : ι → G₀
⊢ (support fun a ↦ f a / g a) = support f ∩ support g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
R : Type u_5
inst✝¹ : One R
inst✝ : AddGroup R
f : ι → R
⊢ mulSupport (1 - f) = support f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
d : α →₀ ℕ
⊢ (d.sum fun x n ↦ n) = 1 ↔ ∃ a, d = single a 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
x : M
⊢ -u • x = -(u • x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
this : ∀ (y : M), f y = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
x : α
hx : x ∈ f.support ∪ g.support
⊢ h x ((f + g) x) = h x (f x) * h x (g x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
this : ∀ (y : M), f y = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : α → M →+ N
⊢ (fun F x ↦ F.comp (singleAddHom x))
      ((fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ }) F) =
    F

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
⊢ f.prod b = b none (f none) * f.some.prod fun a ↦ b (Option.some a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
z : ℤ
x : M
⊢ f ((↑z)⁻¹ • x) = (↑z)⁻¹ • f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
a b : α →₀ M
i j : M
⊢ optionElim (i + j) (a + b) = optionElim i a + optionElim j b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : (α →₀ M) →+ N
⊢ (fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ })
      ((fun F x ↦ F.comp (singleAddHom x)) F) =
    F

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
g : α → M
x : α
hfg : x ∈ support (f • g)
hf : f x = 0
⊢ (f • g) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
g : α → M
x : α
hbf : x ∈ support (f • g)
hf : g x = 0
⊢ (f • g) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G✝ : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F G : α → M →+ N
⊢ { toFun := fun f ↦ f.sum fun x ↦ ⇑((F + G) x), map_zero' := ⋯, map_add' := ⋯ } =
    { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ } +
      { toFun := fun f ↦ f.sum fun x ↦ ⇑(G x), map_zero' := ⋯, map_add' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
⊢ s.indicator (fun a ↦ r a • f a) a = r a • s.indicator f a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
⊢ s.indicator (fun a ↦ r a • f a) a = s.indicator r a • f a

Tactic:
by

Goal state after: