awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst : Group G
inst_1 : AddGroup A
s : Set G
inst_2 : Monoid α
inst_3 : MulDistribMulAction α G
inst_4 : MulDistribMulAction.{u_1, u_2} αᵐᵒᵖ G
inst_5 : IsCentralScalar α G
⊢ IsCentralScalar.{u_1, u_2} α (Subgroup G)

Tactic:
⟨fun _ S => (congr_arg fun f => S.map f) <| MonoidHom.ext <| op_smul_eq_smul _⟩

Premises used: Subgroup.map, MonoidHom.ext, congr_arg, IsCentralScalar.mk, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Group α
inst_2 : MulDistribMulAction α G
a : α
S : Subgroup G
x : G
⊢ a • x ∈ a • S ↔ x ∈ S

Tactic:
smul_mem_smul_set_iff

Premises used: Set.Mem, Set.smul_mem_smul_set_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Group α
inst_2 : MulDistribMulAction α G
a : α
S : Subgroup G
x : G
⊢ x ∈ a • S ↔ a⁻¹ • x ∈ S

Tactic:
mem_smul_set_iff_inv_smul_mem

Premises used: Set.Mem, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Group α
inst_2 : MulDistribMulAction α G
a : α
S : Subgroup G
x : G
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
mem_inv_smul_set_iff

Premises used: Set.Mem, Set.mem_inv_smul_set_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Group α
inst_2 : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ a • S ≤ a • T ↔ S ≤ T

Tactic:
smul_set_subset_smul_set_iff

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_smul_set_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Group α
inst_2 : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ a • S ≤ T ↔ S ≤ a⁻¹ • T

Tactic:
smul_set_subset_iff_subset_inv_smul_set

Premises used: Set.Mem, Set.Subset, Set.smul_set_subset_iff_subset_inv_smul_set
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Group α
inst_2 : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ S ≤ a • T ↔ a⁻¹ • S ≤ T

Tactic:
subset_smul_set_iff

Premises used: Set.Mem, Set.subset_smul_set_iff, Set.Subset
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
g : G
hg : g ∈ (↑P : Set G)
⊢ Membership.mem (α := G) H
    ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
              ((MulAut.conj : (a : G) → MulAut G) (↑h : G)) :
            Monoid.End G) :
          (a : G) → G)
        g :
      G)

Tactic:
H.mul_mem (H.mul_mem h.2 (hP hg)) (H.inv_mem h.2)

Premises used: Set.Mem, Subgroup.inv_mem, Subgroup.mul_mem, Subtype.property
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
g : G
hg : g ∈ (↑P : Set G)
⊢ Membership.mem (α := G) H
    ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
              ((MulAut.conj : (a : G) → MulAut G) (↑h : G)) :
            Monoid.End G) :
          (a : G) → G)
        g :
      G)

Tactic:
exact H.mul_mem (H.mul_mem h.2 (hP hg)) (H.inv_mem h.2)

Premises used: Subgroup.inv_mem, Subgroup.mul_mem, Subtype.property
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H = H

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
refine_1 : HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H ≤ H
refine_2 : H ≤ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H
⊢ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H = H

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H ≤ H

Tactic:
(conj_smul_le_of_le (le_refl H) ⟨h, hh⟩)

Premises used: le_refl, Set.Mem, Subtype.mk, Subgroup.conj_smul_le_of_le
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H ≤ H

Tactic:
exact (conj_smul_le_of_le (le_refl H) ⟨h, hh⟩)

Premises used: le_refl, Subtype.mk, Subgroup.conj_smul_le_of_le
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
refine_2 : HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h⁻¹ : MulAut G) H ≤ H
⊢ H ≤ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H

Tactic:
rw [subset_pointwise_smul_iff, ← map_inv]

Premises used: Subgroup.subset_pointwise_smul_iff, map_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h⁻¹ : MulAut G) H ≤ H

Tactic:
conj_smul_le_of_le (le_refl H) ⟨h⁻¹, H.inv_mem hh⟩

Premises used: le_refl, Set.Mem, Subtype.mk, Subgroup.conj_smul_le_of_le, Inv.inv, Subgroup.inv_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h⁻¹ : MulAut G) H ≤ H

Tactic:
exact conj_smul_le_of_le (le_refl H) ⟨h⁻¹, H.inv_mem hh⟩

Premises used: le_refl, Subtype.mk, Subgroup.conj_smul_le_of_le, Inv.inv, Subgroup.inv_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ HSMul.hSMul (α := MulAut ↥H) ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H) (P.subgroupOf H) =
    (HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) (↑h : G) : MulAut G) P).subgroupOf H

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
refine_1 :
  HSMul.hSMul (α := MulAut ↥H) ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H) (P.subgroupOf H) ≤
    (HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) (↑h : G) : MulAut G) P).subgroupOf H
refine_2 :
  (HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) (↑h : G) : MulAut G) P).subgroupOf H ≤
    HSMul.hSMul (α := MulAut ↥H) ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H) (P.subgroupOf H)
⊢ HSMul.hSMul (α := MulAut ↥H) ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H) (P.subgroupOf H) =
    (HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) (↑h : G) : MulAut G) P).subgroupOf H

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
P H : Subgroup G
hP : P ≤ H
h g : ↥H
hg : g ∈ (↑(P.subgroupOf H) : Set ↥H)
⊢ Membership.mem (α := ↥H)
    ((HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) (↑h : G) : MulAut G) P).subgroupOf H)
    ((((MulDistribMulAction.toMonoidEnd (MulAut ↥H) ↥H : (a : MulAut ↥H) → Monoid.End ↥H)
              ((MulAut.conj : (a : ↥H) → MulAut ↥H) h) :
            Monoid.End ↥H) :
          (a : ↥H) → ↥H)
        g :
      ↥H)

Tactic:
⟨g, hg, rfl⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro, Set.image, Subtype.val, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
P H : Subgroup G
hP : P ≤ H
h g : ↥H
hg : g ∈ (↑(P.subgroupOf H) : Set ↥H)
⊢ Membership.mem (α := ↥H)
    ((HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) (↑h : G) : MulAut G) P).subgroupOf H)
    ((((MulDistribMulAction.toMonoidEnd (MulAut ↥H) ↥H : (a : MulAut ↥H) → Monoid.End ↥H)
              ((MulAut.conj : (a : ↥H) → MulAut ↥H) h) :
            Monoid.End ↥H) :
          (a : ↥H) → ↥H)
        g :
      ↥H)

Tactic:
exact ⟨g, hg, rfl⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
P H : Subgroup G
hP : P ≤ H
h p : ↥H
g : G
hg : g ∈ (↑P : Set G)
hp :
  Eq (α := G)
    ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
              ((MulAut.conj : (a : G) → MulAut G) (↑h : G)) :
            Monoid.End G) :
          (a : G) → G)
        g :
      G)
    ((H.subtype : (a : ↥H) → G) p : G)
⊢ p ∈ HSMul.hSMul (α := MulAut ↥H) ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H) (P.subgroupOf H)

Tactic:
⟨⟨g, hP hg⟩, hg, Subtype.ext hp⟩

Premises used: Set.Mem, setOf, Subtype.mk, And.intro, Exists.intro, Set.image, Subtype.ext
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
P H : Subgroup G
hP : P ≤ H
h p : ↥H
g : G
hg : g ∈ (↑P : Set G)
hp :
  Eq (α := G)
    ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
              ((MulAut.conj : (a : G) → MulAut G) (↑h : G)) :
            Monoid.End G) :
          (a : G) → G)
        g :
      G)
    ((H.subtype : (a : ↥H) → G) p : G)
⊢ p ∈ HSMul.hSMul (α := MulAut ↥H) ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H) (P.subgroupOf H)

Tactic:
exact ⟨⟨g, hP hg⟩, hg, Subtype.ext hp⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : Group α
inst_2 : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ a • (S ⊓ T) = a • S ⊓ a • T

Tactic:
simp [SetLike.ext_iff, mem_pointwise_smul_iff_inv_smul_mem]

Premises used: SetLike.ext_iff, Subgroup.mem_pointwise_smul_iff_inv_smul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ (↑H : Set G) * {h} = (↑H : Set G)

Tactic:
simp [preimage, mul_mem_cancel_right (inv_mem hh)]

Premises used: InvMemClass.inv_mem, Set.preimage, mul_mem_cancel_right
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ {h} * (↑H : Set G) = (↑H : Set G)

Tactic:
simp [preimage, mul_mem_cancel_left (inv_mem hh)]

Premises used: InvMemClass.inv_mem, Set.preimage, mul_mem_cancel_left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
hH : H.Normal
g : ConjAct G
⊢ g • H = H

Tactic:
have : ∀ g : ConjAct G, g • H ≤ H :=
    fun _ => map_le_iff_le_comap.2 fun _ h => hH.conj_mem _ h _
  (this g).antisymm <| (smul_inv_smul g H).symm.trans_le (map_mono <| this _)

Premises used: Iff.mpr, LE.le.antisymm, Eq.trans_le, smul_inv_smul, Inv.inv, Subgroup.map_le_iff_le_comap, ConjAct.ofConjAct, Subgroup.map_mono, Eq.symm, DFunLike.coe, Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
g : G
H : Subgroup G
h : H.Normal
⊢ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) g : MulAut G) H = H

Tactic:
h.conjAct g

Premises used: Subgroup.Normal.conjAct, MulDistribMulAction.toMonoidHom
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : ∀ (g : G), HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) g : MulAut G) H = H
conj_mem : ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H
⊢ H.Normal

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : ∀ (g : G), HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) g : MulAut G) H = H
n : G
hn : n ∈ H
g : G
conj_mem : n ∈ H
⊢ g * n * g⁻¹ ∈ H

Tactic:
rw [← h g, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← map_inv, MulAut.smul_def,
    MulAut.conj_apply, inv_inv, mul_assoc, mul_assoc, inv_mul_cancel, mul_one,
    ← mul_assoc, inv_mul_cancel, one_mul]

Premises used: inv_mul_cancel, map_inv, MulAut.smul_def, mul_assoc, MulAut.conj_apply, inv_inv, mul_one, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, one_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : ∀ (g : G), HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) g : MulAut G) H = H
n : G
hn : n ∈ H
g : G
⊢ n ∈ H

Tactic:
hn
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : ∀ (g : G), HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) g : MulAut G) H = H
n : G
hn : n ∈ H
g : G
⊢ n ∈ H

Tactic:
exact hn
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : ∀ (g : G), g ∈ H.normalCore ↔ Membership.mem (γ := Subgroup G) (⨅ (g : ConjAct G), g • H) g
⊢ H.normalCore = ⨅ (g : ConjAct G), g • H

Tactic:
ext g
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
g : G
h :
  g ∈ { carrier := {a : G | ∀ (b : G), b * a * b⁻¹ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ : Subgroup G } ↔
    ∀ (i : ConjAct G), i⁻¹ • g ∈ H
⊢ g ∈ H.normalCore ↔ Membership.mem (γ := Subgroup G) (⨅ (g : ConjAct G), g • H) g

Tactic:
simp only [Subgroup.normalCore, Subgroup.mem_iInf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem]

Premises used: Subgroup.mem_iInf, Subgroup.normalCore, Subgroup.mem_pointwise_smul_iff_inv_smul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
g : G
⊢ g ∈ { carrier := {a : G | ∀ (b : G), b * a * b⁻¹ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ : Subgroup G } ↔
    ∀ (i : ConjAct G), i⁻¹ • g ∈ H

Tactic:
⟨fun h x ↦ h x⁻¹, fun h x ↦ ?_⟩

Premises used: Inv.inv, Iff.intro
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
g : G
h : ∀ (h : ∀ (i : ConjAct G), i⁻¹ • g ∈ H) (x : G), x * g * x⁻¹ ∈ H
⊢ g ∈ { carrier := {a : G | ∀ (b : G), b * a * b⁻¹ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ : Subgroup G } ↔
    ∀ (i : ConjAct G), i⁻¹ • g ∈ H

Tactic:
refine ⟨fun h x ↦ h x⁻¹, fun h x ↦ ?_⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
g : G
h : ∀ (i : ConjAct G), i⁻¹ • g ∈ H
x : G
⊢ x * g * x⁻¹ ∈ H

Tactic:
simpa only [ConjAct.toConjAct_inv, inv_inv] using h x⁻¹

Premises used: ConjAct.toConjAct_inv, Inv.inv, inv_inv
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
g : G
rw :
  HSMul.hSMul (α := ConjAct G) ((ConjAct.toConjAct : (a : G) → ConjAct G) g : ConjAct G) H = H ↔
    Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) g⁻¹
⊢ HSMul.hSMul (α := ConjAct G) ((ConjAct.toConjAct : (a : G) → ConjAct G) g : ConjAct G) H = H ↔
    Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) g

Tactic:
rw [← (normalizer H : Subgroup G).inv_mem_iff]

Premises used: Subgroup.normalizer, SetLike.coe, Subgroup.inv_mem_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
g : G
⊢ HSMul.hSMul (α := ConjAct G) ((ConjAct.toConjAct : (a : G) → ConjAct G) g : ConjAct G) H = H ↔
    Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) g⁻¹

Tactic:
simp only [Subgroup.ext_iff, mem_pointwise_smul_iff_inv_smul_mem,
    ← ConjAct.toConjAct_inv, ConjAct.toConjAct_smul, mem_normalizer_iff, inv_inv, Iff.comm]

Premises used: ConjAct.toConjAct_inv, Subgroup.ext_iff, ConjAct.toConjAct_smul, Subgroup.mem_normalizer_iff, inv_inv, Iff.comm, Subgroup.mem_pointwise_smul_iff_inv_smul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) g
⊢ HSMul.hSMul (α := ConjAct G) ((ConjAct.toConjAct : (a : G) → ConjAct G) g : ConjAct G) H = H

Tactic:
conjAct_pointwise_smul_iff.2 hg

Premises used: Iff.mpr, Subgroup.conjAct_pointwise_smul_iff
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
N : Type u_3
inst_2 : Group N
g : G
a b : ℤ
⊢ Membership.mem (γ := Set G) (Set.range fun (x : ℤ) ↦ g ^ x)
    (HMul.hMul (α := G) ((fun (x : ℤ) ↦ g ^ x) a) ((fun (x : ℤ) ↦ g ^ x) b))

Tactic:
⟨a + b, zpow_add ..⟩

Premises used: zpow_add, Set.Mem, setOf, HAdd.hAdd, Exists.intro, Set.range
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
N : Type u_3
inst_2 : Group N
g : G
a b : ℤ
⊢ Membership.mem (γ := Set G) (Set.range fun (x : ℤ) ↦ g ^ x)
    (HMul.hMul (α := G) ((fun (x : ℤ) ↦ g ^ x) a) ((fun (x : ℤ) ↦ g ^ x) b))

Tactic:
exact ⟨a + b, zpow_add ..⟩
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
N : Type u_3
inst_2 : Group N
g : G
a : ℤ
⊢ Membership.mem (γ := Set G) (Set.range fun (x : ℤ) ↦ g ^ x) ((fun (x : ℤ) ↦ g ^ x) a)⁻¹

Tactic:
⟨-a, zpow_neg ..⟩

Premises used: Set.Mem, setOf, zpow_neg, Exists.intro, Set.range, Neg.neg
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
N : Type u_3
inst_2 : Group N
g : G
a : ℤ
⊢ Membership.mem (γ := Set G) (Set.range fun (x : ℤ) ↦ g ^ x) ((fun (x : ℤ) ↦ g ^ x) a)⁻¹

Tactic:
exact ⟨-a, zpow_neg ..⟩
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g : G
⊢ Membership.mem (γ := Subgroup G) (zpowers g) g

Tactic:
⟨1, zpow_one _⟩

Premises used: Set.Mem, setOf, zpow_one, Exists.intro, Set.range, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g : G
⊢ (↑(zpowers g) : Set G) = Set.range fun (x : ℤ) ↦ g ^ x

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g : G
h : ∀ (x : G), Membership.mem (γ := Subgroup G) (zpowers g) x ↔ Membership.mem (γ := Subgroup G) (closure {g}) x
⊢ Eq (α := Subgroup G) (zpowers g) (closure {g})

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g x : G
⊢ Membership.mem (γ := Subgroup G) (zpowers g) x ↔ Membership.mem (γ := Subgroup G) (closure {g}) x

Tactic:
mem_closure_singleton.symm

Premises used: Set.Mem, setOf, Subgroup.mem_closure_singleton, Set.range, Iff.symm
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g x : G
⊢ Membership.mem (γ := Subgroup G) (zpowers g) x ↔ Membership.mem (γ := Subgroup G) (closure {g}) x

Tactic:
exact mem_closure_singleton.symm

Premises used: Subgroup.mem_closure_singleton, Iff.symm
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g h : G
⊢ Membership.mem (γ := Subgroup G) (zpowers g) h ↔ ∃ (k : ℤ), g ^ k = h

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g : G
k : ℤ
⊢ Membership.mem (γ := Subgroup G) (zpowers g) (g ^ k)

Tactic:
mem_zpowers_iff.mpr ⟨k, rfl⟩

Premises used: Iff.mpr, Exists.intro, Subgroup.mem_zpowers_iff, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
g : G
k : ℕ
⊢ Membership.mem (γ := Subgroup G) (zpowers g) (g ^ k)

Tactic:
zpow_natCast g k ▸ zpow_mem_zpowers g k

Premises used: zpow_natCast, Eq.rec, Nat.cast, Subgroup.zpow_mem_zpowers
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
x : G
p : ↥(zpowers x) → Prop
⊢ (∀ (g : ↥(zpowers x)), p g) ↔
    ∀ (m : ℤ), p (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (zpowers x) x_1) (x ^ m) ⋯)

Tactic:
Set.forall_subtype_range_iff

Premises used: Set.Mem, setOf, Set.range, Set.forall_subtype_range_iff
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
x : G
p : ↥(zpowers x) → Prop
⊢ (∃ (g : ↥(zpowers x)), p g) ↔
    ∃ (m : ℤ), p (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (zpowers x) x_1) (x ^ m) ⋯)

Tactic:
Set.exists_subtype_range_iff

Premises used: Set.Mem, setOf, Set.exists_subtype_range_iff, Set.range
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
x : G
p : G → Prop
⊢ (∀ (g : G), Membership.mem (γ := Subgroup G) (zpowers x) g → p g) ↔ ∀ (m : ℤ), p (x ^ m)

Tactic:
Set.forall_mem_range

Premises used: Set.forall_mem_range, Set.Mem, setOf, Set.range
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
x : G
p : G → Prop
⊢ (∃ (g : G), Membership.mem (γ := Subgroup G) (zpowers x) g ∧ p g) ↔ ∃ (m : ℤ), p (x ^ m)

Tactic:
Set.exists_range_iff

Premises used: Set.Mem, setOf, Set.exists_range_iff, Set.range
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_3
inst_1 : Group N
f : G →* N
x : G
rw : Subgroup.map f (Subgroup.closure {x}) = Subgroup.zpowers ((f : (a : G) → N) x)
rw₁ : Subgroup.map f (Subgroup.closure {x}) = Subgroup.closure (singleton (α := N) ((f : (a : G) → N) x : N))
rw₂ :
  Eq (α := Subgroup N) (Subgroup.closure (Set.image (α := G) (⇑f : (a : G) → N) {x}))
    (Subgroup.closure (singleton (α := N) ((f : (a : G) → N) x : N)))
