mathlib-initiative/mathlib-tactics huggingface dataset:
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 + g i * (∑ j ∈ s, r j) ^ 2) =
    (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * ((∑ i ∈ s, f i) * ∑ i ∈ s, g i)

Tactic:
by

Goal state after:
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✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ ∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
x✝ : ∃ a ∈ x.support, f a = t
i : α
i_in : i ∈ x.support
hi : f i = t
⊢ ¬x i = 0 ∧ f i = f i ∧ ¬x i = 0

Tactic:
simp [mem_support_iff.mp i_in]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
x✝ : ∃ a ∈ x.support, f a = t
i : α
i_in : i ∈ x.support
hi : f i = t
⊢ ¬x i = 0 ∧ f i = f i ∧ ¬x i = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
⊢ (mapDomain f x).support = image f x.support

Tactic:
by

Goal state after:
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
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
a : α
⊢ (mapDomain f x) (f a) = ∑ i ∈ x.support with f i = f a, x i

Tactic:
by

Goal state after:
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
h : x = 0
⊢ mapDomain f x = 0

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ ∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
⊢ (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : LinearOrder M
f g : ι → M
s : Finset ι
inst✝ : MulLeftMono M
Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i
⊢ ∃ i ∈ s, f i < g i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : CommMonoid N
inst✝¹ : MulDistribMulAction M N
ι : Sort u_4
inst✝ : Finite ι
f : ι → N
r : M
val✝ : Fintype (PLift ι)
⊢ Function.mulSupport (?m.44 ∘ PLift.down) ⊆ ↑Finset.univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : CommMonoid N
inst✝¹ : MulDistribMulAction M N
ι : Sort u_4
inst✝ : Finite ι
f : ι → N
r : M
⊢ r • ∏ᶠ (x : ι), f x = ∏ᶠ (x : ι), r • f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: N : Type u_2
inst✝³ : CommMonoid N
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G N
inst✝ : Fintype G
b : N
g : G
⊢ ∀ (i : G), i ∈ univ ↔ g * i ∈ univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: N : Type u_2
inst✝³ : CommMonoid N
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G N
inst✝ : Fintype G
b : N
g : G
⊢ g • ∏ h, h • b = ∏ h, h • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: N : Type u_2
inst✝³ : CommMonoid N
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G N
inst✝ : Finite G
b : N
g : G
⊢ g • ∏ᶠ (h : G), h • b = ∏ᶠ (h : G), h • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : MulOneClass N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
l : List N
m : M
⊢ m ^ l.length • l.prod = (map (fun x ↦ m • x) l).prod

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : LinearOrder M
f g : ι → M
s : Finset ι
inst✝ : IsOrderedCancelMonoid M
hs : s.Nonempty
Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : CommMonoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Multiset N
b : M
⊢ ∀ (a : List N),
    b ^ card (Quot.mk (⇑(List.isSetoid N)) a) • prod (Quot.mk (⇑(List.isSetoid N)) a) =
      (map (fun x ↦ b • x) (Quot.mk (⇑(List.isSetoid N)) a)).prod

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
⊢ Multiset.map (fun x ↦ b • f x) s.val = Multiset.map (fun x ↦ b • x) (Multiset.map f s.val)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : LinearOrder M
s : Finset ι
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h₁ : ∏ i ∈ s, f i = 1
h₂ : ∃ i ∈ s, f i ≠ 1
⊢ ∃ i ∈ s, 1 < f i

Tactic:
by

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 M
inst✝ : SMulZeroClass R M
a : R
⊢ a • 0 = 0

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_5
R : Type u_11
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
b : R
g : α →₀ M
a : α
⊢ a ∈ (b • g).support → a ∈ g.support

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
S : Type u_12
inst✝³ : Zero M
inst✝² : SMulZeroClass R M
inst✝¹ : Zero N
inst✝ : SMulZeroClass S N
f : M → N
hf : f 0 = 0
c : R
d : S
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = d • f x
⊢ mapRange f hf (c • v) = d • mapRange f hf v

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_3
R : Type u_6
inst✝² : Zero M
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R M
a b : α
f : α → M
r : R
⊢ (single a r) b • f a = (single a (r • f b)) b

Tactic:
by

Goal state after:
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✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g g' : G
f : α →₀ M
⊢ (g * g') • f = g • g' • f

Tactic:
by

Goal state after:
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✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ 1 • f = f

Tactic:
by

Goal state after:
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✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
⊢ g • 0 = 0

Tactic:
by

Goal state after:
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✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f f' : α →₀ M
⊢ g • (f + f') = g • f + g • f'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_3
G : Type u_5
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ (g • f) a = f (g⁻¹ • a)

Tactic:
by

Goal state after:
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✝³ : Nonempty α
inst✝² : Zero M
inst✝¹ : SMulZeroClass R M
inst✝ : FaithfulSMul R M
m₁✝ m₂✝ : R
h : ∀ (a : α →₀ M), m₁✝ • a = m₂✝ • a
a : α
m : M
⊢ m₁✝ • m = m₂✝ • m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_3
R : Type u_6
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
b : R
hb : b ≠ 0
g : α →₀ M
a : α
⊢ a ∈ (b • g).support ↔ a ∈ g.support

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_3
R : Type u_6
p : α → Prop
inst✝² : DecidablePred p
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
b : R
v : α →₀ M
⊢ ⇑(filter p (b • v)) = ⇑(b • filter p v)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : SemilatticeSup α
inst✝³ : OrderBot α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t✝ : Finset ι
i : ι
t : Finset ι
it : i ∉ t
h : f (t.sup s) ≤ ∑ i ∈ t, f (s i)
⊢ f (s i) + f (t.sup s) ≤ f (s i) + ∑ i ∈ t, f (s i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_6
x✝ : Semiring R
c : R
a : α
b : R
⊢ c • single a b = single a (c * b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_6
inst✝ : MulZeroOneClass R
a : α
b : R
⊢ b • single a 1 = single a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
R : Type u_6
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → β
r : R
v : β →₀ M
hfv : Set.InjOn f (f ⁻¹' ↑v.support)
hfrv : Set.InjOn f (f ⁻¹' ↑(r • v).support)
⊢ comapDomain f (r • v) hfrv = r • comapDomain f v hfv

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
⊢ b ^ #s • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : SemilatticeSup α
inst✝³ : OrderBot α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t : Finset ι
⊢ f (t.sup s) ≤ ∑ i ∈ t, f (s i)

Tactic:
by

Goal state after:
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
⊢ f = g

Tactic:
by

Goal state after:
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✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : AddMonoid N
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction R N
a : α
k : R
m : M
⊢ (↑(singleAddHom a)).toFun (k • m) = (MonoidHom.id R) k • (↑(singleAddHom a)).toFun m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
f : Set α → β
zero : f ∅ = 0
ih : ∀ {s t : Set α}, f (s ∪ t) ≤ f s + f t
s : ι → Set α
t : Finset ι
⊢ ∀ {s t : Set α}, f (s ⊔ t) ≤ f s + f t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: 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
s : Finset ι
b : ι → M
f : ι → N
⊢ ∏ i ∈ s, b i • f i = (∏ i ∈ s, b i) • ∏ i ∈ s, f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
x : α
hsx : x ∈ s
hfx : f x ≠ 0
⊢ ∀ y ∈ s \ {x}, f y = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
s : Finset α
f : α → ℕ
⊢ ∑ x ∈ s, f x ≤ 1 ↔ ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
f : ι → M
hf : 1 ≤ f
⊢ (∀ i ∈ Finset.univ, f i = 1) ↔ f = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
f : ι → M
hf : f ≤ 1
⊢ (∀ i ∈ Finset.univ, f i = 1) ↔ f = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf : 1 < f
⊢ ∃ i ∈ Finset.univ, 1 < f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf : f < 1
⊢ ∃ i ∈ Finset.univ, f i < 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf : 1 ≤ f
⊢ 1 < ∏ i, f i ↔ 1 < f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf : f ≤ 1
⊢ ∏ i, f i < 1 ↔ f < 1

Tactic:
by

Goal state after:
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

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k ↦ powersetCard k x) = x.powerset

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ ∀ x ∈ m.toFinset, 1 ≤ count x m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ m.card ≤ m.toFinset.card + 1 ↔ ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2

Tactic:
by

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 : α
⊢ lapply a ∘ₗ lsingle a = LinearMap.id

Tactic:
by

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 a' : α
h : a ≠ a'
⊢ lapply a ∘ₗ lsingle a' = 0

Tactic:
by

Goal state after:
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
f : α ≃ α'
x✝ : α →₀ M
⊢ mapDomain (⇑f.symm) ((lmapDomain M R f.toFun).toFun x✝) = x✝

Tactic:
by

Goal state after:
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
f : α ≃ α'
x✝ : α' →₀ M
⊢ (lmapDomain M R f.toFun).toFun (mapDomain (⇑f.symm) x✝) = x✝

Tactic:
by

Goal state after:
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
⊢ comapDomain f (x + y) ⋯ = comapDomain f x ⋯ + comapDomain f y ⋯

Tactic:
by

Goal state after:
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
⊢ comapDomain f (c • x) ⋯ = (RingHom.id R) c • comapDomain f x ⋯

Tactic:
by

Goal state after:
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
⊢ curryAddEquiv.toFun (c • f) = (RingHom.id R) c • curryAddEquiv.toFun f

Tactic:
by

Goal state after:
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
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝³ : Semiring R
inst✝² : Subsingleton R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι →₀ R
⊢ (fun x ↦ 0) ((fun x ↦ 0) f) = f

Tactic:
by

Goal state after:
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
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
⊢ (mapRange.addMonoidHom ↑f) (g • 0) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) 0

Tactic:
by

Goal state after:
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
f : End (End R M) M
g : End R (ι →₀ M)
x x✝¹ x✝ : ι →₀ M
h : (mapRange.addMonoidHom ↑f) (g • x✝¹) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹
h' : (mapRange.addMonoidHom ↑f) (g • x✝) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝
⊢ (mapRange.addMonoidHom ↑f) (g • (x✝¹ + x✝)) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (x✝¹ + x✝)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
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
s : Set α
p q : α →₀ M
hp : p ∈ {p | ↑p.support ⊆ s}
hq : q ∈ {p | ↑p.support ⊆ s}
⊢ p + q ∈ {p | ↑p.support ⊆ s}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
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
s : Set α
⊢ 0 ∈ {p | ↑p.support ⊆ s}

Tactic:
by

Goal state after: