-- Mathlib/GroupTheory/GroupAction/Quotient.lean
theorem normalCore_eq_ker : H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker

Tactic:
apply le_antisymm

Result:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore ≤ (MulAction.toPermHom G (G ⧸ H)).ker

case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (MulAction.toPermHom G (G ⧸ H)).ker ≤ H.normalCore

Proof state:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (MulAction.toPermHom G (G ⧸ H)).ker ≤ H.normalCore

Tactic:
refine (Subgroup.normal_le_normalCore.mpr fun g hg => ?_)

Result:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ g ∈ H

Proof state:
case a.H
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H

Tactic:
exact H.normalCore.inv_mem hg g'⁻¹

Result:
no goals

Proof state:
case a.H
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
⊢ ∀ (z : G), ((MulAction.toPermHom G (G ⧸ H)) g) ↑z = 1 ↑z

Tactic:
refine fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr ?_)

Result:
case a.H
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ (g • g')⁻¹ * g' ∈ H

Proof state:
case a.H
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ (g • g')⁻¹ * g' ∈ H

Tactic:
rw [smul_eq_mul, mul_inv_rev, ← inv_inv g', inv_inv]

Result:
case a.H
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H

Proof state:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore ≤ (MulAction.toPermHom G (G ⧸ H)).ker

Tactic:
intro g hg

Result:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
⊢ g ∈ (MulAction.toPermHom G (G ⧸ H)).ker

Proof state:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ ↑(g * 1) = ↑1

Tactic:
exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))

Result:
no goals

Proof state:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
⊢ g ∈ (MulAction.toPermHom G (G ⧸ H)).ker

Tactic:
apply Equiv.Perm.ext

Result:
case a.H
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
⊢ ∀ (x : G ⧸ H), ((MulAction.toPermHom G (G ⧸ H)) g) x = 1 x

Proof state:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ g ∈ H

Tactic:
rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]

Result:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ ↑(g * 1) = ↑1

Proof state:
case a.H
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
⊢ ∀ (x : G ⧸ H), ((MulAction.toPermHom G (G ⧸ H)) g) x = 1 x

Tactic:
refine fun q ↦ QuotientGroup.induction_on q ?_

Result:
case a.H
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
⊢ ∀ (z : G), ((MulAction.toPermHom G (G ⧸ H)) g) ↑z = 1 ↑z