awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Actions
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : SMul α β
inst_2 : MulAction G α
inst_3 : MulAction G β
inst_4 : IsScalarTower G α β
S : Subgroup G
⊢ IsScalarTower.{u_1, u_2, u_3} (↥S) α β

Tactic:
inferInstanceAs (IsScalarTower S.toSubmonoid α β)

Premises used: _private.0.Subgroup.instIsScalarTowerSubtypeMem._proof_1
-- Module: Mathlib.Algebra.Group.Subgroup.Actions
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : FaithfulSMul G α
S : Subgroup G
⊢ FaithfulSMul.{u_1, u_2} (↥S) α

Tactic:
inferInstanceAs (FaithfulSMul S.toSubmonoid α)

Premises used: _private.0.Subgroup.instFaithfulSMulSubtypeMem._proof_1
-- Module: Mathlib.Algebra.Group.Subgroup.Actions
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
⊢ SMulCommClass (↥(center G)) G G

Tactic:
Submonoid.center.smulCommClass_left

Premises used: Set.Mem, Subgroup.center, Submonoid.center.smulCommClass_left, Submonoid.center
-- Module: Mathlib.Algebra.Group.Subgroup.Actions
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
⊢ SMulCommClass G (↥(center G)) G

Tactic:
Submonoid.center.smulCommClass_right

Premises used: Set.Mem, Subgroup.center, Submonoid.center.smulCommClass_right, Submonoid.center
-- Module: Mathlib.Algebra.Group.Subgroup.Actions
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulZeroOneClass M
inst_1 : MulZeroOneClass N
inst_2 : MulZeroOneClass P
g : N →*₀ P
f : M →*₀ N
⊢ Eq (α := Submonoid M) (Submonoid.comap f (mker g)) (mker (g.comp f))

Tactic:
rfl

Premises used: MonoidHom.mker, Set.Mem, setOf, MonoidWithZeroHom.comp, Submonoid.comap, Set.preimage, Set.singleton, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
S : Type u_6
H : S
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
a b : G
⊢ a / b ∈ H ↔ b / a ∈ H

Tactic:
inv_div b a ▸ inv_mem_iff

Premises used: Set.Mem, Eq.rec, inv_mem_iff, inv_div
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
⊢ a / b ∈ H ↔ b / a ∈ H

Tactic:
div_mem_comm_iff

Premises used: div_mem_comm_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
K : Subgroup N
⊢ (↑(H.prod K) : Set (G × N)) = (↑H : Set G) ×ˢ (↑K : Set N)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
K : Subgroup N
p : G × N
⊢ p ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.prod
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
⊢ Relator.LiftFun (γ := Subgroup N → Subgroup (G × N)) (δ := Subgroup N → Subgroup (G × N))
    (fun (x1 x2 : Subgroup G) ↦ x1 ≤ x2)
    ((fun (x1 x2 : Subgroup N) ↦ x1 ≤ x2) ⇒ fun (x1 x2 : Subgroup (G × N)) ↦ x1 ≤ x2) prod prod

Tactic:
fun _s _s' hs _t _t' ht => Set.prod_mono hs ht

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, Set.prod_mono, Relator.LiftFun
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
K : Subgroup G
⊢ Monotone (β := Subgroup (G × N)) fun (t : Subgroup N) ↦ K.prod t

Tactic:
prod_mono (le_refl K)

Premises used: le_refl, Set.Mem, Monotone, Subgroup.prod_mono
-- 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
⊢ Monotone (β := Subgroup (G × N)) fun (K : Subgroup G) ↦ K.prod H

Tactic:
fun _ _ hs =>
  prod_mono hs (le_refl H)

Premises used: le_refl, Set.Mem, Monotone, Subgroup.prod_mono
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
K : Subgroup G
x : G × N
⊢ Membership.mem (γ := Subgroup (G × N)) (K.prod ⊤) x ↔
    Membership.mem (γ := Subgroup (G × N)) (comap (MonoidHom.fst G N) K) x

Tactic:
simp [mem_prod, MonoidHom.coe_fst]

Premises used: MonoidHom.coe_fst, Subgroup.mem_prod
-- 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
x : G × N
⊢ Membership.mem (γ := Subgroup (G × N)) (prod ⊤ H) x ↔
    Membership.mem (γ := Subgroup (G × N)) (comap (MonoidHom.snd G N) H) x

