mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: case ha
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ 0 ≤ f a

pp: case hbc
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f s.prod ≤ (map f s).prod

Tactic:
;

Goal state after:
case ha
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ 0 ≤ f a

case hbc
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f s.prod ≤ (map f s).prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_12
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
x : β
⊢ (equivMapDomain f l) x = (mapDomain (⇑f) l) x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_12
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
x : β
⊢ (equivMapDomain f l) x = (mapDomain (⇑f) l) x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
l : α →₀ M
a✝ : α
⊢ (comapDomain (⇑f) (embDomain f l) ⋯) a✝ = l a✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
l : α →₀ M
a✝ : α
⊢ (comapDomain (⇑f) (embDomain f l) ⋯) a✝ = l a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1.e_v
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
⊢ (comapDomain.addMonoidHom ⋯) l = comapDomain (fun x ↦ x + 1) (erase 0 l) ⋯

Tactic:
;

Goal state after:
case refine_1.e_v
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
⊢ (comapDomain.addMonoidHom ⋯) l = comapDomain (fun x ↦ x + 1) (erase 0 l) ⋯
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1.e_v
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
a✝ : ℕ
⊢ ((comapDomain.addMonoidHom ⋯) l) a✝ = (comapDomain (fun x ↦ x + 1) (erase 0 l) ⋯) a✝

Tactic:
;

Goal state after:
case refine_1.e_v
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
a✝ : ℕ
⊢ ((comapDomain.addMonoidHom ⋯) l) a✝ = (comapDomain (fun x ↦ x + 1) (erase 0 l) ⋯) a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : α →₀ M
a✝ : α
⊢ (comapDomain f (mapDomain f l) ⋯) a✝ = l a✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : α →₀ M
a✝ : α
⊢ (comapDomain f (mapDomain f l) ⋯) a✝ = l a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (filter (fun x ↦ a = x) f) a✝ = (single a (f a)) a✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (filter (fun x ↦ a = x) f) a✝ = (single a (f a)) a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (if a = a✝ then f a✝ else 0) = if a = a✝ then f a else 0

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (if a = a✝ then f a✝ else 0) = if a = a✝ then f a else 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case h₂
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝¹ : α
a✝ : a = a✝¹
⊢ a✝¹ = a

Tactic:
;

Goal state after:
case h₂
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝¹ : α
a✝ : a = a✝¹
⊢ a✝¹ = a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ (filter p f + filter (fun x ↦ ¬p x) f) a✝ = f a✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ (filter p f + filter (fun x ↦ ¬p x) f) a✝ = f a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ ((if p a✝ then f a✝ else 0) + if p a✝ then 0 else f a✝) = f a✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ ((if p a✝ then f a✝ else 0) + if p a✝ then 0 else f a✝) = f a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
p✝ p : α → Prop
f : α →₀ M
a : Subtype p
⊢ f ↑a ≠ 0 ↔ (⇑f ∘ Subtype.val) a ≠ 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
p✝ p : α → Prop
f : α →₀ M
a : Subtype p
⊢ f ↑a ≠ 0 ↔ (⇑f ∘ Subtype.val) a ≠ 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ f i * f j = ∏ k ∈ cons i {j} ⋯, f k

Tactic:
prod_cons,

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ f i * f j = f i * ∏ x ∈ {j}, f x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ { support := image Prod.fst f.support,
        toFun := fun a ↦
          { support := filterMap (fun x ↦ if x.1 = a then some x.2 else none) f.support ⋯, toFun := fun b ↦ f (a, b),
            mem_support_toFun := ⋯ },
        mem_support_toFun := ⋯ }.support =
    image Prod.fst f.support

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ { support := image Prod.fst f.support,
        toFun := fun a ↦
          { support := filterMap (fun x ↦ if x.1 = a then some x.2 else none) f.support ⋯, toFun := fun b ↦ f (a, b),
            mem_support_toFun := ⋯ },
        mem_support_toFun := ⋯ }.support =
    image Prod.fst f.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : AddZeroClass M
