awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : map f (normalizer (↑(comap f H) : Set N)) ≤ normalizer (↑H : Set G)
⊢ normalizer (↑(comap f H) : Set N) ≤ comap f (normalizer (↑H : Set G))

Tactic:
rw [← map_le_iff_le_comap]

Premises used: Subgroup.map_le_iff_le_comap
-- 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 : LE.le (α := Subgroup G) (normalizer (↑(map f (comap f H)) : Set G)) (normalizer (↑H : Set G))
⊢ map f (normalizer (↑(comap f H) : Set N)) ≤ normalizer (↑H : Set G)

Tactic:
apply (le_normalizer_map f).trans

Premises used: LE.le.trans, Subgroup.le_normalizer_map
-- 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
rw rw₁ : LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑H : Set G))
⊢ LE.le (α := Subgroup G) (normalizer (↑(map f (comap f H)) : Set G)) (normalizer (↑H : Set G))

Tactic:
rw [map_comap_eq_self h]

Premises used: Subgroup.map_comap_eq_self
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
h : H ≤ N
⊢ subgroupOf (normalizer (↑H : Set G)) N = normalizer (↑(H.subgroupOf N) : Set ↥N)

Tactic:
comap_normalizer_eq_of_le_range (h.trans_eq N.range_subtype.symm)

Premises used: Subgroup.subgroupOf, LE.le.trans_eq, Subgroup.range_subtype, Eq.symm, Subgroup.comap_normalizer_eq_of_le_range
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
rw : (H.subgroupOf K).Normal ↔ subgroupOf (normalizer (↑H : Set G)) K = ⊤
rw₁ : (H.subgroupOf K).Normal ↔ Eq (α := Subgroup ↥K) (normalizer (↑(H.subgroupOf K) : Set ↥K)) ⊤
rw₂ rw₃ : (H.subgroupOf K).Normal ↔ (H.subgroupOf K).Normal
⊢ (H.subgroupOf K).Normal ↔ K ≤ normalizer (↑H : Set G)

Tactic:
rw [← subgroupOf_eq_top, subgroupOf_normalizer_eq h, normalizer_eq_top_iff]

Premises used: Subgroup.subgroupOf_normalizer_eq, Subgroup.subgroupOf_eq_top, Subgroup.normalizer_eq_top_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (H.subgroupOf K).Normal ↔ K ≤ normalizer (↑(H ⊓ K) : Set G)

Tactic:
inf_subgroupOf_right H K ▸ normal_subgroupOf_iff_le_normalizer inf_le_right

Premises used: inf_le_right, Eq.rec, Subgroup.inf_subgroupOf_right, Subgroup.normal_subgroupOf_iff_le_normalizer
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
H K : Subgroup G
N : Type u_5
inst_4 : Group N
⊢ Normal (G := ↥(normalizer (↑H : Set G))) (H.subgroupOf (normalizer (↑H : Set G)))

Tactic:
(normal_subgroupOf_iff_le_normalizer H.le_normalizer).mpr le_rfl

Premises used: Iff.mpr, le_rfl, Subgroup.le_normalizer, Subgroup.normal_subgroupOf_iff_le_normalizer
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Maximal (fun (x : Subgroup G) ↦ (H.subgroupOf x).Normal) (normalizer (↑H : Set G))

Tactic:
⟨inferInstance,
    fun _ hnormal hle ↦ (normal_subgroupOf_iff_le_normalizer <| le_normalizer.trans hle).mp hnormal⟩

Premises used: inferInstance, Subgroup.le_normalizer, Subgroup.normal_subgroupOf_iff_le_normalizer, And.intro, Iff.mp, Maximal, LE.le.trans
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hK : (H.subgroupOf K).Normal
HK : H ≤ K
⊢ K ≤ normalizer (↑H : Set G)

Tactic:
(normal_subgroupOf_iff_le_normalizer HK).mp hK

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
hH : H.Normal
⊢ S ⊆ (↑(normalizer (↑H : Set G)) : Set G)

Tactic:
(@normalizer_eq_top _ _ H hH) ▸ le_top

Premises used: Eq.rec, Subgroup.normalizer_eq_top, le_top, Eq.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : H.Normal
⊢ K ≤ normalizer (↑H : Set G)

Tactic:
subset_normalizer_of_normal

Premises used: Subgroup.subset_normalizer_of_normal, Set.Subset
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ LE.le (α := Subgroup G) (normalizer (↑H : Set G) ⊓ normalizer (↑K : Set G)) (normalizer (↑(H ⊓ K) : Set G))

Tactic:
fun _ h g ↦ and_congr (h.1 g) (h.2 g)

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, and_congr
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
h : ∀ (a : Subgroup G), a < ⊤ → a < normalizer (↑a : Set G) ↔ normalizer (↑a : Set G) = a → a = ⊤
⊢ NormalizerCondition G ↔ ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
⊢ H < ⊤ → H < normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤

Tactic:
simp only [lt_iff_le_and_ne, le_normalizer, Ne]

Premises used: lt_iff_le_and_ne, Ne, Subgroup.le_normalizer
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : (H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)) → normalizer (↑H : Set G) = H → H = ⊤
h₁ : (normalizer (↑H : Set G) = H → H = ⊤) → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₂ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₃ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₄ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₅ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₆ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₇ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₈ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₉ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₀ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₁ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₂ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
h₁₃ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
h₁₄ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₅ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₁₆ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₇ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₁₈ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₉ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₂₀ h₂₁ h₂₂ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₂₃ h₂₄ h₂₅ : ¬normalizer (↑H : Set G) = H → H = normalizer (↑H : Set G) → H ≤ ⊤ → ¬H = ⊤ → False
h₂₆ : H = ⊤ → H = normalizer (↑H : Set G) → H ≤ ⊤ → ¬H = ⊤ → False
h₂₇ h₂₈ h₂₉ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₃₀ h₃₁ h₃₂ : normalizer (↑H : Set G) = H → H = ⊤ → H = ⊤
h₃₃ h₃₄ h₃₅ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₃₆ h₃₇ h₃₈ : ¬normalizer (↑H : Set G) = H → H = normalizer (↑H : Set G) → H ≤ ⊤ → ¬H = ⊤ → False
h₃₉ h₄₀ h₄₁ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₄₂ h₄₃ h₄₄ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₄₅ h₄₆ h₄₇ : ¬normalizer (↑H : Set G) = H → H = normalizer (↑H : Set G) → H ≤ ⊤ → ¬H = ⊤ → False
h₄₈ h₄₉ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₅₀ h₅₁ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₅₂ h₅₃ : ¬normalizer (↑H : Set G) = H → H = normalizer (↑H : Set G) → H ≤ ⊤ → ¬H = ⊤ → False
⊢ H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤

Tactic:
tauto
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
x : G
rw : (∃ (i : G) (_ : i ∈ s), x ∈ conjugatesOf i) ↔ ∃ a ∈ s, IsConj a x
⊢ x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x

Tactic:
rw [conjugatesOfSet, Set.mem_iUnion₂]

Premises used: Set.mem_iUnion₂, Group.conjugatesOfSet
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
x : G
⊢ (∃ (i : G) (_ : i ∈ s), x ∈ conjugatesOf i) ↔ ∃ a ∈ s, IsConj a x

Tactic:
simp only [conjugatesOf, isConj_iff, Set.mem_setOf_eq, exists_prop]

Premises used: isConj_iff, conjugatesOf, Set.mem_setOf_eq, exists_prop
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ s ⊆ conjugatesOfSet s

Tactic:
fun (x : G) (h : x ∈ s) =>
  mem_conjugatesOfSet_iff.2 ⟨x, h, IsConj.refl _⟩

Premises used: Iff.mpr, Set.Subset, Group.mem_conjugatesOfSet_iff, And.intro, IsConj.refl, Exists.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s t : Set G
h : s ⊆ t
⊢ conjugatesOfSet s ⊆ conjugatesOfSet t

Tactic:
Set.biUnion_subset_biUnion_left h

Premises used: Group.conjugatesOfSet, Set.biUnion_subset_biUnion_left
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
tn : N.Normal
a_1 : G
h : a_1 ∈ N
a : G
hc : a ∈ conjugatesOf a_1
obtain : ∀ (c : G) (hc : c * a_1 * c⁻¹ ∈ conjugatesOf a_1), c * a_1 * c⁻¹ ∈ (↑N : Set G)
⊢ a ∈ (↑N : Set G)