Tactic:
simp [mem_prod, MonoidHom.coe_snd]

Premises used: MonoidHom.coe_snd, Subgroup.mem_prod
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
⊢ Eq (α := Subgroup (G × N)) (prod ⊤ ⊤) ⊤

Tactic:
(top_prod _).trans <| comap_top _

Premises used: Subgroup.top_prod, Subgroup.comap_top, Eq.trans
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
⊢ (↑(prod ⊥ ⊥) : Set (G × N)) = (↑⊥ : Set (G × N))

Tactic:
simp [coe_prod]

Premises used: Subgroup.coe_prod
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
K : Subgroup N
J : Subgroup (G × N)
⊢ J ≤ H.prod K ↔ map (MonoidHom.fst G N) J ≤ H ∧ map (MonoidHom.snd G N) J ≤ K

Tactic:
simpa only [← Subgroup.toSubmonoid_le] using Submonoid.le_prod_iff

Premises used: Subgroup.toSubmonoid_le, Submonoid.le_prod_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
K : Subgroup N
J : Subgroup (G × N)
⊢ H.prod K ≤ J ↔ map (MonoidHom.inl G N) H ≤ J ∧ map (MonoidHom.inr G N) K ≤ J

Tactic:
simpa only [← Subgroup.toSubmonoid_le] using Submonoid.prod_le_iff

Premises used: Subgroup.toSubmonoid_le, Submonoid.prod_le_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
K : Subgroup N
⊢ H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥

Tactic:
simpa only [← Subgroup.toSubmonoid_inj] using Submonoid.prod_eq_bot_iff

Premises used: Submonoid.prod_eq_bot_iff, Subgroup.toSubmonoid_inj
-- 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
t : Set N
hs : 1 ∈ s
ht : 1 ∈ t
⊢ Eq (α := Subgroup (G × N)) (closure (s ×ˢ t)) (prod (closure s) (closure t))

Tactic:
le_antisymm
    (closure_le _ |>.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, subset_closure⟩)
    (prod_le_iff.2 ⟨
      map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _x hx => subset_closure ⟨hx, ht⟩,
      map_le_iff_le_comap.2 <| closure_le _ |>.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)

Premises used: Iff.mpr, Set.prod_subset_prod_iff, Subgroup.closure_le, Subgroup.subset_closure, le_antisymm, Subgroup.prod_le_iff, Subgroup.map_le_iff_le_comap, And.intro, Or.inl
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
η : Type u_7
f : η → Type u_8
inst : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
⊢ (↑(pi (f := f) I H) : Set ((i : η) → f i)) = I.pi (α := f) fun (i : η) ↦ (↑(H i) : Set (f i))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.pi, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
η : Type u_7
f : η → Type u_8
inst : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
p : (i : η) → f i
⊢ p ∈ pi (f := f) I H ↔ ∀ i ∈ I, p i ∈ H i

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.pi
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
η : Type u_7
f : η → Type u_8
inst : (i : η) → Group (f i)
I : Set η
x : (i : η) → f i
⊢ Membership.mem (γ := Subgroup ((i : η) → f i)) (pi (f := f) I fun (i : η) ↦ ⊤) x ↔
    Membership.mem (γ := Subgroup ((i : η) → f i)) ⊤ x

Tactic:
simp [mem_pi]

Premises used: Subgroup.mem_pi
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
η : Type u_7
f : η → Type u_8
inst : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
x : (i : η) → f i
⊢ x ∈ pi (f := f) ∅ H ↔ Membership.mem (γ := Subgroup ((i : η) → f i)) ⊤ x

Tactic:
simp [mem_pi]

Premises used: Subgroup.mem_pi
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
η : Type u_7
f : η → Type u_8
inst : (i : η) → Group (f i)
x : (i : η) → f i
⊢ Membership.mem (γ := Subgroup ((i : η) → f i)) (pi (f := f) univ fun (i : η) ↦ ⊥) x ↔
    Membership.mem (γ := Subgroup ((i : η) → f i)) ⊥ x

Tactic:
simp [mem_pi, funext_iff]

Premises used: funext_iff, Subgroup.mem_pi
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
η : Type u_7
f : η → Type u_8
inst : (i : η) → Group (f i)
I : Set η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ J ≤ pi (f := f) I H ↔ ∀ i ∈ I, J ≤ comap (Pi.evalMonoidHom f i) (H i)

Tactic:
Set.subset_pi_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.pi, Set.subset_pi_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
η : Type u_7
f : η → Type u_8
inst : (i : η) → Group (f i)
inst_1 : DecidableEq η
I : Set η
H : (i : η) → Subgroup (f i)
i : η
x : f i
⊢ Pi.mulSingle (M := f) i x ∈ pi (f := f) I H ↔ i ∈ I → x ∈ H i

Tactic:
Set.update_mem_pi_iff_of_mem (one_mem (pi I H))

Premises used: Set.Mem, setOf, Set.update_mem_pi_iff_of_mem, Set.pi, OneMemClass.one_mem, Subgroup.pi, Pi.mulSingle
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
η : Type u_7
f : η → Type u_8
inst : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
simp_rw :
  (↑(pi (f := f) univ H) : Set ((i : η) → f i)) = (↑⊥ : Set ((i : η) → f i)) ↔
    ∀ (i : η), (↑(H i) : Set (f i)) = (↑⊥ : Set (f i))
⊢ pi (f := f) univ H = ⊥ ↔ ∀ (i : η), H i = ⊥

Tactic:
simp_rw [SetLike.ext'_iff]

Premises used: SetLike.ext'_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
η : Type u_7
f : η → Type u_8
inst : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (↑(pi (f := f) univ H) : Set ((i : η) → f i)) = (↑⊥ : Set ((i : η) → f i)) ↔
    ∀ (i : η), (↑(H i) : Set (f i)) = (↑⊥ : Set (f i))

Tactic:
Set.univ_pi_eq_singleton_iff

Premises used: setOf, Set.singleton, Set.univ_pi_eq_singleton_iff, Set.pi
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
η : Type u_7
f : η → Type u_8
inst : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ (↑(pi (f := f) univ H) : Set ((i : η) → f i)) = (↑⊥ : Set ((i : η) → f i)) ↔
    ∀ (i : η), (↑(H i) : Set (f i)) = (↑⊥ : Set (f i))

Tactic:
exact Set.univ_pi_eq_singleton_iff

Premises used: Set.univ_pi_eq_singleton_iff
-- 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
k : Set G
N : Type u_5
inst_4 : Group N
P : Type u_6
inst_5 : Group P
inst_6 : IsMulTorsionFree G
n : ℕ
hn : n ≠ 0
a b : ↥H
⊢ Eq.{u_1 + 1} (α := G) ((fun (a : G) ↦ a ^ n) (↑a : G)) ((fun (a : G) ↦ a ^ n) (↑b : G)) → (↑a : G) = (↑b : G)

Tactic:
have := pow_left_injective hn (M := G) (a₁ := a) (a₂ := b)
-- 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
k : Set G
N : Type u_5
inst_4 : Group N
P : Type u_6
inst_5 : Group P
inst_6 : IsMulTorsionFree G
n : ℕ
hn : ¬n = 0
a b : ↥H
this : (↑a : G) ^ n = (↑b : G) ^ n → (↑a : G) = (↑b : G)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ∀ (this : a ^ n = b ^ n → a = b), a ^ n = b ^ n → a = b
⊢ a ^ n = b ^ n → a = b

Tactic:
norm_cast at this
-- 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
h : H.Characteristic
⊢ H.Normal

Tactic:
⟨fun a ha b => (SetLike.ext_iff.mp (h.fixed (MulAut.conj b)) a).mpr ha⟩

Premises used: Iff.mpr, Subgroup.Characteristic.fixed, SetLike.ext_iff, MulAut.conj, Subgroup.Normal.mk, Iff.mp, DFunLike.coe
-- 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 : AddSubgroup A
h : H.Characteristic
⊢ H.Normal

Tactic:
⟨fun a ha b => (SetLike.ext_iff.mp (h.fixed (AddAut.conj b)) a).mpr ha⟩

Premises used: Iff.mpr, SetLike.ext_iff, AddSubgroup.Characteristic.fixed, Iff.mp, AddSubgroup.Normal.mk, DFunLike.coe, AddAut.conj
-- 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 : G), Membership.mem (γ := Subgroup G) ⊥ n → ∀ (g : G), Membership.mem (γ := Subgroup G) ⊥ (g * n * g⁻¹)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.toMonoidHom H = H

Tactic:
⟨Characteristic.fixed, Characteristic.mk⟩

Premises used: Subgroup.Characteristic.fixed, Subgroup.Characteristic.mk, Iff.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.toMonoidHom H ≤ H

Tactic:
characteristic_iff_comap_eq.trans
    ⟨fun h ϕ => le_of_eq (h ϕ), fun h ϕ =>
      le_antisymm (h ϕ) fun g hg => h ϕ.symm ((congr_arg (· ∈ H) (ϕ.symm_apply_apply g)).mpr hg)⟩

Premises used: Eq.mpr, Subgroup.characteristic_iff_comap_eq, Membership.mem, congr_arg, le_antisymm, Iff.intro, Iff.trans, le_of_eq, MulEquiv.symm, MulEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ comap ϕ.toMonoidHom H

Tactic:
characteristic_iff_comap_eq.trans
    ⟨fun h ϕ => ge_of_eq (h ϕ), fun h ϕ =>
      le_antisymm (fun g hg => (congr_arg (· ∈ H) (ϕ.symm_apply_apply g)).mp (h ϕ.symm hg)) (h ϕ)⟩

Premises used: Subgroup.characteristic_iff_comap_eq, ge_of_eq, Membership.mem, Eq.mp, congr_arg, le_antisymm, Iff.intro, Iff.trans, MulEquiv.symm, MulEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
simp_rw : H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H = H
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H = H

Tactic:
simp_rw [map_equiv_eq_comap_symm']

Premises used: Subgroup.map_equiv_eq_comap_symm'
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H = H

Tactic:
characteristic_iff_comap_eq.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

Premises used: Subgroup.characteristic_iff_comap_eq, Iff.intro, Iff.trans, MulEquiv.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H = H

Tactic:
exact characteristic_iff_comap_eq.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

Premises used: Subgroup.characteristic_iff_comap_eq, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
simp_rw : H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H ≤ H
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H ≤ H

Tactic:
simp_rw [map_equiv_eq_comap_symm']

Premises used: Subgroup.map_equiv_eq_comap_symm'
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H ≤ H

Tactic:
characteristic_iff_comap_le.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

Premises used: Subgroup.characteristic_iff_comap_le, Iff.intro, Iff.trans, MulEquiv.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H ≤ H

Tactic:
exact characteristic_iff_comap_le.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

Premises used: Subgroup.characteristic_iff_comap_le, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
simp_rw : H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ comap ϕ.symm.toMonoidHom H
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ map ϕ.toMonoidHom H

Tactic:
simp_rw [map_equiv_eq_comap_symm']

Premises used: Subgroup.map_equiv_eq_comap_symm'
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ comap ϕ.symm.toMonoidHom H

Tactic:
characteristic_iff_le_comap.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

Premises used: Subgroup.characteristic_iff_le_comap, Iff.intro, Iff.trans, MulEquiv.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ comap ϕ.symm.toMonoidHom H

Tactic:
exact characteristic_iff_le_comap.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

Premises used: Subgroup.characteristic_iff_le_comap, Iff.intro, Iff.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
H K : Subgroup G
⊢ Characteristic.{u_1} (G := G) ⊥

Tactic:
characteristic_iff_le_map.mpr fun _ϕ => bot_le

Premises used: Iff.mpr, bot_le, Subgroup.characteristic_iff_le_map
-- 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
⊢ Characteristic.{u_1} (G := G) ⊤

Tactic:
characteristic_iff_map_le.mpr fun _ϕ => le_top

Premises used: Iff.mpr, Subgroup.characteristic_iff_map_le, le_top
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
⊢ Eq.{u_1 + 1} (α := Subgroup G) (normalizer ∅) ⊤

Tactic:
ext fun _ ↦ ⟨fun _ ↦ trivial, fun _ _ ↦ .rfl⟩

Premises used: trivial, Iff.rfl, Iff.intro, Subgroup.ext
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : CommGroup G
s : Set G
h : ∀ (x : G), Membership.mem (γ := Subgroup G) (normalizer s) x ↔ Membership.mem (γ := Subgroup G) ⊤ x
⊢ Eq (α := Subgroup G) (normalizer s) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : CommGroup G
s : Set G
x : G
⊢ Membership.mem (γ := Subgroup G) (normalizer s) x ↔ Membership.mem (γ := Subgroup G) ⊤ x

Tactic:
simp [mem_set_normalizer_iff]

Premises used: Subgroup.mem_set_normalizer_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
simp_rw : (∀ (h : G), h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g * x_1 * g⁻¹ = x) ↔ x ∈ s
⊢ Membership.mem (γ := Subgroup G) (normalizer s) g ↔
    (⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' s = s

Tactic:
simp_rw [mem_set_normalizer_iff'', Set.ext_iff, Set.mem_image, MulAut.conj_apply]

Premises used: Subgroup.mem_set_normalizer_iff'', Set.mem_image, MulAut.conj_apply, Set.ext_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
⊢ (∀ (h : G), h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g * x_1 * g⁻¹ = x) ↔ x ∈ s

Tactic:
forall_congr' fun h ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
refine : ∀ (h : G), (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x * g⁻¹ = h) ↔ h ∈ s)
⊢ (∀ (h : G), h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g * x_1 * g⁻¹ = x) ↔ x ∈ s

Tactic:
refine forall_congr' fun h ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
g h : G
simp_rw : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x = h * g) ↔ h ∈ s)
simp_rw₁ : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, x = g⁻¹ * (h * g)) ↔ h ∈ s)
simp_rw₂ : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, x = g⁻¹ * h * g) ↔ h ∈ s)
simp_rw₃ : (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ (g⁻¹ * h * g ∈ s ↔ h ∈ s)
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x * g⁻¹ = h) ↔ h ∈ s)