x✝¹ x✝ : α × β →₀ M
a✝¹ : α
a✝ : β
⊢ ((curryEquiv.toFun (x✝¹ + x✝)) a✝¹) a✝ = ((curryEquiv.toFun x✝¹ + curryEquiv.toFun x✝) a✝¹) a✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : AddZeroClass M
x✝¹ x✝ : α × β →₀ M
a✝¹ : α
a✝ : β
⊢ ((curryEquiv.toFun (x✝¹ + x✝)) a✝¹) a✝ = ((curryEquiv.toFun x✝¹ + curryEquiv.toFun x✝) a✝¹) a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
f : α →₀ γ
g : β →₀ γ
a✝ : α
⊢ (comapDomain Sum.inl (f.sumElim g) ⋯) a✝ = f a✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
f : α →₀ γ
g : β →₀ γ
a✝ : α
⊢ (comapDomain Sum.inl (f.sumElim g) ⋯) a✝ = f a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
f : α →₀ γ
g : β →₀ γ
a✝ : β
⊢ (comapDomain Sum.inr (f.sumElim g) ⋯) a✝ = g a✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
f : α →₀ γ
g : β →₀ γ
a✝ : β
⊢ (comapDomain Sum.inr (f.sumElim g) ⋯) a✝ = g a✝
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 =
    2 * ((∑ i ∈ s, r i) * ((∑ i ∈ s, g i) * ∑ i ∈ s, r i))

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 =
    2 * ((∑ i ∈ s, r i) * ((∑ i ∈ s, g i) * ∑ i ∈ s, r i))
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ ∀ i ∈ s, f i = 1 → f i ≤ 1

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ ∀ i ∈ s, f i = 1 → f i ≤ 1
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
s : Set α
M : Type u_12
inst✝¹ : AddCommMonoid M
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ↑s →₀ M
⊢ f.extendDomain = f.extendDomain

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
M : Type u_12
inst✝¹ : AddCommMonoid M
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ↑s →₀ M
⊢ f.extendDomain = f.extendDomain
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case e'_1.e'_4
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
x✝ : α →₀ M
a✝ : β
⊢ (embDomain f x✝) a✝ = (mapDomain (⇑f) x✝) a✝

Tactic:
;

Goal state after:
case e'_1.e'_4
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
x✝ : α →₀ M
a✝ : β
⊢ (embDomain f x✝) a✝ = (mapDomain (⇑f) x✝) a✝
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, f i) * (∑ j ∈ s, g j) ^ 2 + (∑ j ∈ s, g j) * (∑ j ∈ s, r j) ^ 2 =
    (∑ j ∈ s, g j) * (∑ j ∈ s, r j) ^ 2 + (∑ j ∈ s, g j) * ((∑ i ∈ s, f i) * ∑ j ∈ s, g j)

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, f i) * (∑ j ∈ s, g j) ^ 2 + (∑ j ∈ s, g j) * (∑ j ∈ s, r j) ^ 2 =
    (∑ j ∈ s, g j) * (∑ j ∈ s, r j) ^ 2 + (∑ j ∈ s, g j) * ((∑ i ∈ s, f i) * ∑ j ∈ s, g j)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
i : α
h : ∀ (i_1 : α), ¬x i_1 = 0 → f i_1 = f i → x i_1 = 0
⊢ x i = 0 i

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
i : α
h : ∀ (i_1 : α), ¬x i_1 = 0 → f i_1 = f i → x i_1 = 0
⊢ x i = 0 i
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
⊢ mapDomain f x = 0 ↔ x = 0

Tactic:
refine ⟨fun h ↦ Finsupp.ext (fun i ↦ ?_), fun h ↦ by rw [h, mapDomain_zero]⟩
  replace h := Finsupp.ext_iff.mp h (f i)
  simp [mapDomain_apply_eq_sum] at h; grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α →₀ M
i : α
⊢ (0 • f) i = 0 i

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α →₀ M
i : α
⊢ (0 • f) i = 0 i
Module: Mathlib.Data.Finsupp.SMul

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_7
inst✝ : Module.IsTorsionFree R M
r : R
hr : IsRegular r
f g : ι →₀ M
hfg : (fun x ↦ r • x) f = (fun x ↦ r • x) g
i : ι
⊢ f i = g i

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_7
inst✝ : Module.IsTorsionFree R M
r : R
hr : IsRegular r
f g : ι →₀ M
hfg : (fun x ↦ r • x) f = (fun x ↦ r • x) g
i : ι
⊢ f i = g i
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: case cons
M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : CommMonoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
b : ι → M
f : ι → N
a✝ : ι
s✝ : Finset ι
hj : a✝ ∉ s✝
ih : ∏ i ∈ s✝, b i • f i = (∏ i ∈ s✝, b i) • ∏ i ∈ s✝, f i
⊢ ∏ i ∈ cons a✝ s✝ hj, b i • f i = (∏ i ∈ cons a✝ s✝ hj, b i) • ∏ i ∈ cons a✝ s✝ hj, f i

Tactic:
prod_cons,

Goal state after:
case cons
M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : CommMonoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
b : ι → M
f : ι → N
a✝ : ι
s✝ : Finset ι
hj : a✝ ∉ s✝
ih : ∏ i ∈ s✝, b i • f i = (∏ i ∈ s✝, b i) • ∏ i ∈ s✝, f i
⊢ b a✝ • f a✝ * ∏ x ∈ s✝, b x • f x = (∏ i ∈ cons a✝ s✝ hj, b i) • ∏ i ∈ cons a✝ s✝ hj, f i
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
i : Finset β
f : β → Multiset α
⊢ i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)

