case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
⊢ normalClosure {{ val := c * g * c⁻¹, property := hg' }} = ⊤
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g g' : G
hg : g ∈ N
hg' : g' ∈ N
hc : IsConj g g'
ht : normalClosure {{ val := g, property := hg }} = ⊤
⊢ normalClosure {{ val := g', property := hg' }} = ⊤
obtain ⟨c, rfl⟩ := isConj_iff.1 hc
case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
⊢ normalClosure {{ val := c * g * c⁻¹, property := hg' }} = ⊤
case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
⊢ normalClosure {{ val := c * g * c⁻¹, property := hg' }} = ⊤
have h : ∀ x : N, (MulAut.conj c) x ∈ N := by
  rintro ⟨x, hx⟩
  exact hn.conj_mem _ hx c
case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
hs : Surjective ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
⊢ map (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h) ⊤ ≤
    normalClosure {{ val := c * g * c⁻¹, property := hg' }}
case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
hs : Surjective ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
⊢ normalClosure {{ val := c * g * c⁻¹, property := hg' }} = ⊤
rw [eq_top_iff, ← MonoidHom.range_top_of_surjective _ hs, MonoidHom.range_eq_map]
case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
hs : Surjective ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
⊢ {{ val := g, property := hg }} ⊆
    ↑(comap (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
        (normalClosure {{ val := c * g * c⁻¹, property := hg' }}))
case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
hs : Surjective ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
⊢ map (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h) ⊤ ≤
    normalClosure {{ val := c * g * c⁻¹, property := hg' }}
refine' le_trans (map_mono (eq_top_iff.1 ht)) (map_le_iff_le_comap.2 (normalClosure_le_normal _))
case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
hs : Surjective ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
⊢ { val := g, property := hg } ∈
    comap (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
      (normalClosure {{ val := c * g * c⁻¹, property := hg' }})
case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
hs : Surjective ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
⊢ {{ val := g, property := hg }} ⊆
    ↑(comap (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
        (normalClosure {{ val := c * g * c⁻¹, property := hg' }}))
rw [Set.singleton_subset_iff, SetLike.mem_coe]
case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
hs : Surjective ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
⊢ { val := c * g * c⁻¹, property := (_ : (fun x => x ∈ N) (c * g * c⁻¹)) } ∈
    normalClosure {{ val := c * g * c⁻¹, property := hg' }}
case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
hs : Surjective ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
⊢ { val := g, property := hg } ∈
    comap (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
      (normalClosure {{ val := c * g * c⁻¹, property := hg' }})
simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply, coe_mk,
  MonoidHom.restrict_apply, mem_comap]
no goals
case intro
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
hs : Surjective ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
⊢ { val := c * g * c⁻¹, property := (_ : (fun x => x ∈ N) (c * g * c⁻¹)) } ∈
    normalClosure {{ val := c * g * c⁻¹, property := hg' }}
exact subset_normalClosure (Set.mem_singleton _)
case mk
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
x : G
hx : x ∈ N
⊢ ↑(↑MulAut.conj c) ↑{ val := x, property := hx } ∈ N
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
⊢ ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
rintro ⟨x, hx⟩
no goals
case mk
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
x : G
hx : x ∈ N
⊢ ↑(↑MulAut.conj c) ↑{ val := x, property := hx } ∈ N
exact hn.conj_mem _ hx c
case mk
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ ∃ a,
    ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h) a =
      { val := x, property := hx }
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
⊢ Surjective ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
rintro ⟨x, hx⟩
case mk.refine'_1
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ c⁻¹ * x * c ∈ N

case mk.refine'_2
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
      { val := c⁻¹ * x * c, property := ?mk.refine'_1 } =
    { val := x, property := hx }
case mk
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ ∃ a,
    ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h) a =
      { val := x, property := hx }
refine' ⟨⟨c⁻¹ * x * c, _⟩, _⟩
case mk.refine'_2
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ x * c * c⁻¹ = x
case mk.refine'_2
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ ↑(MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom (↑MulAut.conj c)) N) N h)
      { val := c⁻¹ * x * c, property := (_ : c⁻¹ * x * c ∈ N) } =
    { val := x, property := hx }
simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply, coe_mk,
  MonoidHom.restrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_self, one_mul]
no goals
case mk.refine'_2
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ x * c * c⁻¹ = x
rw [mul_assoc, mul_inv_self, mul_one]
case mk.refine'_1
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h✝ : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
h : c⁻¹ * x * c⁻¹⁻¹ ∈ N
⊢ c⁻¹ * x * c ∈ N
case mk.refine'_1
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ c⁻¹ * x * c ∈ N
have h := hn.conj_mem _ hx c⁻¹
no goals
case mk.refine'_1
G : Type u_1
G' : Type ?u.732819
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.732828
inst✝¹ : AddGroup A
N✝ : Type ?u.732834
inst✝ : Group N✝
N : Subgroup G
hn : Normal N
g : G
hg : g ∈ N
ht : normalClosure {{ val := g, property := hg }} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h✝ : ∀ (x : { x // x ∈ N }), ↑(↑MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
h : c⁻¹ * x * c⁻¹⁻¹ ∈ N
⊢ c⁻¹ * x * c ∈ N
rwa [inv_inv] at h