mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H K : Subgroup G
inst✝ : H.Normal
g : G
hg : g ∈ centralizer ↑H
i h : G
hh : h ∈ ↑H
⊢ h * (i * g * i⁻¹) = i * g * i⁻¹ * h

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
hH : H.Characteristic
⊢ (centralizer ↑H).Characteristic

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x : G
hx : x ∈ ⨅ g ∈ s, centralizer {g}
⊢ x ∈ centralizer s

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
⊢ {y | toLex (a, y) ∈ s}.IsPWO

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ center G = ⨅ g ∈ s, centralizer {g}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ center G = ⨅ g, centralizer {↑g}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ centralizer s ≤ normalizer s

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : c ∈ centralizer s
hn : n ∈ normalizer s
g : G
hg : g ∈ s
this : n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1
⊢ ⁅n * c * n⁻¹, g⁆ = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
s : Set G
⊢ ((centralizer s).subgroupOf (normalizer s)).Normal

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
⊢ WellFounded (Prod.Lex rα rβ on fun c ↦ (f c, g c))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ normalizer {g} = centralizer {g}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
⊢ ∀ (x y : ↥(normalizer ↑H)) (b : ↥H), (x * y) • b = x • y • b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
g : ↥H
⊢ 1 • g = g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
⊢ ∀ (r : ↥(normalizer ↑H)), r • 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
⊢ ∀ (r : ↥(normalizer ↑H)) (x y : ↥H), r • (x * y) = r • x * r • y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalizerMonoidHom.ker = (centralizer ↑H).subgroupOf (normalizer ↑H)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
⊢ WellFounded (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
s : Set γ
hι : s.WellFoundedOn (rι on f)
hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
⊢ s.WellFoundedOn (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Hom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
a x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
h : SemiconjBy a x y
f : F
⊢ SemiconjBy (f a) (f x) (f y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Hom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
a x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ⇑f
h : SemiconjBy (f a) (f x) (f y)
⊢ f (a * x) = f (y * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Hom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ⇑f
h : Commute (f x) (f y)
⊢ f (x * y) = f (y * x)

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (↑l) comm b = List.foldr f b l

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β → β
s : Multiset α
a : α
h : {x | x ∈ a ::ₘ s}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
h' : {x | x ∈ s}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (a ::ₘ s) h b = f a (noncommFoldr f s h' b)

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β → β
s : Multiset α
h : LeftCommutative f
b : β
⊢ noncommFoldr f s ⋯ b = foldr f b s

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 : α → α → α
assoc : Std.Associative op
s : Multiset α
comm : {x | x ∈ s}.Pairwise fun x y ↦ op x y = op y x
x : α
hx : x ∈ {x | x ∈ s}
y : α
hy : y ∈ {x | x ∈ s}
h : x ≠ y
b : α
⊢ op x (op y b) = op y (op x b)

Tactic:
by

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

Goal state before:
pp: α : Type u_3
op : α → α → α
assoc : Std.Associative op
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y ↦ op x y = op y x
a : α
⊢ noncommFold op (↑l) comm a = List.foldr op a l

Tactic:
by

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

Goal state before:
pp: G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
⊢ a • ↑s = ↑s

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Subgroup G
⊢ ↑s = ↑⊥ ↔ ↑s = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_3
op : α → α → α
assoc : Std.Associative op
s : Multiset α
a : α
h : {x | x ∈ a ::ₘ s}.Pairwise fun x y ↦ op x y = op y x
h' : {x | x ∈ s}.Pairwise fun x y ↦ op x y = op y x
x : α
⊢ noncommFold op (a ::ₘ s) h x = op a (noncommFold op s h' x)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
⊢ MulOpposite.op a • ↑s = ↑s

Tactic:
by

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

Goal state before:
pp: G : Type u_2
S : Type u_4
inst✝² : SetLike S G
inst✝¹ : DivisionMonoid G
inst✝ : SubgroupClass S G
H : S
⊢ ↑H / ↑H = ↑H

Tactic:
by

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

Goal state before:
pp: α : Type u_3
op : α → α → α
assoc : Std.Associative op
s : Multiset α
inst✝ : Std.Commutative op
a : α
⊢ noncommFold op s ⋯ a = fold op a s

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ s * ↑(closure s) = ↑(closure s)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ↑(closure s) * s = ↑(closure s)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ s ^ 0 * ↑(closure s) = ↑(closure s)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ s ^ (n + 1) * ↑(closure s) = ↑(closure s)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ↑(closure s) * s ^ 0 = ↑(closure s)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ ↑(closure s) * s ^ (n + 1) = ↑(closure s)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s ∈ ↑(closure S)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
⊢ (closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
⊢ (zpowers g).toSubmonoid = Submonoid.powers g ⊔ Submonoid.powers g⁻¹

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
⊢ Submonoid.powers g ≤ (zpowers g).toSubmonoid

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
l : List α
comm : {x | x ∈ ↑l}.Pairwise Commute
⊢ (↑l).noncommProd comm = l.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
a : α
comm : {x | x ∈ a ::ₘ s}.Pairwise Commute
⊢ (a ::ₘ s).noncommProd comm = a * s.noncommProd ⋯

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x⁻¹ * y) ⋯
x : G
h : x ∈ closure s
⊢ p x h

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : x ∈ closure s
m : Gᵐᵒᵖ
hm : m ∈ closure (MulOpposite.unop ⁻¹' s)
⊢ MulOpposite.unop m ∈ closure s

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : x ∈ closure s
⊢ { unop' := x } ∈ closure (MulOpposite.unop ⁻¹' s)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ = closure s

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
x : G
⊢ closure {x⁻¹} = closure {x}

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ ⨆ i, S i
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : G
hx : x ∈ ⨆ i, S i
⊢ C x hx

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
H : Subgroup G
n : ℕ
hs : s ⊆ ↑H
⊢ s ^ n ⊆ ↑H

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
⊢ closure (s ^ n) ≤ closure s

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
m n : ℕ
hmn : m ∣ n
⊢ closure (s ^ n) ≤ closure (s ^ m)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ closure s ≤ closure (s ^ n)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
⊢ S * ↑N = ↑N * S

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑(H ⊔ N) = ↑H * ↑N

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
N H : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑(N ⊔ H) = ↑N * ↑H

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
this : y⁻¹ * (y * z) ∈ C
⊢ z ∈ ↑C

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
⊢ ↑A * ↑(B ⊓ C) = ↑A * ↑B ∩ ↑C

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
a : α
comm : {x | x ∈ a ::ₘ s}.Pairwise Commute
⊢ (a ::ₘ s).noncommProd comm = s.noncommProd ⋯ * a

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ ↑B
z : G
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
this : y * z * z⁻¹ ∈ A
⊢ y ∈ ↑A

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s t : Multiset α
comm : {x | x ∈ s + t}.Pairwise Commute
⊢ (s + t).noncommProd comm = s.noncommProd ⋯ * t.noncommProd ⋯

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
⊢ ↑(A ⊓ B) * ↑C = ↑A ∩ (↑B * ↑C)

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p x
⊢ p (s.noncommProd comm)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
⊢ normalizer ↑H ⊓ normalizer ↑K ≤ normalizer ↑(H ⊔ K)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
⊢ {x | x ∈ map (⇑f) s}.Pairwise Commute

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Finset M
⊢ s.val.prod = s.prod id

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
⊢ f (s.noncommProd comm) = (map (⇑f) s).noncommProd ⋯

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
⊢ ⨅ i, normalizer ↑(H i) ≤ normalizer ↑(⨆ i, H i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
⊢ ∑ a ∈ s, {a} = s.val

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
m : α
h : ∀ x ∈ s, x = m
⊢ s.noncommProd comm = m ^ s.card

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
G : Type u_7
inst✝¹ : FunLike G M N
inst✝ : MonoidHomClass G M N
g : G
f : ι → M
s : Finset ι
⊢ g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)

Tactic:
by

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

Goal state before:
pp: α : Type u_6
inst✝ : CommMonoid α
s : Multiset α
⊢ s.noncommProd ⋯ = s.prod

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
f : ι → M
inst✝¹ : CommMonoid M
inst✝ : IsEmpty ι
s : Finset ι
⊢ ∏ i ∈ s, f i = 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝ : CommMonoid M
⊢ ∏ _x ∈ s, 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
y : α
h : ∀ x ∈ s, Commute y x
⊢ Commute y (s.noncommProd comm)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
hHnK : normalizer ↑H ≤ normalizer ↑K
⊢ normalizer ↑H ≤ normalizer ↑(K ⊔ H)

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 ι
e : ι ↪ κ
f : κ → M
⊢ ∏ x ∈ map e s, f x = ∏ x ∈ s, f (e x)

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 ι
e : ι ↪ κ
⊢ (map e s).prod = fun f ↦ ∏ x ∈ s, f (e 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
s : Finset ι
f : ι → M
⊢ (List.map f s.toList).prod = s.prod f

Tactic:
by

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

Goal state before:
pp: M : Type u_7
inst✝ : CommMonoid M
s : Finset M
⊢ s.toList.prod = ∏ x ∈ s, x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
n : G
hmem : n ∈ H ⊔ K
g : G
⊢ g * n * g⁻¹ ∈ H ⊔ K

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
σ : Equiv.Perm ι
s : Finset ι
f : ι → M
hs : {a | σ a ≠ a} ⊆ ↑s
⊢ ∏ x ∈ s, f (σ x) = ∏ x ∈ s, f x

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
this : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x
⊢ a * (l.erase a).prod = l.prod

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup A
s : Set G
ι : Sort u_5
H : ι → Subgroup G
inst✝ : ∀ (i : ι), (H i).Normal
⊢ (⨆ i, H i).Normal

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Type u_5
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, (H i).Normal
⊢ (⨆ i ∈ s, H i).Normal

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
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a | σ a ≠ a} ⊆ ↑s
⊢ ∏ x ∈ s, f (σ x) x = ∏ x ∈ s, f x ((Equiv.symm σ) x)

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
Hs : Set (Subgroup G)
h : ∀ H ∈ Hs, H.Normal
⊢ (sSup Hs).Normal

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
hg : g ∈ closure s
x : X
hx : x ∈ t
⊢ g • x ∈ t

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
h : Gᵐᵒᵖ
s : Set G
⊢ (fun y ↦ h • y) '' (fun x ↦ g * x) ⁻¹' s = (fun x ↦ g * x) ⁻¹' (fun y ↦ h • y) '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
S : Subgroup G
⊢ 1 • S = S

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 ≤ 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
⊢ MulAut.conj h • H = H

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
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
⊢ ∏ x ∈ s, f x = ∏ x ∈ t, g 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
⊢ a * (s.erase a).noncommProd comm' = s.noncommProd comm

Tactic:
by

Goal state after: