mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ s ⊆ ↑(map (↑(MulAut.conj h)) (closure s))

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ s ⊆ ↑(map (↑(MulAut.conj h)) (closure s))
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : map (↑(MulAut.conj y)) H = H
hx : f y ∈ map f (normalizer ↑H)
this : (↑(MulAut.conj (f y))).comp f = f.comp ↑(MulAut.conj y)
⊢ map (↑(MulAut.conj (f y))) (map f H) = map f H

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : map (↑(MulAut.conj y)) H = H
hx : f y ∈ map f (normalizer ↑H)
this : (↑(MulAut.conj (f y))).comp f = f.comp ↑(MulAut.conj y)
⊢ map (↑(MulAut.conj (f y))) (map f H) = map f H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : map (↑(MulAut.conj y)) H = H
hx : f y ∈ map f (normalizer ↑H)
this : (↑(MulAut.conj (f y))).comp f = f.comp ↑(MulAut.conj y)
⊢ map f H = map f H

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ map f (normalizer ↑(comap f H)) ≤ normalizer ↑H

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ map f (normalizer ↑(comap f H)) ≤ normalizer ↑H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ normalizer ↑H ≤ normalizer ↑H

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ (H.subgroupOf K).Normal ↔ (H.subgroupOf K).Normal

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ (∃ i, ∃ (_ : i ∈ s), x ∈ conjugatesOf i) ↔ ∃ a ∈ s, IsConj a x

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ (∃ i, ∃ (_ : i ∈ s), x ∈ conjugatesOf i) ↔ ∃ a ∈ s, IsConj a x
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_3
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * x * g⁻¹ * (g * y * g⁻¹) ∈ normalClosure s

Tactic:
]

Goal state after:
case refine_3
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * x * g⁻¹ * (g * y * g⁻¹) ∈ normalClosure s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_4
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ (g * x * g⁻¹)⁻¹ ∈ normalClosure s

Tactic:
]

Goal state after:
case refine_4
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ (g * x * g⁻¹)⁻¹ ∈ normalClosure s
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s t : Set α
⊢ image2 (fun a b ↦ op b • a) t s = image2 (fun x1 x2 ↦ x1 * x2) t s

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : Mul α
s t : Set α
⊢ image2 (fun a b ↦ op b • a) t s = image2 (fun x1 x2 ↦ x1 * x2) t s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ s ⊆ {1} ↔ s ⊆ {1}

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ (fun x ↦ a * x) '' s ∪ (fun x ↦ b * x) '' s = a • s ∪ b • s

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ (fun x ↦ a * x) '' s ∪ (fun x ↦ b * x) '' s = a • s ∪ b • s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ (fun x ↦ x * a) '' s ∪ (fun x ↦ x * b) '' s = s <• a ∪ s <• b

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ (fun x ↦ x * a) '' s ∪ (fun x ↦ x * b) '' s = s <• a ∪ s <• b
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
⊢ 1 ∈ H

Tactic:
]

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
⊢ 1 ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ 1 * a * 1⁻¹ ∈ H

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ 1 * a * 1⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ a * b = a * b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
⊢ a ^ (n.succ * 2) = a ^ (n.succ * 2)

Tactic:
]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * b * a * (c * b)⁻¹ ∈ H

Tactic:
]

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * b * a * (c * b)⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
ih : a ^ (n + 1) = a
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
q : M
eq : q * a = 1
⊢ a = a

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ ⨅ i, map (↑(MulAut.conj g)) (map (↑(MulAut.conj i)) H) = ⨅ x, map (↑(MulAut.conj ((Equiv.mulLeft g) x))) H

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ ⨅ i, map (↑(MulAut.conj g)) (map (↑(MulAut.conj i)) H) = ⨅ x, map (↑(MulAut.conj ((Equiv.mulLeft g) x))) H
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_6
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M
he : IsIdempotentElem e
f : F
⊢ f e = f e

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
a : α
⊢ s = univ ↔ s = univ

Tactic:
]

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
g : G
⊢ map (↑(MulAut.conj g)) H ≤ map (↑(MulAut.conj g)) H

Tactic:
]

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⨅ g, map (↑(MulAut.conj g)) H = ⨅ x, comap (↑(MulAut.conj ((Equiv.inv G) x))) H

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⨅ g, map (↑(MulAut.conj g)) H = ⨅ x, comap (↑(MulAut.conj ((Equiv.inv G) x))) H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
N : Type u_5
inst✝² : Group N
G' : Type u_8
N' : Type u_9
inst✝¹ : Group G'
inst✝ : Group N'
f : G →* N
g : G' →* N'
⊢ comap (f.prodMap g) ⊥ = comap (f.prodMap g) ⊥

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ Subgroup.map f (normalizer ↑H) ≤ normalizer ↑(Subgroup.map f H)

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ Subgroup.map f (normalizer ↑H) ≤ normalizer ↑(Subgroup.map f H)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ (∀ (b : N), ?m.45 b) ↔ ∀ (h : N), f.symm h ∈ H ↔ f.symm (x * h * x⁻¹) ∈ H

pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ ∀ (a : G), (a ∈ H ↔ f.symm x * a * (f.symm x)⁻¹ ∈ H) ↔ ?m.45 (f.toEquiv a)

pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ N → Prop

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ ∀ (a : G), (a ∈ H ↔ f.symm x * a * (f.symm x)⁻¹ ∈ H) ↔ (f.symm (f.toEquiv a) ∈ H ↔ f.symm (x * f.toEquiv a * x⁻¹) ∈ H)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ g.ker

Tactic:
]

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ g.ker
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f (f_inv (x * y)) = f (f_inv x) * f (f_inv y)

Tactic:
]

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f (f_inv (x * y)) = f (f_inv x) * f (f_inv y)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv (f x) * x⁻¹ ∈ g.ker

Tactic:
]

Goal state after:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv (f x) * x⁻¹ ∈ g.ker
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
h : ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
i j : α
ne : ((j⁻¹ * i) • s ∩ s).Nonempty
⊢ i = j

Tactic:
by simpa [inv_mul_eq_one, eq_comm] using h _ ne

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

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f (f_inv (f x)) = f x

Tactic:
]

Goal state after:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f (f_inv (f x)) = f x
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) = of d
H : (map f) a✝¹ = 1
⊢ f head = d

Tactic:
]

Goal state after:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) = of d
H : (map f) a✝¹ = 1
⊢ f head = d
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H : Subgroup N
⊢ H.Normal ↔ H.Normal

Tactic:
]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G ≃* G'
H : Subgroup G
⊢ H.Normal ↔ H.Normal

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : B ≤ normalizer ↑(B' ⊓ B)
⊢ A ⊓ B ≤ normalizer ↑(A ⊓ B' ⊓ (A ⊓ B))

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : B ≤ normalizer ↑(B' ⊓ B)
⊢ A ⊓ B ≤ normalizer ↑(A ⊓ B' ⊓ (A ⊓ B))
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : CommGroup β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
x : α × β
f : F
⊢ x • graphOn (⇑f) univ = graphOn (fun a ↦ x.2 / f x.1 * f a) univ

Tactic:
by simp [smul_graphOn]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : B ≤ normalizer ↑(B' ⊓ B)
⊢ A ⊓ B ≤ normalizer ↑(A ⊓ (B' ⊓ B))

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : B ≤ normalizer ↑(B' ⊓ B)
⊢ A ⊓ B ≤ normalizer ↑(A ⊓ (B' ⊓ B))
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : A ≤ normalizer ↑(A' ⊓ A)
⊢ A ⊓ B ≤ normalizer ↑(A' ⊓ B ⊓ (A ⊓ B))

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : A ≤ normalizer ↑(A' ⊓ A)
⊢ A ⊓ B ≤ normalizer ↑(A' ⊓ B ⊓ (A ⊓ B))
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : A ≤ normalizer ↑(A' ⊓ A)
⊢ A ⊓ B ≤ normalizer ↑(A' ⊓ A ⊓ B)

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : A ≤ normalizer ↑(A' ⊓ A)
⊢ A ⊓ B ≤ normalizer ↑(A' ⊓ A ⊓ B)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
⊢ ∀ (i : ι), h * g * h⁻¹ ∈ a i

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
⊢ ∀ (i : ι), h * g * h⁻¹ ∈ a i
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons_cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂✝ → 1 ≤ x
⊢ a * l₂✝.prod ≤ a * l₂✝.prod

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
⊢ (iInf a).Normal

Tactic:
by
  constructor
  intro g g_in_iInf h
  rw [Subgroup.mem_iInf] at g_in_iInf ⊢
  intro i
  exact (norm i).conj_mem g (g_in_iInf i) h

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * a ∈ H
⊢ b * a ∈ H

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * a ∈ H
⊢ b * a ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y = (x⁻¹ * y⁻¹)⁻¹
⊢ x * y = y * x

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y = (x⁻¹ * y⁻¹)⁻¹
⊢ x * y = y * x
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ hd * tl.prod

Tactic:
]

Goal state after:
case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ hd * tl.prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod ∧ (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

Tactic:
]

Goal state after:
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod ∧ (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * (y * x⁻¹ * y⁻¹) ∈ H₁
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₁.toSubmonoid

Tactic:
by simpa [mul_assoc]

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

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map f l).prod ∧ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map g l).prod

Tactic:
]

Goal state after:
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map f l).prod ∧ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map g l).prod
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ H ≤ normalizer ↑(N ⊓ H)

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ H ≤ normalizer ↑(N ⊓ H)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case inl
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take n L).prod * L[n]

Tactic:
]

Goal state after:
case inl
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take n L).prod * L[n]
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ H ⊔ N ≤ normalizer ↑N

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ H ⊔ N ≤ normalizer ↑N
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 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 : List α
ih : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
hpla : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a * s.prod) ≤ f a * (map f s).prod

Tactic:
h_mul a s.prod (hpl _ mem_cons_self) hp_prod,

Goal state after:
case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 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 : List α
ih : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
hpla : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f a * f s.prod ≤ f a * (map f s).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 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 : List α
ih : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
hpla : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f a * (map f s).prod ≤ f a * (map f s).prod

Tactic:
]

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h✝ : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
h : c⁻¹ * x * c ∈ N
⊢ c⁻¹ * x * c ∈ N

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h✝ : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
h : c⁻¹ * x * c ∈ N
⊢ c⁻¹ * x * c ∈ N
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ x = x

Tactic:
]

Goal state after: