G : Type u_1
G' : Type ?u.448898
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.448907
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ normalCore H
⊢ 1 * a * 1⁻¹ ∈ H
G : Type u_1
G' : Type ?u.448898
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.448907
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ normalCore H
⊢ a ∈ H
rw [← mul_one a, ← inv_one, ← one_mul a]
no goals
G : Type u_1
G' : Type ?u.448898
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.448907
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ normalCore H
⊢ 1 * a * 1⁻¹ ∈ H
exact h 1