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

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

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a✝ : α
⊢ (embDomain Embedding.some f) (Option.some a✝) = f a✝
Module: Mathlib.Algebra.Order.Group.Indicator

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

Tactic:
]

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ i, s i
⊢ f x = ⨆ i, (s i).mulIndicator f x
Module: Mathlib.Algebra.Order.Group.Indicator

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

Tactic:
]

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ i, x ∈ s i
⊢ f x = ⨆ i, (s i).mulIndicator f x
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 α
⊢ a.elim y ⇑f = a.elim y ⇑f

Tactic:
]

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

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

Tactic:
]

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋃ i, s i
⊢ 1 = ⨆ i, (s i).mulIndicator f x
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case none
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : Option α →₀ M
⊢ f none = f none

Tactic:
]

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

Goal state before:
pp: case neg
ι : 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 : α
hx : x ∉ ⋂ i, s i
⊢ 1 = ⨅ i, (s i).mulIndicator f x

Tactic:
]

Goal state after:
case neg
ι : 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 : α
hx : x ∉ ⋂ i, s i
⊢ 1 = ⨅ i, (s i).mulIndicator f x
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
⊢ 0 none = 0 none

Tactic:
]

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 : α
⊢ 0 (Option.some a) = 0 (Option.some a)

Tactic:
]

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

Goal state before:
pp: case refine_1
α : 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) ≤ (s i).mulIndicator (f i)

pp: case hf
α : 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 : ι
⊢ 1 ≤ f i

Tactic:
]

Goal state after:
case hf
α : 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 : ι
⊢ 1 ≤ f i
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ 0 = 0

Tactic:
]

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
⊢ 1 = 1

Tactic:
]

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
⊢ (if a ∈ f.support then b a (f a) else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
]

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

Goal state before:
pp: case pos
α : 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 : ι
hi : a ∈ s i
⊢ ⨆ i, f i a ≤ ⨆ i, (s i).mulIndicator (f i) a

Tactic:
]

Goal state after:
case pos
α : 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 : ι
hi : a ∈ s i
⊢ ⨆ i, f i a ≤ ⨆ i, (s i).mulIndicator (f i) a
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case pos
α : 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 : ι
hi : a ∈ s i
j k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ f k a = f k a

Tactic:
]

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) * (f.support.erase y).prod ?m.68 = g y (f y) * ∏ x ∈ f.support.erase y, g x (f x)

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
⊢ ∀ x ∈ f.support.erase y, g x ((erase y f) x) = ?m.68 x

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
⊢ α → N

Tactic:
]

Goal state after:
α : 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
⊢ ∀ x ∈ f.support.erase y, g x ((erase y f) x) = g x (f x)
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case neg
α : 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, (s i).mulIndicator (f i)) a

Tactic:
]

Goal state after:
case neg
α : 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, (s i).mulIndicator (f i)) a
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
h : α
hx : h ∈ f.support.erase y
⊢ g h (f h) = g h (f h)

Tactic:
]

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

Goal state before:
pp: case neg
α : 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
hyf : y ∉ f.support
⊢ f.prod g = f.prod g

Tactic:
]

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

Goal state before:
pp: case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
h✝ : ¬x✝ ∈ s
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : ¬i ∈ s
⊢ 0 = 0

Tactic:
]

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 f i * a = s.indicator f i * a

Tactic:
]

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 : ι
⊢ a * s.indicator f i = a * s.indicator f i

Tactic:
]

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.indicator (t.indicator fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i

Tactic:
]

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ s.indicator (t.indicator fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i
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
⊢ ∏ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = ∏ x ∈ f1.support ∪ f2.support, g2 x (f2 x)

Tactic:
]

Goal state after:
α : 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
⊢ ∏ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = ∏ x ∈ f1.support ∪ f2.support, g2 x (f2 x)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: 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 : f a = 0
⊢ g a 0 = 1

Tactic:
]

Goal state after:
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 : f a = 0
⊢ g a 0 = 1
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 + (Multiset.map (single a✝) s).sum = single a✝ a + (Multiset.map (single a✝) s).sum

Tactic:
]

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 : α
⊢ (Multiset.map (single a ∘ fun b ↦ f b) s.val).sum = ∑ b ∈ s, single a (f b)

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ (Multiset.map (single a ∘ fun b ↦ f b) s.val).sum = ∑ b ∈ s, single a (f b)
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.sup fun x ↦ (f x).support

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (s.sum f).support ⊆ s.sup fun x ↦ (f x).support
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case cons
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
ih : (s✝.sum f).support ⊆ s✝.sup fun x ↦ (f x).support
⊢ (f a✝ + ∑ x ∈ s✝, f x).support ⊆ (f a✝).support ⊔ s✝.sup fun x ↦ (f x).support

Tactic:
]

Goal state after:
case cons
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
ih : (s✝.sum f).support ⊆ s✝.sup fun x ↦ (f x).support
⊢ (f a✝ + ∑ x ∈ s✝, f x).support ⊆ (f a✝).support ⊔ s✝.sup fun x ↦ (f x).support
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

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

Tactic:
]

Goal state after:
α : Type u_1
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
h1 : ¬(d a = 0 ∧ ((erase a d).sum fun x n ↦ n) = 1) → d a = 1 ∧ ((erase a d).sum fun x n ↦ n) = 0
ha : d a ≠ 0 a
⊢ d a = 1 ∧ ∀ (i : α), i ≠ a → d i = 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

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

Tactic:
]

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
⊢ support (-f) = support f

Tactic:
support_neg

Goal state after:
ι : Type u_1
R : Type u_5
inst✝¹ : One R
inst✝ : AddGroup R
f : ι → R
⊢ support f = support f
Module: Mathlib.Algebra.GroupWithZero.Indicator

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

Tactic:
]

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

Goal state before:
pp: case refine_2
α : Type u_1
a : α
⊢ 1 = 1

pp: α : Type u_1
a : α
⊢ ∀ (b : α), (single a 1) b ≠ 0 → b ≠ a → (single a 1) b = 0

Tactic:
]

Goal state after:
α : Type u_1
a : α
⊢ ∀ (b : α), (single a 1) b ≠ 0 → b ≠ a → (single a 1) b = 0
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:
]

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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case add
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
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₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ b none (f₁ none) * b none (f₂ none) *
      ((f₁.some.prod fun a ↦ b (Option.some a)) * f₂.some.prod fun a ↦ b (Option.some a)) =
    b none (f₁ none) * b none (f₂ none) *
      ((f₁.some.prod fun a ↦ b (Option.some a)) * f₂.some.prod fun a ↦ b (Option.some a))

Tactic:
]

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 ∈ f.support ∪ g.support, h x ((f + g) x) = ∏ x ∈ f.support ∪ g.support, h x (f x) * h x (g x)

Tactic:
]

Goal state after:
α : 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 ∈ f.support ∪ g.support, h x ((f + g) x) = ∏ x ∈ f.support ∪ g.support, h x (f x) * h x (g x)
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case neg
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 : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ (↑n)⁻¹ • f (↑n • x) = 0

Tactic:
]

Goal state after:
case neg
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 : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ (↑n)⁻¹ • f (↑n • x) = 0
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case pos
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 : ℕ
hR : ¬↑n = 0
hS : ↑n = 0
x : M
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
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
⊢ (↑n)⁻¹ • f x = (↑n)⁻¹ • f x

Tactic:
]

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

Goal state before:
pp: case inl
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₂
x : M
n : ℕ
⊢ (↑n)⁻¹ • f x = (↑n)⁻¹ • f x

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
⊢ ∑ i, f i = ∑ a, f a

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
P : Type u_11
inst✝² : AddZeroClass M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
⊢ g.comp (f a) = g.comp (f a)

Tactic:
]

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✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ x ∈ v.support, g (f x) ((embDomain f v) (f x)) = ∏ a ∈ v.support, g (f a) (v a)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ x ∈ v.support, g (f x) ((embDomain f v) (f x)) = ∏ a ∈ v.support, g (f a) (v a)
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
M' : Type u_3
inst✝ : One M'
f : α → M
g : α → M'
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ (mulSupport f ∪ mulSupport g).Finite

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : One M
M' : Type u_3
inst✝ : One M'
f : α → M
g : α → M'
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ (mulSupport f ∪ mulSupport g).Finite
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
s✝ : Finset ι
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₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
⊢ (g a).prod h * (∑ i ∈ s, g i).prod h = (g a).prod h * (∑ x ∈ s, g x).prod h

Tactic:
]

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✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = (Multiset.map (fun g ↦ g.sum h) s).sum
⊢ a.sum h + (Multiset.map (fun g ↦ g.sum h) s).sum = a.sum h + (Multiset.map (fun g ↦ g.sum h) s).sum

Tactic:
]

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

Goal state before:
pp: case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support
⊢ ((g i).support ∪ s.biUnion fun i ↦ (g i).support) = (g i).support ∪ s.biUnion fun i ↦ (g i).support

pp: case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support
⊢ Disjoint (g i).support (∑ i ∈ s, g i).support

Tactic:
]

Goal state after:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support
⊢ Disjoint (g i).support (∑ i ∈ s, g i).support
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support
⊢ ∀ i_1 ∈ s, Disjoint (g i).support (g i_1).support

Tactic:
]

Goal state after:
case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s✝ : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs : (∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support
⊢ ∀ i_1 ∈ s, Disjoint (g i).support (g i_1).support
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inr.succ
R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
h✝ : Nontrivial R
n : ℕ
ih : abv ↑n ≤ ↑n
⊢ ↑n + 1 ≤ ↑n + 1

Tactic:
]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv a * abv a = abv a * abv a

Tactic:
]

Goal state after: