mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : ι → κ
hi : ∀ a ∈ s, i a ∈ t
i_inj : Set.InjOn i ↑s
i_surj : Set.SurjOn i ↑s ↑t
h : ∀ a ∈ s, f a = g (i a)
⊢ ∀ b ∈ t, ∃ a, ∃ (_ : a ∈ s), i a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj h • P.subgroupOf H = (MulAut.conj ↑h • P).subgroupOf H

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
this : ∀ b ∈ s.erase a, Commute a b
⊢ (s.erase a).noncommProd comm' * a = s.noncommProd comm

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∏ i ∈ s, f i = ∏ i ∈ t, g i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ a • (S ⊓ T) = a • S ⊓ a • T

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ r (∏ x ∈ s, f x) (∏ x ∈ s, g x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ ↑H * {h} = ↑H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ {h} * ↑H = ↑H

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f g : ι → M
⊢ (∏ x ∈ s, if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
⊢ (∏ x ∈ s, if h : p then f h x else g h x) = if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : ι → M
⊢ (if p then ∏ x ∈ s, f x else 1) = ∏ x ∈ s, if p then f x else 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : ι → M
⊢ (if p then 1 else ∏ x ∈ s, f x) = ∏ x ∈ s, if p then 1 else f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
⊢ (s.erase a).noncommProd comm' * a = s.noncommProd comm

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ k ∈ range 0, f k = 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
l : List ι
⊢ ∑ x ∈ l.toFinset with p x, count x l = countP (fun b ↦ decide (p b)) l

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
b : β
hb : b ∈ Multiset.map f s.val
⊢ ?m.28

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
⊢ p (s.noncommProd f comm)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∏ x, f x = ∏ x ∈ m.toFinset, g x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
M : Type u_7
inst✝ : CommMonoid M
f : ι → M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
nonempty : s.Nonempty
base : ∀ x ∈ s, p (f x)
⊢ Multiset.map (fun x ↦ f x) s.val ≠ ∅

Tactic:
by

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

Goal state before:
pp: ι : Type u_7
M : Type u_8
inst✝ : CommMonoid M
s t : Finset ι
f : ι → M
h : s ⊆ t
⊢ s.val ≤ t.val

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ (Commute on g) x y

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
⊢ s₁.noncommProd f comm = s₂.noncommProd g ⋯

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).prod % n = (∏ i ∈ s, f i % n) % n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
l : List α
f : α → β
comm : (↑l.toFinset).Pairwise (Commute on f)
hl : l.Nodup
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
⊢ H.Normal

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).prod % n = (∏ i ∈ s, f i % n) % n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid M
e : ι → κ
he : Bijective e
f : ι → M
g : κ → M
h : ∀ (x : ι), f x = g (e x)
⊢ ∀ (i : ι), i ∈ univ ↔ (Equiv.ofBijective e he) i ∈ univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : (↑(insert a s)).Pairwise (Commute on f)
ha : a ∉ s
⊢ (insert a s).noncommProd f comm = f a * s.noncommProd f ⋯

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid M
e : ι → κ
he : Bijective e
f : ι → M
g : κ → M
h : ∀ (x : ι), f x = g (e x)
⊢ ∀ i ∈ univ, f i = g ((Equiv.ofBijective e he) i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : (↑(insert a s)).Pairwise (Commute on f)
ha : a ∉ s
⊢ (insert a s).noncommProd f comm = s.noncommProd f ⋯ * f a

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : Fintype ι
f : ↥univ → M
⊢ ∀ (x : Subtype (Membership.mem univ)), f x = f ⟨(Equiv.subtypeUnivEquiv ⋯) x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ (↑{a}).Pairwise (Commute on f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = ⨅ g, g • H

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝³ : Monoid β
inst✝² : Monoid γ
inst✝¹ : FunLike F β γ
inst✝ : MonoidHomClass F β γ
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
g : F
⊢ g (s.noncommProd f comm) = s.noncommProd (fun i ↦ g (f i)) ⋯

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
i : ↥s
⊢ ∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j

Tactic:
by

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

Goal state before:
pp: α : Type u_6
a : Multiset α
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a

Tactic:
by

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

Goal state before:
pp: α : Type u_6
a : Multiset α
l : List (Multiset α)
⊢ Disjoint a l.sum ↔ ∀ b ∈ l, Disjoint a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ ConjAct.toConjAct g • H = H ↔ g ∈ normalizer ↑H

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ s.noncommProd f comm = m ^ #s

Tactic:
by

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

Goal state before:
pp: α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint (sum ⟦l⟧) a ↔ ∀ b ∈ ⟦l⟧, Disjoint b a

Tactic:
by

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

Goal state before:
pp: α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
⊢ Disjoint a i.sum ↔ ∀ b ∈ i, Disjoint a b

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y : β
h : ∀ x ∈ s, Commute y (f x)
⊢ Commute y (s.noncommProd f comm)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
inst✝ : DecidableEq α
s : Finset ι
a : α
f : ι → Multiset α
⊢ count a (∑ x ∈ s, f x) = ∑ x ∈ s, count a (f x)

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
S : Multiset M
⊢ S.toFinset.prod id ∣ S.prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s).Pairwise (Commute on f)
comm' : ∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → (Commute on f) x x_1
⊢ f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : List M
⊢ ofMul s.prod = (List.map (⇑ofMul) s).sum

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : List (Additive M)
⊢ toMul s.sum = (List.map (⇑toMul) s).prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s).Pairwise (Commute on f)
comm' : ∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → (Commute on f) x x_1
⊢ (s.erase a).noncommProd f comm' * f a = s.noncommProd f comm

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝ : AddMonoid M
s : List M
⊢ ofAdd s.sum = (List.map (⇑ofAdd) s).prod

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List ↥S
⊢ ↑l.prod ∈ S

Tactic:
exact l.prod.coe_prop

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List M
hl : ∀ x ∈ l, x ∈ S
⊢ l.prod ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset M
hm : ∀ a ∈ m, a ∈ S
⊢ m.prod ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
m : Multiset M
comm : {x | x ∈ m}.Pairwise Commute
h : ∀ x ∈ m, x ∈ S
⊢ m.noncommProd comm ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
⊢ t.noncommProd f comm ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
⊢ ↑∅ ⊆ s ∧ Function.support 0 ⊆ ↑∅ ∧ ∏ a ∈ ∅, a ^ 0 a = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_6
inst✝ : CommMonoid β
s : Finset α
f : α → β
⊢ s.noncommProd f ⋯ = s.prod f

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝ : AddMonoid M
s : List (Multiplicative M)
⊢ toAdd s.prod = (List.map (⇑toAdd) s).sum

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ ofMul s.prod = (Multiset.map (⇑ofMul) s).sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x✝ : M
s : Set M
x : M
hx : x ∈ s
⊢ ↑{x} ⊆ s ∧ Function.support (Pi.single x 1) ⊆ ↑{x} ∧ ∏ a ∈ {x}, a ^ Pi.single x 1 a = x

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset (Additive M)
⊢ toMul s.sum = (Multiset.map (⇑toMul) s).prod

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
s : Multiset M
⊢ ofAdd s.sum = (Multiset.map (⇑ofAdd) s).prod

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
s : Multiset (Multiplicative M)
⊢ toAdd s.prod = (Multiset.map (⇑toAdd) s).sum

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
f : α → β
comm : (↑(s ∪ t)).Pairwise (Commute on f)
⊢ (s ∪ t).noncommProd f comm = s.noncommProd f ⋯ * t.noncommProd f ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
⊢ (↑s).Pairwise fun x y ↦ Commute ((f * g) x) ((f * g) y)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
⊢ s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ insert i (univ.erase i),
    (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M x_1) (x x_1)) = Pi.mulSingle x_1 (x x_1) i

pp: case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (insert i (univ.erase i)).noncommProd (fun j ↦ Pi.mulSingle j (x j) i) ⋯ = x i

Tactic:
· intro j _; dsimp

Goal state after:
case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (insert i (univ.erase i)).noncommProd (fun j ↦ Pi.mulSingle j (x j) i) ⋯ = x i
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
hx : x ∈ closure s
⊢ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
⊢ (∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x) → x ∈ closure s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
⊢ univ.noncommProd (fun i ↦ Pi.mulSingle i (x i)) ⋯ = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Finset M
⊢ x ∈ closure ↑s → ∃ f, Function.support f ⊆ ↑s ∧ ∏ a ∈ s, a ^ f a = x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
x y : α × β
hxy : (r.prod s) x y
⊢ (Quotient.mk'' x.1, Quotient.mk'' x.2).1 = (Quotient.mk'' y.1, Quotient.mk'' y.2).1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
x y : α × β
hxy : (r.prod s) x y
⊢ (Quotient.mk'' x.1, Quotient.mk'' x.2).2 = (Quotient.mk'' y.1, Quotient.mk'' y.2).2

Tactic:
simpa [Quotient.eq] using hxy.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
x y : α × β
hxy : (r.prod s) x y
⊢ (Quotient.mk'' x.1, Quotient.mk'' x.2).2 = (Quotient.mk'' y.1, Quotient.mk'' y.2).2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient r × Quotient s
⊢ (fun q ↦ q.liftOn' (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯)
      ((fun x ↦
          match x with
          | (x, y) => Quotient.map₂ Prod.mk ⋯ x y)
        q) =
    q

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
⊢ (fun x ↦
        match x with
        | (x, y) => Quotient.map₂ Prod.mk ⋯ x y)
      ((fun q ↦ q.liftOn' (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯) q) =
    q

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : Quotient piSetoid
x y : (i : ι) → α i
hxy : piSetoid x y
⊢ (fun i ↦ Quotient.mk'' (x i)) = fun i ↦ Quotient.mk'' (y i)

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : (i : ι) → Quotient (r i)
⊢ (fun q ↦ q.liftOn' (fun x i ↦ Quotient.mk'' (x i)) ⋯) ((fun x ↦ Quotient.mk'' fun i ↦ (x i).out) q) = q

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : Quotient piSetoid
⊢ (fun x ↦ Quotient.mk'' fun i ↦ (x i).out) ((fun q ↦ q.liftOn' (fun x i ↦ Quotient.mk'' (x i)) ⋯) q) = q

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
⊢ ⇑(sInf s) = sInf (@r α '' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
iseqv : Equivalence r
⊢ { r := r, iseqv := iseqv } = ⊤ ↔ r = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
iseqv : Equivalence r
⊢ { r := r, iseqv := iseqv } = ⊥ ↔ r = fun x1 x2 ↦ x1 = x2

Tactic:
by

Goal state after: