awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g : G
hg : Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer s) g
this :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
⊢ (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure s) : Set G)

Tactic:
rw [AddSubgroup.mem_normalizer_iff_addConj_image_eq.mp hg] at this

Premises used: AddSubgroup.mem_normalizer_iff_addConj_image_eq, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g : G
hg : Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer s) g
this rwa rwa₁ rwa₂ rwa₃ :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure s) : Set G)
⊢ Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer (↑(AddSubgroup.closure s) : Set G)) g

Tactic:
rwa [AddSubgroup.mem_normalizer_iff_addConj_image_eq]

Premises used: AddSubgroup.mem_normalizer_iff_addConj_image_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Eq (α := Subgroup G) (normalizer (↑H : Set G)) ⊤ ↔ H.Normal

Tactic:
eq_top_iff.trans
    ⟨fun h => ⟨fun a ha b => (h (mem_top b) a).mp ha⟩, fun h a _ha b =>
      ⟨fun hb => h.conj_mem b hb a, fun hb => inv_mul_cancel_left a b ▸ h.mem_comm_iff.mp hb⟩⟩

Premises used: Subgroup.Normal.mem_comm_iff, eq_top_iff, inv_mul_cancel_left, Eq.rec, Subgroup.Normal.mk, Iff.intro, Iff.mp, Subgroup.mem_top, Iff.trans, Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.Normal
⊢ Eq (α := Subgroup G) (normalizer (↑H : Set G)) ⊤

Tactic:
normalizer_eq_top_iff.mpr h

Premises used: Iff.mpr, Subgroup.normalizer_eq_top_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
⊢ H ≤ normalizer s ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s

Tactic:
⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩

Premises used: Iff.intro, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
refine : ∀ (hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s) (h : G) (hh : h ∈ H) (k : G) (hk : h * k * h⁻¹ ∈ s), k ∈ s
⊢ H ≤ normalizer s ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s

Tactic:
refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s
h : G
hh : h ∈ H
k : G
hk : h * k * h⁻¹ ∈ s
⊢ k ∈ s

Tactic:
simpa [mul_assoc] using hH h⁻¹ (inv_mem hh) _ hk

Premises used: mul_assoc, InvMemClass.inv_mem, Inv.inv
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H ≤ normalizer (↑K : Set G) ↔ ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K

Tactic:
⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩

Premises used: Iff.intro, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
refine :
  ∀ (hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K) (h : G) (hh : h ∈ H) (k : G) (hk : h * k * h⁻¹ ∈ (↑K : Set G)),
    k ∈ (↑K : Set G)
⊢ H ≤ normalizer (↑K : Set G) ↔ ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K

Tactic:
refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K
h : G
hh : h ∈ H
k : G
hk : h * k * h⁻¹ ∈ (↑K : Set G)
⊢ k ∈ (↑K : Set G)

Tactic:
simpa [mul_assoc] using hH h⁻¹ (inv_mem hh) _ hk

Premises used: mul_assoc, InvMemClass.inv_mem, Inv.inv
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
⊢ H ≤ normalizer (↑(closure s) : Set G) ↔ ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)

Tactic:
⟨fun hH h hh g hg ↦ hH hh g |>.mp <| mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩

Premises used: Subgroup.mem_closure_of_mem, Iff.intro, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
refine :
  ∀ (hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)) (h : G) (hh : h ∈ H),
    Membership.mem (γ := Subgroup G) (normalizer (↑(closure s) : Set G)) h
⊢ H ≤ normalizer (↑(closure s) : Set G) ↔ ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)

Tactic:
refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp <| mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
h : G
hh : h ∈ H
⊢ (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)

Tactic:
have : MulAut.conj h '' (closure s) = closure (MulAut.conj h '' s) :=
    congr($(MulAut.conj h |>.toMonoidHom.map_closure s))
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
h : G
hh : h ∈ H
this :
  (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
rw :
  (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G) =
    (↑(closure s) : Set G)
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑(closure s) : Set G)) h

Tactic:
rw [mem_normalizer_iff_conj_image_eq, this]

Premises used: Subgroup.mem_normalizer_iff_conj_image_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
h : G
hh : h ∈ H
this :
  (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
⊢ (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G) ⊆
    (↑(closure s) : Set G)

Tactic:
simpa using hH h hh
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
h : G
hh : h ∈ H
this :
  (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
apply :
  (↑(closure s) : Set G) ⊆
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
⊢ (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G) =
    (↑(closure s) : Set G)

Tactic:
apply subset_antisymm <| by simpa using hH h hh

Premises used: subset_antisymm
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
h : G
hh : h ∈ H
this :
  (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
rw : s ⊆ (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G)
⊢ (↑(closure s) : Set G) ⊆
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)

Tactic:
rw [SetLike.coe_subset_coe, closure_le, ← this]

Premises used: Subgroup.closure_le, SetLike.coe_subset_coe
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
h : G
hh : h ∈ H
this :
  (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
g : G
hg : g ∈ s
⊢ (((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) (h⁻¹ * g * h⁻¹⁻¹) = g

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
h : G
hh : h ∈ H
this :
  (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
⊢ s ⊆ (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G)

Tactic:
exact fun g hg ↦ ⟨_, hH _ (inv_mem hh) g hg, by simp [mul_assoc]⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
⊢ H ≤ AddSubgroup.normalizer (↑(AddSubgroup.closure s) : Set G) ↔
    ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)

Tactic:
⟨fun hH h hh g hg ↦ hH hh g |>.mp <| AddSubgroup.mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩

Premises used: AddSubgroup.mem_closure_of_mem, Iff.intro, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
refine :
  ∀ (hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)) (h : G)
    (hh : h ∈ H), Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer (↑(AddSubgroup.closure s) : Set G)) h
⊢ H ≤ AddSubgroup.normalizer (↑(AddSubgroup.closure s) : Set G) ↔
    ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)

Tactic:
refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp <| AddSubgroup.mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
h : G
hh : h ∈ H
⊢ (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)

Tactic:
have : AddAut.conj h '' (AddSubgroup.closure s) = AddSubgroup.closure (AddAut.conj h '' s) :=
    congr($(AddAut.conj h |>.toAddMonoidHom.map_closure s))
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
h : G
hh : h ∈ H
this :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
rw :
  (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G) =
    (↑(AddSubgroup.closure s) : Set G)
⊢ Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer (↑(AddSubgroup.closure s) : Set G)) h

Tactic:
rw [AddSubgroup.mem_normalizer_iff_addConj_image_eq, this]

Premises used: AddSubgroup.mem_normalizer_iff_addConj_image_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
h : G
hh : h ∈ H
this :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
⊢ (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G) ⊆
    (↑(AddSubgroup.closure s) : Set G)

Tactic:
simpa using hH h hh
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
h : G
hh : h ∈ H
this :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
apply :
  (↑(AddSubgroup.closure s) : Set G) ⊆
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
⊢ (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G) =
    (↑(AddSubgroup.closure s) : Set G)

Tactic:
apply subset_antisymm <| by simpa using hH h hh

Premises used: subset_antisymm
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
h : G
hh : h ∈ H
this :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
rw :
  s ⊆
    (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G)
⊢ (↑(AddSubgroup.closure s) : Set G) ⊆
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)

Tactic:
rw [SetLike.coe_subset_coe, AddSubgroup.closure_le, ← this]