Tactic:
by
  induction i using Finset.cons_induction_on with
  | empty =>
    simp only [Finset.notMem_empty, IsEmpty.forall_iff, imp_true_iff, Finset.sum_empty,
      Finset.sup_empty, bot_eq_zero]
  | cons z i hz hr =>
    simp_rw [Finset.sum_cons hz, Finset.sup_cons, Finset.mem_cons, Multiset.sup_eq_union,
      forall_eq_or_imp, Ne, not_true_eq_false, IsEmpty.forall_iff, true_and,
      imp_and, forall_and, ← hr, @eq_comm _ z]
    have := fun x (H : x ∈ i) => ne_of_mem_of_not_mem H hz
    simp +contextual only [this, not_false_iff, true_imp_iff]
    simp_rw [← disjoint_finsetSum_left, ← disjoint_finsetSum_right, disjoint_comm, ← and_assoc,
      and_self_iff]
    exact add_eq_union_left_of_le (Finset.sup_le fun x hx => le_sum_of_mem (mem_map_of_mem f hx))

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : α
x✝ : M
⊢ (lapply a ∘ₗ lsingle a) x✝ = LinearMap.id x✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : α
x✝ : M
⊢ (lapply a ∘ₗ lsingle a) x✝ = LinearMap.id x✝
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a a' : α
h : a ≠ a'
x✝ : M
⊢ (lapply a ∘ₗ lsingle a') x✝ = 0 x✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a a' : α
h : a ≠ a'
x✝ : M
⊢ (lapply a ∘ₗ lsingle a') x✝ = 0 x✝
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
x y : β →₀ M
a✝ : α
⊢ (comapDomain f (x + y) ⋯) a✝ = (comapDomain f x ⋯ + comapDomain f y ⋯) a✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
x y : β →₀ M
a✝ : α
⊢ (comapDomain f (x + y) ⋯) a✝ = (comapDomain f x ⋯ + comapDomain f y ⋯) a✝
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
c : R
x : β →₀ M
a✝ : α
⊢ (comapDomain f (c • x) ⋯) a✝ = ((RingHom.id R) c • comapDomain f x ⋯) a✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
c : R
x : β →₀ M
a✝ : α
⊢ (comapDomain f (c • x) ⋯) a✝ = ((RingHom.id R) c • comapDomain f x ⋯) a✝
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: α✝ : Type u_1
M✝ : Type u_2
N : Type u_3
P : Type u_4
R✝ : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹⁴ : Semiring R✝
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R₂ N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R₃ P
σ₁₂ : R✝ →+* R₂
σ₂₁ : R₂ →+* R✝
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R✝ →+* R₃
σ₃₁ : R₃ →+* R✝
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
α : Type u_9
β : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
f : α × β →₀ M
a✝¹ : α
a✝ : β
⊢ ((curryAddEquiv.toFun (c • f)) a✝¹) a✝ = (((RingHom.id R) c • curryAddEquiv.toFun f) a✝¹) a✝

Tactic:
;

Goal state after:
α✝ : Type u_1
M✝ : Type u_2
N : Type u_3
P : Type u_4
R✝ : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹⁴ : Semiring R✝
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R₂ N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R₃ P
σ₁₂ : R✝ →+* R₂
σ₂₁ : R₂ →+* R✝
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R✝ →+* R₃
σ₃₁ : R₃ →+* R✝
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
α : Type u_9
β : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
f : α × β →₀ M
a✝¹ : α
a✝ : β
⊢ ((curryAddEquiv.toFun (c • f)) a✝¹) a✝ = (((RingHom.id R) c • curryAddEquiv.toFun f) a✝¹) a✝
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑1), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ = (1 x✝) a✝

Tactic:
;

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑1), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ = (1 x✝) a✝
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : End (End R M) M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑(x✝² * x✝¹)), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ =
    (({ toFun := ⇑(mapRange.addMonoidHom ↑x✝²), map_add' := ⋯, map_smul' := ⋯ } *
          { toFun := ⇑(mapRange.addMonoidHom ↑x✝¹), map_add' := ⋯, map_smul' := ⋯ })
        x✝)
      a✝

Tactic:
;

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : End (End R M) M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑(x✝² * x✝¹)), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ =
    (({ toFun := ⇑(mapRange.addMonoidHom ↑x✝²), map_add' := ⋯, map_smul' := ⋯ } *
          { toFun := ⇑(mapRange.addMonoidHom ↑x✝¹), map_add' := ⋯, map_smul' := ⋯ })
        x✝)
      a✝