Tactic:
obtain ⟨c, rfl⟩ := isConj_iff.1 hc

Premises used: isConj_iff, Iff.mp, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
tn : N.Normal
a : G
h : a ∈ N
c : G
hc : c * a * c⁻¹ ∈ conjugatesOf a
⊢ c * a * c⁻¹ ∈ (↑N : Set G)

Tactic:
tn.conj_mem a h c

Premises used: Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
tn : N.Normal
a : G
h : a ∈ N
c : G
hc : c * a * c⁻¹ ∈ conjugatesOf a
⊢ c * a * c⁻¹ ∈ (↑N : Set G)

Tactic:
exact tn.conj_mem a h c

Premises used: Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
⊢ conjugatesOfSet s ⊆ (↑N : Set G)

Tactic:
Set.iUnion₂_subset fun _x H => conjugates_subset_normal (h H)

Premises used: Set.iUnion₂_subset, Group.conjugates_subset_normal, Group.conjugatesOfSet
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
rcases : ∀ (a : G) (h₁ : a ∈ s) (h₂ : IsConj a x), c * x * c⁻¹ ∈ conjugatesOfSet s
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s

Tactic:
rcases mem_conjugatesOfSet_iff.1 H with ⟨a, h₁, h₂⟩

Premises used: Group.mem_conjugatesOfSet_iff, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
a : G
h₁ : a ∈ s
h₂ : IsConj a x
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s

Tactic:
mem_conjugatesOfSet_iff.2 ⟨a, h₁, h₂.trans (isConj_iff.2 ⟨c, rfl⟩)⟩

Premises used: Iff.mpr, isConj_iff, IsConj.trans, Group.mem_conjugatesOfSet_iff, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
a : G
h₁ : a ∈ s
h₂ : IsConj a x
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s

Tactic:
exact mem_conjugatesOfSet_iff.2 ⟨a, h₁, h₂.trans (isConj_iff.2 ⟨c, rfl⟩)⟩

Premises used: Iff.mpr, isConj_iff, IsConj.trans, Group.mem_conjugatesOfSet_iff, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ conjugatesOfSet s ⊆ (↑(normalClosure s) : Set G)

Tactic:
subset_closure

Premises used: Subgroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ s ⊆ (↑(normalClosure s) : Set G)

Tactic:
Set.Subset.trans subset_conjugatesOfSet conjugatesOfSet_subset_normalClosure

Premises used: Subgroup.conjugatesOfSet_subset_normalClosure, Set.Subset.trans, Group.subset_conjugatesOfSet
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H ≤ normalClosure (↑H : Set G)

Tactic:
fun _ h =>
  subset_normalClosure h

Premises used: Subgroup.subset_normalClosure
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g : G
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * n * g⁻¹)

Tactic:
Subgroup.closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_)
      (fun x _ ihx => ?_) h

Premises used: Subgroup.closure_induction
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g : G
refine_1 : ∀ (x : G) (hx : x ∈ conjugatesOfSet s), Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
refine_2 : Membership.mem (γ := Subgroup G) (normalClosure s) (g * 1 * g⁻¹)
refine_3 :
  ∀ (x y : G),
    Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x →
      Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y →
        ∀ (ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹))
          (ihy : Membership.mem (γ := Subgroup G) (normalClosure s) (g * y * g⁻¹)),
          Membership.mem (γ := Subgroup G) (normalClosure s) (g * (x * y) * g⁻¹)
refine_4 :
  ∀ (x : G),
    Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x →
      ∀ (ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)),
        Membership.mem (γ := Subgroup G) (normalClosure s) (g * x⁻¹ * g⁻¹)
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * n * g⁻¹)

Tactic:
refine Subgroup.closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_)
      (fun x _ ihx => ?_) h
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g x : G
hx : x ∈ conjugatesOfSet s
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)

Tactic:
conjugatesOfSet_subset_normalClosure (conj_mem_conjugatesOfSet hx)