Premises used: SetLike.coe_subset_coe, AddSubgroup.closure_le
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
h : G
hh : h ∈ H
this :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
g : G
hg : g ∈ s
⊢ (((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
          AddAut G) :
        (a : G) → G)
      (-h + g + - -h) =
    g

Tactic:
simp [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
h : G
hh : h ∈ H
this :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
⊢ s ⊆
    (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G)

Tactic:
exact fun g hg ↦ ⟨_, hH _ (neg_mem hh) g hg, by simp [add_assoc]⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : N →* G
x : N
simp :
  (∀ (h : G),
      h ∈ H ↔ HMul.hMul (β := G) (HMul.hMul (α := G) ((f : (a : N) → G) x : G) h) (((f : (a : N) → G) x)⁻¹ : G) ∈ H) →
    ∀ (h : N),
      Membership.mem (α := G) H ((f : (a : N) → G) h : G) ↔
        Membership.mem (α := G) H ((f : (a : N) → G) (x * h * x⁻¹) : G)
⊢ x ∈ comap f (normalizer (↑H : Set G)) → Membership.mem (γ := Subgroup N) (normalizer (↑(comap f H) : Set N)) x

Tactic:
simp only [mem_normalizer_iff, mem_comap]

Premises used: Subgroup.mem_comap, Subgroup.mem_normalizer_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : N →* G
x : N
h :
  ∀ (h : G),
    h ∈ H ↔ HMul.hMul (β := G) (HMul.hMul (α := G) ((f : (a : N) → G) x : G) h) (((f : (a : N) → G) x)⁻¹ : G) ∈ H
n : N
⊢ Membership.mem (α := G) H ((f : (a : N) → G) n : G) ↔ Membership.mem (α := G) H ((f : (a : N) → G) (x * n * x⁻¹) : G)

Tactic:
simp [h (f n)]

Premises used: DFunLike.coe
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : N
simp :
  ∀ (x_1 : G),
    (∀ (h : G), h ∈ H ↔ x_1 * h * x_1⁻¹ ∈ H) →
      (f : (a : G) → N) x_1 = x →
        ∀ (h : N), (∃ x ∈ H, (f : (a : G) → N) x = h) ↔ ∃ x_2 ∈ H, (f : (a : G) → N) x_2 = x * h * x⁻¹
⊢ x ∈ map f (normalizer (↑H : Set G)) → Membership.mem (γ := Subgroup N) (normalizer (↑(map f H) : Set N)) x

Tactic:
simp only [and_imp, mem_map, exists_imp, mem_normalizer_iff]

Premises used: and_imp, Subgroup.mem_normalizer_iff, Subgroup.mem_map, exists_imp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
mp :
  (∃ x ∈ H, (f : (a : G) → N) x = n) →
    ∃ x_1 ∈ H,
      (f : (a : G) → N) x_1 =
        HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)
mpr :
  (∃ x_1 ∈ H,
      (f : (a : G) → N) x_1 =
        HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)) →
    ∃ x ∈ H, (f : (a : G) → N) x = n
⊢ (∃ x ∈ H, (f : (a : G) → N) x = n) ↔
    ∃ x_1 ∈ H,
      (f : (a : G) → N) x_1 =
        HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
y : G
hy : y ∈ H
right :
  (f : (a : G) → N) (x * y * x⁻¹) =
    HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : G) → N) x : N) ((f : (a : G) → N) y : N))
      (((f : (a : G) → N) x)⁻¹ : N)
⊢ ∃ x_1 ∈ H,
    (f : (a : G) → N) x_1 =
      HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : G) → N) x : N) ((f : (a : G) → N) y : N))
        (((f : (a : G) → N) x)⁻¹ : N)

Tactic:
use x * y * x⁻¹, (hx y).1 hy

Premises used: Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
y : G
hy : y ∈ H
⊢ (f : (a : G) → N) (x * y * x⁻¹) =
    HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : G) → N) x : N) ((f : (a : G) → N) y : N))
      (((f : (a : G) → N) x)⁻¹ : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
y : G
hyH : y ∈ H
hy :
  (f : (a : G) → N) y =
    HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)
h : x⁻¹ * y * x ∈ H ∧ (f : (a : G) → N) (x⁻¹ * y * x) = n
⊢ ∃ x ∈ H, (f : (a : G) → N) x = n

Tactic:
use x⁻¹ * y * x
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
y : G
hyH : y ∈ H
hy :
  (f : (a : G) → N) y =
    HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)
h : x * (x⁻¹ * y * x) * x⁻¹ ∈ H ∧ (f : (a : G) → N) (x⁻¹ * y * x) = n
⊢ x⁻¹ * y * x ∈ H ∧ (f : (a : G) → N) (x⁻¹ * y * x) = n

Tactic:
rw [hx]
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
y : G
hyH : y ∈ H
hy :
  (f : (a : G) → N) y =
    HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)
⊢ x * (x⁻¹ * y * x) * x⁻¹ ∈ H ∧ (f : (a : G) → N) (x⁻¹ * y * x) = n

Tactic:
simp [hy, hyH, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : N →* G
h : H ≤ f.range
apply : normalizer (↑(comap f H) : Set N) ≤ comap f (normalizer (↑H : Set G))
⊢ comap f (normalizer (↑H : Set G)) = normalizer (↑(comap f H) : Set N)

Tactic:
apply le_antisymm (le_normalizer_comap f)

Premises used: Subgroup.le_normalizer_comap, le_antisymm