awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
simp_rw :
  h =
    (f.liftOfRightInverse f_inv hf : (a : { g : G₁ →* G₃ // f.ker ≤ g.ker }) → G₂ →* G₃)
      (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (h.comp f) ⋯)
⊢ h =
    (f.liftOfRightInverse f_inv hf : (a : { g : G₁ →* G₃ // f.ker ≤ g.ker }) → G₂ →* G₃)
      (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) g hg)

Tactic:
simp_rw [← hh]
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h =
    (f.liftOfRightInverse f_inv hf : (a : { g : G₁ →* G₃ // f.ker ≤ g.ker }) → G₂ →* G₃)
      (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (h.comp f) ⋯)

Tactic:
((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm

Premises used: Equiv.apply_symm_apply, MonoidHom.liftOfRightInverse, Eq.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h =
    (f.liftOfRightInverse f_inv hf : (a : { g : G₁ →* G₃ // f.ker ≤ g.ker }) → G₂ →* G₃)
      (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (h.comp f) ⋯)

Tactic:
exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm

Premises used: Equiv.apply_symm_apply, MonoidHom.liftOfRightInverse, Eq.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup N
hH : H.Normal
f : G →* N
x : G
⊢ x ∈ Subgroup.comap f H → ∀ (g : G), g * x * g⁻¹ ∈ Subgroup.comap f H

Tactic:
simp +contextual [Subgroup.mem_comap, hH.conj_mem]

Premises used: Subgroup.mem_comap, Subgroup.Normal.conj_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
N : Type u_5
inst_4 : Group N
H : Subgroup N
nH : H.Normal
f : G →* N
⊢ (comap f H).Normal

Tactic:
nH.comap _

Premises used: Subgroup.Normal.comap
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : H.Normal
K : Subgroup G
⊢ (H.subgroupOf K).Normal

Tactic:
hH.comap _

Premises used: Subgroup.subgroupOf, Subgroup.Normal.comap
-- 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
N_1 : Type u_5
inst_4 : Group N_1
H N : Subgroup G
inst_5 : N.Normal
⊢ (N.subgroupOf H).Normal

Tactic:
Subgroup.normal_comap _

Premises used: Subgroup.subgroupOf, Subgroup.normal_comap
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set G
f : G →* N
⊢ normalClosure s ≤ comap f (normalClosure ((⇑f : (a : G) → N) '' s))

Tactic:
simp [normalClosure_le_normal, ← Set.image_subset_iff, subset_normalClosure]

Premises used: Subgroup.normalClosure_le_normal, Subgroup.subset_normalClosure, Set.image_subset_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set G
f : G →* N
⊢ map f (normalClosure s) ≤ normalClosure ((⇑f : (a : G) → N) '' s)

Tactic:
simp [map_le_iff_le_comap, comap_normalClosure_image_ge]

Premises used: Subgroup.map_le_iff_le_comap, Subgroup.comap_normalClosure_image_ge
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set G
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ (map f (normalClosure s)).Normal

Tactic:
have : Normal (map f (normalClosure s)) := Normal.map inferInstance f hf
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set G
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
this : (map f (normalClosure s)).Normal
a : map f (normalClosure s) ≤ normalClosure ((⇑f : (a : G) → N) '' s)
a₁ : normalClosure ((⇑f : (a : G) → N) '' s) ≤ map f (normalClosure s)
⊢ map f (normalClosure s) = normalClosure ((⇑f : (a : G) → N) '' s)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set G
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) ≤ normalClosure ((⇑f : (a : G) → N) '' s)

Tactic:
map_normalClosure_le s f

Premises used: Subgroup.map_normalClosure_le
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set G
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) ≤ normalClosure ((⇑f : (a : G) → N) '' s)

Tactic:
exact map_normalClosure_le s f

Premises used: Subgroup.map_normalClosure_le
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set G
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
this : (map f (normalClosure s)).Normal
⊢ normalClosure ((⇑f : (a : G) → N) '' s) ≤ map f (normalClosure s)

Tactic:
normalClosure_le_normal (Set.image_mono subset_normalClosure)

Premises used: Set.image_mono, Subgroup.normalClosure_le_normal, Subgroup.subset_normalClosure
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set G
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
this : (map f (normalClosure s)).Normal
⊢ normalClosure ((⇑f : (a : G) → N) '' s) ≤ map f (normalClosure s)

Tactic:
exact normalClosure_le_normal (Set.image_mono subset_normalClosure)

Premises used: Subgroup.normalClosure_le_normal
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set N
f : G ≃* N
⊢ Eq.{u_1 + 1} (α := Set G) ((⇑f.symm : (a : N) → G) '' s) ((⇑f.toEquiv : (a : G) → N) ⁻¹' s)

Tactic:
have := f.toEquiv.image_symm_eq_preimage s
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set N
f : G ≃* N
this : Eq.{u_1 + 1} (α := Set G) ((⇑f.symm : (a : N) → G) '' s) ((⇑f.toEquiv : (a : G) → N) ⁻¹' s)
⊢ Eq (α := Subgroup G) (normalClosure ((⇑f : (a : G) → N) ⁻¹' s)) (comap (↑f : G →* N) (normalClosure s))

Tactic:
simp_all [comap_equiv_eq_map_symm, map_normalClosure s (f.symm : N →* G) f.symm.surjective]

Premises used: Subgroup.comap_equiv_eq_map_symm, MonoidHomClass.toMonoidHom, MulEquiv.surjective, Subgroup.map_normalClosure, MulEquiv.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_6
H : Type u_7
inst : Group G
inst_1 : Group H
φ : G →* H
hφ : Injective.{u_6 + 1, u_7 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
L : Subgroup G
n : (Subgroup.map φ L).Normal
⊢ L.Normal

Tactic:
L.comap_map_eq_self_of_injective hφ ▸ n.comap φ

Premises used: Eq.rec, Subgroup.comap_map_eq_self_of_injective, Subgroup.Normal.comap
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
L : Subgroup ↥K
n : (Subgroup.map K.subtype L).Normal
⊢ L.Normal

Tactic:
n.of_map_injective K.subtype_injective

Premises used: Subgroup.Normal.of_map_injective, Subgroup.subtype_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hHK : H ≤ K
⊢ (H.subgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k * h * k⁻¹ ∈ H

Tactic:
⟨fun hN h k hH hK => hN.conj_mem ⟨h, hHK hH⟩ hH ⟨k, hK⟩, fun hN =>
    { conj_mem := fun h hm k => hN h.1 k.1 hm k.2 }⟩

Premises used: Subtype.mk, Subgroup.Normal.mk, Iff.intro, Subtype.val, Subtype.property, Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
A B' B : Subgroup G
hN : (B'.subgroupOf B).Normal
rw : ∀ (hN : B ≤ normalizer (↑(B' ⊓ B) : Set G)), A ⊓ B ≤ normalizer (↑(A ⊓ B' ⊓ (A ⊓ B)) : Set G)
⊢ Normal (G := ↥(A ⊓ B)) ((A ⊓ B').subgroupOf (A ⊓ B))

Tactic:
rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer_inf
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
A B' B : Subgroup G
hN : B ≤ normalizer (↑(B' ⊓ B) : Set G)
rw : A ⊓ B ≤ normalizer (↑(A ⊓ (B' ⊓ B)) : Set G)
⊢ A ⊓ B ≤ normalizer (↑(A ⊓ B' ⊓ (A ⊓ B)) : Set G)

Tactic:
rw [inf_inf_inf_comm, inf_idem]

Premises used: inf_inf_inf_comm, inf_idem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
A B' B : Subgroup G
hN : B ≤ normalizer (↑(B' ⊓ B) : Set G)
⊢ A ⊓ B ≤ normalizer (↑(A ⊓ (B' ⊓ B)) : Set G)

Tactic:
le_trans (inf_le_inf A.le_normalizer hN) inf_normalizer_le_normalizer_inf

Premises used: inf_le_inf, Subgroup.le_normalizer, Subgroup.inf_normalizer_le_normalizer_inf, le_trans
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
A B' B : Subgroup G
hN : B ≤ normalizer (↑(B' ⊓ B) : Set G)
⊢ A ⊓ B ≤ normalizer (↑(A ⊓ (B' ⊓ B)) : Set G)

Tactic:
exact le_trans (inf_le_inf A.le_normalizer hN) inf_normalizer_le_normalizer_inf

Premises used: inf_le_inf, Subgroup.le_normalizer, Subgroup.inf_normalizer_le_normalizer_inf, le_trans
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
A' A B : Subgroup G
hN : (A'.subgroupOf A).Normal
rw : ∀ (hN : A ≤ normalizer (↑(A' ⊓ A) : Set G)), A ⊓ B ≤ normalizer (↑(A' ⊓ B ⊓ (A ⊓ B)) : Set G)
⊢ Normal (G := ↥(A ⊓ B)) ((A' ⊓ B).subgroupOf (A ⊓ B))

Tactic:
rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer_inf
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
A' A B : Subgroup G
hN : A ≤ normalizer (↑(A' ⊓ A) : Set G)
rw : A ⊓ B ≤ normalizer (↑(A' ⊓ A ⊓ B) : Set G)
⊢ A ⊓ B ≤ normalizer (↑(A' ⊓ B ⊓ (A ⊓ B)) : Set G)

Tactic:
rw [inf_inf_inf_comm, inf_idem]

Premises used: inf_inf_inf_comm, inf_idem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
A' A B : Subgroup G
hN : A ≤ normalizer (↑(A' ⊓ A) : Set G)
⊢ A ⊓ B ≤ normalizer (↑(A' ⊓ A ⊓ B) : Set G)

Tactic:
le_trans (inf_le_inf hN B.le_normalizer) inf_normalizer_le_normalizer_inf

Premises used: inf_le_inf, Subgroup.le_normalizer, Subgroup.inf_normalizer_le_normalizer_inf, le_trans
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
A' A B : Subgroup G
hN : A ≤ normalizer (↑(A' ⊓ A) : Set G)
⊢ A ⊓ B ≤ normalizer (↑(A' ⊓ A ⊓ B) : Set G)

Tactic:
exact le_trans (inf_le_inf hN B.le_normalizer) inf_normalizer_le_normalizer_inf

Premises used: inf_le_inf, Subgroup.le_normalizer, Subgroup.inf_normalizer_le_normalizer_inf, le_trans
-- 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
N : Type u_5
inst_4 : Group N
H K : Subgroup G
hH : H.Normal
hK : K.Normal
⊢ (H ⊓ K).Normal

Tactic:
⟨fun n hmem g => ⟨hH.conj_mem n hmem.1 g, hK.conj_mem n hmem.2 g⟩⟩

Premises used: Subgroup.Normal.mk, And.right, And.left, And.intro, Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
conj_mem : ∀ n ∈ iInf a, ∀ (g : G), g * n * g⁻¹ ∈ iInf a
⊢ (iInf a).Normal

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : g ∈ iInf a
h : G
conj_mem : ∀ (g_in_iInf : ∀ (i : ι), g ∈ a i) (h : G) (i : ι), h * g * h⁻¹ ∈ a i
⊢ h * g * h⁻¹ ∈ iInf a

Tactic:
rw [Subgroup.mem_iInf] at g_in_iInf ⊢

Premises used: Subgroup.mem_iInf
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
i : ι
⊢ h * g * h⁻¹ ∈ a i

Tactic:
(norm i).conj_mem g (g_in_iInf i) h

Premises used: Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
i : ι
⊢ h * g * h⁻¹ ∈ a i

Tactic:
exact (norm i).conj_mem g (g_in_iInf i) h

Premises used: Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
⊢ b * (a * b) * b⁻¹ ∈ H

Tactic:
have := (normal_subgroupOf_iff hK).mp hN (a * b) b h hb
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * b) * b⁻¹ ∈ H
rwa : ∀ (this : b * (a * b * b⁻¹) ∈ H), b * a ∈ H
rwa₁ : ∀ (this : b * (a * (b * b⁻¹)) ∈ H), b * a ∈ H
rwa₂ : ∀ (this : b * (a * 1) ∈ H), b * a ∈ H
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : b * a ∈ H), b * a ∈ H
⊢ b * a ∈ H

Tactic:
rwa [mul_assoc, mul_assoc, mul_inv_cancel, mul_one] at this

Premises used: mul_assoc, mul_inv_cancel, mul_one
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y * x⁻¹ * y⁻¹ = 1
⊢ x * y = (x⁻¹ * y⁻¹)⁻¹

Tactic:
rw [mul_assoc, mul_eq_one_iff_eq_inv] at this

Premises used: mul_assoc, mul_eq_one_iff_eq_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y = (x⁻¹ * y⁻¹)⁻¹
⊢ x * y = y * x

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
suffices : x * y * x⁻¹ * y⁻¹ = 1
⊢ Commute x y

Tactic:
suffices x * y * x⁻¹ * y⁻¹ = 1 by
    change x * y = y * x
    · rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
      simpa
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
a : x * y * x⁻¹ * y⁻¹ ∈ H₁ ⊓ H₂
⊢ x * y * x⁻¹ * y⁻¹ = 1

Tactic:
apply hdis.le_bot

Premises used: Disjoint.le_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
a : x * y * x⁻¹ * y⁻¹ ∈ (↑H₁.toSubmonoid : Set G)
a₁ : x * y * x⁻¹ * y⁻¹ ∈ (↑H₂.toSubmonoid : Set G)
⊢ x * y * x⁻¹ * y⁻¹ ∈ H₁ ⊓ H₂

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * (y * x⁻¹ * y⁻¹) ∈ H₁
⊢ x * y * x⁻¹ * y⁻¹ ∈ (↑H₁.toSubmonoid : Set G)

Tactic:
simpa [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
a : x * (y * x⁻¹ * y⁻¹) ∈ H₁
⊢ x * y * x⁻¹ * y⁻¹ ∈ (↑H₁.toSubmonoid : Set G)

Tactic:
suffices x * (y * x⁻¹ * y⁻¹) ∈ H₁ by simpa [mul_assoc]
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * (y * x⁻¹ * y⁻¹) ∈ H₁

Tactic:
H₁.mul_mem hx (hH₁.conj_mem _ (H₁.inv_mem hx) _)

Premises used: Subgroup.inv_mem, Subgroup.mul_mem, Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * (y * x⁻¹ * y⁻¹) ∈ H₁

Tactic:
exact H₁.mul_mem hx (hH₁.conj_mem _ (H₁.inv_mem hx) _)

Premises used: Subgroup.inv_mem, Subgroup.mul_mem, Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
apply : x * y * x⁻¹ ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ H₂

Tactic:
apply H₂.mul_mem _ (H₂.inv_mem hy)

Premises used: Subgroup.inv_mem, Subgroup.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ ∈ H₂

Tactic:
apply hH₂.conj_mem _ hy

Premises used: Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
rw : H ≤ normalizer (↑(N ⊓ H) : Set G)
⊢ (N.subgroupOf H).Normal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer_inf]

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer_inf
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
⊢ H ≤ normalizer (↑(N ⊓ H) : Set G)

Tactic:
(le_inf hLE H.le_normalizer).trans inf_normalizer_le_normalizer_inf

Premises used: Subgroup.le_normalizer, le_inf, LE.le.trans, Subgroup.inf_normalizer_le_normalizer_inf
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
⊢ H ≤ normalizer (↑(N ⊓ H) : Set G)

Tactic:
exact (le_inf hLE H.le_normalizer).trans inf_normalizer_le_normalizer_inf

Premises used: Subgroup.le_normalizer, le_inf, LE.le.trans, Subgroup.inf_normalizer_le_normalizer_inf
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
rw : H ⊔ N ≤ normalizer (↑N : Set G)
⊢ Normal (G := ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N))

Tactic:
rw [normal_subgroupOf_iff_le_normalizer le_sup_right]

Premises used: le_sup_right, Subgroup.normal_subgroupOf_iff_le_normalizer
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
⊢ H ⊔ N ≤ normalizer (↑N : Set G)

Tactic:
sup_le hLE le_normalizer

Premises used: Subgroup.le_normalizer, sup_le
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
⊢ H ⊔ N ≤ normalizer (↑N : Set G)

Tactic:
exact sup_le hLE le_normalizer

Premises used: Subgroup.le_normalizer, sup_le
-- 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
N : Type u_5
inst_4 : Group N
s : Set G
⊢ Normal (G := ↥(normalizer s)) (subgroupOf (closure s) (normalizer s))

Tactic:
normal_subgroupOf_of_le_normalizer <| normalizer_le_normalizer_closure s

Premises used: Subgroup.normal_subgroupOf_of_le_normalizer, Subgroup.normalizer_le_normalizer_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g g' : G
hg : g ∈ N
hg' : g' ∈ N
hc : IsConj g g'
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
obtain :
  ∀ (c : G) {hg' : c * g * c⁻¹ ∈ N} (hc : IsConj g (c * g * c⁻¹)),
    Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}) ⊤
⊢ Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g' hg'}) ⊤

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
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
x : G
hx : x ∈ N
⊢ Membership.mem (α := G) N
    ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G)
        (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ N) x hx) : G) :
      G)

Tactic:
hn.conj_mem _ hx c

Premises used: Set.Mem, Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
x : G
hx : x ∈ N
⊢ Membership.mem (α := G) N
    ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G)
        (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ N) x hx) : G) :
      G)

Tactic:
exact hn.conj_mem _ hx c

Premises used: Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
⊢ ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)

Tactic:
have h : ∀ x : N, (MulAut.conj c) x ∈ N := by
    rintro ⟨x, hx⟩
    exact hn.conj_mem _ hx c
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
⊢ ∃ (a : ↥N),
    (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h :
          (a : ↥N) → ↥N)
        a =
      Subtype.mk (p := fun (x : G) ↦ x ∈ N) x hx

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

Premises used: HMul.hMul, Subtype.mk, Inv.inv, Exists.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
refine_1 : c⁻¹ * x * c ∈ N
refine_2 :
  (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h :
        (a : ↥N) → ↥N)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c⁻¹ * x * c) ⋯) =
    Subtype.mk (p := fun (x : G) ↦ x ∈ N) x hx
⊢ ∃ (a : ↥N),
    (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h :
          (a : ↥N) → ↥N)
        a =
      Subtype.mk (p := fun (x : G) ↦ x ∈ N) x hx

Tactic:
refine ⟨⟨c⁻¹ * x * c, ?_⟩, ?_⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
⊢ c⁻¹ * x * c⁻¹⁻¹ ∈ N

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