Premises used: Subgroup.conjugatesOfSet_subset_normalClosure, Group.conj_mem_conjugatesOfSet
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g x : G
hx : x ∈ conjugatesOfSet s
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)

Tactic:
exact conjugatesOfSet_subset_normalClosure (conj_mem_conjugatesOfSet hx)

Premises used: Subgroup.conjugatesOfSet_subset_normalClosure, Group.conj_mem_conjugatesOfSet
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g : G
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * 1 * g⁻¹)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g x y : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
h_2 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y
ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
ihy : Membership.mem (γ := Subgroup G) (normalClosure s) (g * y * g⁻¹)
refine_3 : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹ * (g * y * g⁻¹))
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * (x * y) * g⁻¹)

Tactic:
rw [← conj_mul]

Premises used: conj_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g x y : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
h_2 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y
ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
ihy : Membership.mem (γ := Subgroup G) (normalClosure s) (g * y * g⁻¹)
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹ * (g * y * g⁻¹))

Tactic:
mul_mem ihx ihy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g x y : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
h_2 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y
ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
ihy : Membership.mem (γ := Subgroup G) (normalClosure s) (g * y * g⁻¹)
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹ * (g * y * g⁻¹))

Tactic:
exact mul_mem ihx ihy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g x : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
refine_4 : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)⁻¹
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * x⁻¹ * g⁻¹)

Tactic:
rw [← conj_inv]

Premises used: conj_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g x : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)⁻¹

Tactic:
inv_mem ihx

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g x : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)⁻¹

Tactic:
exact inv_mem ihx

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
⊢ a ∈ N

Tactic:
closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w

Premises used: Subgroup.closure_induction
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
refine_1 : ∀ (x : G) (hx : x ∈ conjugatesOfSet s), x ∈ N
refine_2 : 1 ∈ N
refine_3 :
  ∀ (x y : G),
    Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x →
      Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y → ∀ (ihx : x ∈ N) (ihy : y ∈ N), x * y ∈ N
refine_4 : ∀ (x : G), Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x → ∀ (ihx : x ∈ N), x⁻¹ ∈ N
⊢ a ∈ N

Tactic:
refine closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ N

Tactic:
conjugatesOfSet_subset h hx

Premises used: Group.conjugatesOfSet_subset
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ N

Tactic:
exact conjugatesOfSet_subset h hx

Premises used: Group.conjugatesOfSet_subset
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
⊢ 1 ∈ N

Tactic:
one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
⊢ 1 ∈ N

Tactic:
exact one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
x y : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
h_2 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

Tactic:
mul_mem ihx ihy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
x y : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
h_2 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

Tactic:
exact mul_mem ihx ihy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
x : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
ihx : x ∈ N
⊢ x⁻¹ ∈ N

Tactic:
inv_mem ihx

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
x : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
ihx : x ∈ N
⊢ x⁻¹ ∈ N

Tactic:
exact inv_mem ihx

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
⊢ s ⊆ (↑N : Set G) ↔ normalClosure s ≤ N

Tactic:
⟨normalClosure_le_normal, Set.Subset.trans subset_normalClosure⟩

Premises used: Set.Subset.trans, Iff.intro, Subgroup.normalClosure_le_normal, Subgroup.subset_normalClosure
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
rw : LE.le (α := Subgroup G) (normalClosure s) ⊥ ↔ s ⊆ {1}
rw₁ : s ⊆ (↑⊥ : Set G) ↔ s ⊆ {1}
rw₂ rw₃ : s ⊆ {1} ↔ s ⊆ {1}
⊢ Eq (α := Subgroup G) (normalClosure s) ⊥ ↔ s ⊆ {1}

Tactic:
rw [eq_bot_iff, ← normalClosure_subset_iff, coe_bot]

Premises used: Subgroup.normalClosure_subset_iff, eq_bot_iff, Subgroup.coe_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s t : Set G
h : s ⊆ t
⊢ LE.le (α := Subgroup G) (normalClosure s) (normalClosure t)

Tactic:
normalClosure_le_normal (Set.Subset.trans h subset_normalClosure)

Premises used: Set.Subset.trans, Subgroup.normalClosure_le_normal, Subgroup.subset_normalClosure