-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem normalClosure_eq_top_of {N : Subgroup G} [hn : N.Normal] {g g' : G} {hg : g ∈ N}
    {hg' : g' ∈ N} (hc : IsConj g g') (ht : normalClosure ({⟨g, hg⟩} : Set N) = ⊤) :
    normalClosure ({⟨g', hg'⟩} : Set N) = ⊤

Proof state:
case intro
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
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)
⊢ normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤

Tactic:
rw [eq_top_iff, ← MonoidHom.range_eq_top.2 hs, MonoidHom.range_eq_map]

Result:
case intro
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
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)
⊢ map (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) ⊤ ≤ normalClosure {⟨c * g * c⁻¹, hg'⟩}

Proof state:
case intro
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
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)
⊢ ⟨g, hg⟩ ∈
    comap (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) (normalClosure {⟨c * g * c⁻¹, hg'⟩})

Tactic:
simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply, coe_mk,
  MonoidHom.restrict_apply, mem_comap]

Result:
case intro
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
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)
⊢ ⟨c * g * c⁻¹, ⋯⟩ ∈ normalClosure {⟨c * g * c⁻¹, hg'⟩}

Proof state:
case mk.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 * c * c⁻¹ = x

Tactic:
rw [mul_assoc, mul_inv_cancel, mul_one]

Result:
no goals

Proof state:
case mk.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:
rwa [inv_inv] at h

Result:
no goals

Proof state:
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
⊢ Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)

Tactic:
rintro ⟨x, hx⟩

Result:
case mk
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
⊢ ∃ a, (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) a = ⟨x, hx⟩

Proof state:
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⁻¹)
⊢ ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N

Tactic:
rintro ⟨x, hx⟩

Result:
case mk
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⁻¹)
x : G
hx : x ∈ N
⊢ (MulAut.conj c) ↑⟨x, hx⟩ ∈ N

Proof state:
case mk
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⁻¹)
x : G
hx : x ∈ N
⊢ (MulAut.conj c) ↑⟨x, hx⟩ ∈ N

Tactic:
exact hn.conj_mem _ hx c

Result:
no goals

Proof state:
case mk
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
⊢ ∃ a, (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) a = ⟨x, hx⟩

Tactic:
refine ⟨⟨c⁻¹ * x * c, ?_⟩, ?_⟩

Result:
case mk.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
⊢ c⁻¹ * x * c ∈ N

case mk.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
⊢ (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) ⟨c⁻¹ * x * c, ?mk.refine_1⟩ = ⟨x, hx⟩

Proof state:
case intro
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
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)
⊢ {⟨g, hg⟩} ⊆
    ↑(comap (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) (normalClosure {⟨c * g * c⁻¹, hg'⟩}))

Tactic:
rw [Set.singleton_subset_iff, SetLike.mem_coe]

Result:
case intro
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
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)
⊢ ⟨g, hg⟩ ∈
    comap (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) (normalClosure {⟨c * g * c⁻¹, hg'⟩})

Proof state:
case intro
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
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)
⊢ map (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) ⊤ ≤ normalClosure {⟨c * g * c⁻¹, hg'⟩}

Tactic:
refine le_trans (map_mono (eq_top_iff.1 ht)) (map_le_iff_le_comap.2 (normalClosure_le_normal ?_))

Result:
case intro
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
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)
⊢ {⟨g, hg⟩} ⊆
    ↑(comap (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) (normalClosure {⟨c * g * c⁻¹, hg'⟩}))

Proof state:
case mk.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
⊢ c⁻¹ * x * c ∈ N

Tactic:
have h := hn.conj_mem _ hx c⁻¹

Result:
case mk.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