rw₃ rw₄ :
  Eq (α := Subgroup N) (Subgroup.closure (singleton (α := N) ((f : (a : G) → N) x : N)))
    (Subgroup.closure (singleton (α := N) ((f : (a : G) → N) x : N)))
⊢ Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers ((f : (a : G) → N) x)

Tactic:
rw [Subgroup.zpowers_eq_closure, Subgroup.zpowers_eq_closure, f.map_closure, Set.image_singleton]

Premises used: Set.image_singleton, MonoidHom.map_closure, Subgroup.zpowers_eq_closure
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
a b k : ℤ
rw : (fun (x : ℤ) ↦ x • a) k = b ↔ b = k * a
rw₁ : b = (fun (x : ℤ) ↦ x • a) k ↔ b = k * a
rw₂ rw₃ : b = (fun (x : ℤ) ↦ x • a) k ↔ b = k • a
⊢ (fun (x : ℤ) ↦ x • a) k = b ↔ b = a * k

Tactic:
rw [mul_comm, eq_comm, ← smul_eq_mul]

Premises used: eq_comm, mul_comm, smul_eq_mul
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
h :
  ∀ (z : ℤ), Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples 1) z ↔ Membership.mem (γ := AddSubgroup ℤ) ⊤ z
⊢ Eq (α := AddSubgroup ℤ) (AddSubgroup.zmultiples 1) ⊤

Tactic:
ext z
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
z : ℤ
⊢ Membership.mem (γ := AddSubgroup ℤ) (AddSubgroup.zmultiples 1) z ↔ Membership.mem (γ := AddSubgroup ℤ) ⊤ z

Tactic:
simp [Int.mem_zmultiples_iff]

Premises used: Int.mem_zmultiples_iff
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
x : G
h :
  ∀ (x_1 : Additive G),
    Membership.mem (γ := Set (Additive G)) ((⇑Additive.ofMul : (a : G) → Additive G) '' (↑(Subgroup.zpowers x) : Set G))
        x_1 ↔
      x_1 ∈
        (↑(AddSubgroup.zmultiples ((Additive.ofMul : (a : G) → Additive G) x) : AddSubgroup (Additive G)) :
          Set (Additive G))
⊢ (⇑Additive.ofMul : (a : G) → Additive G) '' (↑(Subgroup.zpowers x) : Set G) =
    (↑(AddSubgroup.zmultiples ((Additive.ofMul : (a : G) → Additive G) x) : AddSubgroup (Additive G)) :
      Set (Additive G))

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
x : G
x_1 : Additive G
⊢ Membership.mem (γ := Set (Additive G)) ((⇑Additive.ofMul : (a : G) → Additive G) '' (↑(Subgroup.zpowers x) : Set G))
      x_1 ↔
    x_1 ∈
      (↑(AddSubgroup.zmultiples ((Additive.ofMul : (a : G) → Additive G) x) : AddSubgroup (Additive G)) :
        Set (Additive G))

Tactic:
Set.mem_image_iff_of_inverse (congrFun rfl) (congrFun rfl)

Premises used: Set.Mem, Additive, congrFun, Set.mem_image_iff_of_inverse, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Goal:
G : Type u_1
inst : Group G
x : G
x_1 : Additive G
⊢ Membership.mem (γ := Set (Additive G)) ((⇑Additive.ofMul : (a : G) → Additive G) '' (↑(Subgroup.zpowers x) : Set G))
      x_1 ↔
    x_1 ∈
      (↑(AddSubgroup.zmultiples ((Additive.ofMul : (a : G) → Additive G) x) : AddSubgroup (Additive G)) :
        Set (Additive G))

Tactic:
exact Set.mem_image_iff_of_inverse (congrFun rfl) (congrFun rfl)

Premises used: congrFun, Set.mem_image_iff_of_inverse, rfl