Tactic:
simp_rw [mul_inv_eq_iff_eq_mul, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, exists_eq_right, iff_comm]

Premises used: mul_assoc, exists_eq_right, iff_comm, eq_inv_mul_iff_mul_eq, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g : G
simp_rw : (∀ (h : G), h ∈ s ↔ -g + h + g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g + x_1 + -g = x) ↔ x ∈ s
⊢ Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer s) g ↔
    (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
              AddAut G) :
          (a : G) → G) ''
        s =
      s

Tactic:
simp_rw [AddSubgroup.mem_set_normalizer_iff'', Set.ext_iff, Set.mem_image, AddAut.conj_apply]

Premises used: Set.mem_image, AddSubgroup.mem_set_normalizer_iff'', AddAut.conj_apply, Set.ext_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g : G
⊢ (∀ (h : G), h ∈ s ↔ -g + h + g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g + x_1 + -g = x) ↔ x ∈ s

Tactic:
forall_congr' fun h ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g : G
refine : ∀ (h : G), (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x + -g = h) ↔ h ∈ s)
⊢ (∀ (h : G), h ∈ s ↔ -g + h + g ∈ s) ↔ ∀ (x : G), (∃ x_1 ∈ s, g + x_1 + -g = x) ↔ x ∈ s

Tactic:
refine forall_congr' fun h ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g h : G
simp_rw : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x = h + g) ↔ h ∈ s)
simp_rw₁ : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, x = -g + (h + g)) ↔ h ∈ s)
simp_rw₂ : (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, x = -g + h + g) ↔ h ∈ s)
simp_rw₃ : (h ∈ s ↔ -g + h + g ∈ s) ↔ (-g + h + g ∈ s ↔ h ∈ s)
⊢ (h ∈ s ↔ -g + h + g ∈ s) ↔ ((∃ x ∈ s, g + x + -g = h) ↔ h ∈ s)

Tactic:
simp_rw [add_neg_eq_iff_eq_add, ← eq_neg_add_iff_add_eq, ← add_assoc, exists_eq_right, iff_comm]

Premises used: add_assoc, exists_eq_right, iff_comm, eq_neg_add_iff_add_eq, add_neg_eq_iff_eq_add
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
hg : Membership.mem (γ := Subgroup G) (normalizer s) g
⊢ (⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' s)) : Set G)

Tactic:
have : MulAut.conj g '' (closure s) = closure (MulAut.conj g '' s) :=
    congr($(MulAut.conj g |>.toMonoidHom.map_closure s))
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
g : G
hg : Membership.mem (γ := Subgroup G) (normalizer s) g
this :
  (⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' s)) : Set G)
⊢ (⇑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) = (↑(closure s) : Set G)

Tactic:
rw [mem_normalizer_iff_conj_image_eq.mp hg] at this

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

Tactic:
rwa [mem_normalizer_iff_conj_image_eq]

Premises used: Subgroup.mem_normalizer_iff_conj_image_eq
-- 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
⊢ (⇑((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)

Tactic:
have : AddAut.conj g '' (AddSubgroup.closure s) = AddSubgroup.closure (AddAut.conj g '' s) :=
    congr($(AddAut.conj g |>.toAddMonoidHom.map_closure s))