awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
p : ℕ
g : G
h : g ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (CommMonoid.primaryComponent G p))
k : ℕ
hk : g ^ p ^ k = 1
rw : (g ^ p ^ k)⁻¹ = 1
rw₁ : Eq.{u_1 + 1} (α := G) 1⁻¹ 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := G) 1 1
⊢ g⁻¹ ^ p ^ k = 1

Tactic:
rw [inv_pow, hk, inv_one]

Premises used: inv_one, inv_pow
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
p : ℕ
g : G
⊢ Membership.mem (γ := Subgroup G) (primaryComponent G p) g ↔ ∃ (k : ℕ), g ^ p ^ k = 1

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
p : ℕ
inst_1 : Fact (Nat.Prime p)
g : G
⊢ Membership.mem (γ := Subgroup G) (primaryComponent G p) g ↔ ∃ (n : ℕ), orderOf g = p ^ n

Tactic:
exists_orderOf_eq_prime_pow_iff.symm

Premises used: Set.Mem, setOf, exists_orderOf_eq_prime_pow_iff, Iff.symm
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : CommGroup G
p : ℕ
g : ↥(primaryComponent G p)
x : ℕ
hk : (↑g : G) ^ p ^ x = 1
⊢ (↑(g ^ p ^ x) : G) = (↑1 : G)

Tactic:
simpa using hk
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
⊢ IsMulTorsionFree.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (torsion G))

Tactic:
.of_not_isOfFinOrder fun g hne hfin ↦ hne ?_

Premises used: IsMulTorsionFree.of_not_isOfFinOrder
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
refine : ∀ (g : HasQuotient.Quotient G (B := Subgroup G) (torsion G)) (hne : g ≠ 1) (hfin : IsOfFinOrder g), g = 1
⊢ IsMulTorsionFree.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (torsion G))

Tactic:
refine .of_not_isOfFinOrder fun g hne hfin ↦ hne ?_
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
g : HasQuotient.Quotient G (B := Subgroup G) (torsion G)
hne : g ≠ 1
hfin : IsOfFinOrder g
mk :
  ∀ (g : G)
    (hne :
      Ne (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
        (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1)
    (hfin :
      IsOfFinOrder (G := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
        (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g)),
    Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
      (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
⊢ g = 1

Tactic:
obtain ⟨g⟩ := g
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
g_1 : HasQuotient.Quotient G (B := Subgroup G) (torsion G)
g : G
hne :
  Ne (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
hfin :
  IsOfFinOrder (G := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g)
mk :
  ∀ (m : ℕ) (mpos : 0 < m)
    (hm :
      HPow.hPow (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
          (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) m =
        1),
    Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
      (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
⊢ Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1

Tactic:
obtain ⟨m, mpos, hm⟩ := hfin.exists_pow_eq_one

Premises used: IsOfFinOrder.exists_pow_eq_one
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
g_1 : HasQuotient.Quotient G (B := Subgroup G) (torsion G)
g : G
hne :
  Ne (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
hfin :
  IsOfFinOrder (G := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g)
m : ℕ
mpos : 0 < m
hm :
  HPow.hPow (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
      (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) m =
    1
mk :
  ∀ (n : ℕ) (npos : 0 < n) (hn : HPow.hPow (α := G) ((fun (x : G) ↦ x ^ m) g) n = 1),
    Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
      (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
⊢ Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1

Tactic:
obtain ⟨n, npos, hn⟩ := ((QuotientGroup.eq_one_iff _).mp hm).exists_pow_eq_one

Premises used: Iff.mp, QuotientGroup.eq_one_iff, IsOfFinOrder.exists_pow_eq_one
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
g_1 : HasQuotient.Quotient G (B := Subgroup G) (torsion G)
g : G
hne :
  Ne (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
hfin :
  IsOfFinOrder (G := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g)
m : ℕ
mpos : 0 < m
hm :
  HPow.hPow (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
      (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) m =
    1
n : ℕ
npos : 0 < n
hn : HPow.hPow (α := G) ((fun (x : G) ↦ x ^ m) g) n = 1
⊢ Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1

Tactic:
(QuotientGroup.eq_one_iff g).mpr
    (isOfFinOrder_iff_pow_eq_one.mpr ⟨m * n, mul_pos mpos npos, (pow_mul g m n).symm ▸ hn⟩)

Premises used: Iff.mpr, HMul.hMul, Eq.rec, pow_mul, mul_pos, And.intro, Exists.intro, Eq.symm, isOfFinOrder_iff_pow_eq_one, QuotientGroup.eq_one_iff
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : CommGroup G
inst_1 : CommGroup H
g_1 : HasQuotient.Quotient G (B := Subgroup G) (torsion G)
g : G
hne :
  Ne (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1
hfin :
  IsOfFinOrder (G := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g)
m : ℕ
mpos : 0 < m
hm :
  HPow.hPow (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
      (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) m =
    1
n : ℕ
npos : 0 < n
hn : HPow.hPow (α := G) ((fun (x : G) ↦ x ^ m) g) n = 1
⊢ Eq (α := HasQuotient.Quotient G (B := Subgroup G) (torsion G))
    (Quot.mk (⇑(QuotientGroup.leftRel (torsion G)) : G → G → Prop) g) 1

Tactic:
exact (QuotientGroup.eq_one_iff g).mpr
    (isOfFinOrder_iff_pow_eq_one.mpr ⟨m * n, mul_pos mpos npos, (pow_mul g m n).symm ▸ hn⟩)

Premises used: Iff.mpr, QuotientGroup.eq_one_iff
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
m : M
h : m ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (AddCommGroup.torsion M)))
n : ℕ
hn : n > 0
hn' : Function.IsPeriodicPt (fun (x : M) ↦ m + x) n 0
simp : ∀ (hn' : n • m = 0), r • n • m = 0
⊢ Function.IsPeriodicPt (fun (x : M) ↦ r • m + x) n 0

Tactic:
simp only [Function.IsPeriodicPt, Function.IsFixedPt, add_left_iterate, add_zero,
      smul_comm n] at hn' ⊢

Premises used: add_left_iterate, Function.IsPeriodicPt, Function.IsFixedPt, SMulCommClass.smul_comm, add_zero
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
m : M
h : m ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (AddCommGroup.torsion M)))
n : ℕ
hn : n > 0
hn' : n • m = 0
⊢ r • n • m = 0

Tactic:
simp only [hn', smul_zero]

Premises used: smul_zero
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
m : M
h : m ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (AddCommGroup.torsion M)))
n : ℕ
hn : n > 0
hn' : Function.IsPeriodicPt (fun (x : M) ↦ m + x) n 0
simp simp₁ : ∀ (hn' : n • m = 0), r • n • m = 0
⊢ Function.IsPeriodicPt (fun (x : M) ↦ r • m + x) n 0

Tactic:
{ simp only [Function.IsPeriodicPt, Function.IsFixedPt, add_left_iterate, add_zero,
      smul_comm n] at hn' ⊢; simp only [hn', smul_zero] }

Premises used: smul_zero, add_left_iterate, Function.IsPeriodicPt, Function.IsFixedPt, SMulCommClass.smul_comm, add_zero
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M :=
  let __src : AddSubgroup M := AddCommGroup.torsion M;
  { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }
⊢ AddSubgroup.map (↑(AddEquiv.refl M) : M →+ M) (AddCommGroup.torsion M) = S.toAddSubgroup

Tactic:
simp [S]
-- Module: Mathlib.GroupTheory.Torsion
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : HasDistribNeg M
⊢ HPow.hPow (α := M) (β := ℕ) (-1) 2 = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Type u_2
inst_1 : CommGroup A
ϕ : MonoidHom.{u_1, u_2} (↥H) A
T : H.LeftTransversal
inst_2 : H.FiniteIndex
⊢ diff ϕ T T = 1

Tactic:
mul_eq_left.mp (diff_mul_diff ϕ T T T)

Premises used: Subgroup.leftTransversals.diff_mul_diff, Iff.mp, mul_eq_left
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Type u_2
inst_1 : CommGroup A
ϕ : MonoidHom.{u_1, u_2} (↥H) A
S T : H.LeftTransversal
inst_2 : H.FiniteIndex
⊢ (diff ϕ S T)⁻¹ = diff ϕ T S

Tactic:
inv_eq_of_mul_eq_one_right <| (diff_mul_diff ϕ S T S).trans <| diff_self ϕ S

Premises used: Subgroup.leftTransversals.diff_self, Subgroup.leftTransversals.diff_mul_diff, inv_eq_of_mul_eq_one_right, Eq.trans
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Type u_2
inst_1 : CommGroup A
ϕ : MonoidHom.{u_1, u_2} (↥H) A
S T : H.LeftTransversal
inst_2 : H.FiniteIndex
g : G
x : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
x_1 : G ⧸ H
⊢ Eq.{u_2 + 1} (α := A)
    ((ϕ : (a : ↥H) → A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((⋯.leftQuotientEquiv (S := (↑(g • S) : Set G)) : (a : G ⧸ H) → (↑(↑(g • S) : Set G) : Type u_1)) x_1) :
                G)⁻¹
            (↑((⋯.leftQuotientEquiv (S := (↑(g • T) : Set G)) : (a : G ⧸ H) → (↑(↑(g • T) : Set G) : Type u_1)) x_1) :
              G))
          ⋯) :
      A)
    ((ϕ : (a : ↥H) → A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1))
                    ((Equiv.symm (toPerm g) : (a : G ⧸ H) → G ⧸ H) x_1)) :
                G)⁻¹
            (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1))
                  ((Equiv.symm (toPerm g) : (a : G ⧸ H) → G ⧸ H) x_1)) :
              G))
          ⋯) :
      A)

Tactic:
simp only [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc,
      inv_mul_cancel_left, toPerm_symm_apply]

Premises used: inv_mul_cancel_left, mul_assoc, MulAction.toPerm_symm_apply, Subgroup.smul_apply_eq_smul_apply_inv_smul, mul_inv_rev, smul_eq_mul
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ H.transferFunction g q =
    HPow.hPow (β := ℤ) g
        (ZMod.cast (n :=
          minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
            (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
              (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                ((H.quotientEquivSigmaZMod g :
                    (a : G ⧸ H) →
                      (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                        ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                  q))))
          (Sigma.snd (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
              ((H.quotientEquivSigmaZMod g :
                  (a : G ⧸ H) →
                    (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                      ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                q) :
            ZMod
              (minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
                (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
                  (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                    ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                    ((H.quotientEquivSigmaZMod g :
                        (a : G ⧸ H) →
                          (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                      q)))))) *
      Quotient.out (s := QuotientGroup.leftRel H)
        (Quotient.out (s := orbitRel (↥(zpowers g)) (G ⧸ H))
          (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
            ((H.quotientEquivSigmaZMod g :
                (a : G ⧸ H) →
                  (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ×
                    ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
              q)))

Tactic:
rfl

Premises used: Subgroup.transferFunction, rfl
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ H.transferFunction g q ∈ H.transferSet g

Tactic:
⟨q, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, Subgroup.transferSet, rfl
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ (↑((⋯.leftQuotientEquiv (S := (↑(H.transferTransversal g) : Set G)) :
            (a : G ⧸ H) → (↑(↑(H.transferTransversal g) : Set G) : Type u_1))
          q) :
      G) =
    H.transferFunction g q

Tactic:
IsComplement.leftQuotientEquiv_apply (coe_transferFunction g) q

Premises used: setOf, Subgroup.coe_transferFunction, Set.range, Subgroup.IsComplement.leftQuotientEquiv_apply, Subgroup.transferSet
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))
rw :
  HPow.hPow (β := ℤ) g
        (if k = 0 then
          (↑(minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
                (Quotient.out
                  (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                    ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                    (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                      ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1))))) :
            ℤ)
        else k.cast) *
      Quotient.out
        (Quotient.out
          (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
            (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1)))) =
    if k = 0 then g ^ minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
⊢ (↑((⋯.leftQuotientEquiv (S := (↑(g • H.transferTransversal g) : Set G)) :
            (a : G ⧸ H) → (↑(↑(g • H.transferTransversal g) : Set G) : Type u_1))
          (HPow.hPow (β := ℤ) g k.cast • Quotient.out q)) :
      G) =
    if k = 0 then g ^ minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)

Tactic:
rw [smul_apply_eq_smul_apply_inv_smul, transferTransversal_apply, transferFunction_apply, ←
    mul_smul, ← zpow_neg_one, ← zpow_add, quotientEquivSigmaZMod_apply, smul_eq_mul, ← mul_assoc,
    ← zpow_one_add, Int.cast_add, Int.cast_neg, Int.cast_one, intCast_cast, cast_id', id, ←
    sub_eq_neg_add, cast_sub_one, add_sub_cancel]

Premises used: Int.cast_neg, Subgroup.transferTransversal_apply, zpow_add, zpow_neg_one, sub_eq_neg_add, mul_assoc, Int.cast_add, zpow_one_add, Subgroup.smul_apply_eq_smul_apply_inv_smul, id, Subgroup.quotientEquivSigmaZMod_apply, ZMod.cast_id', add_sub_cancel, Subgroup.transferFunction_apply, ZMod.cast_sub_one, smul_eq_mul, ZMod.intCast_cast, SemigroupAction.mul_smul, Int.cast_one
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))
hk : ¬k = 0
neg :
  HPow.hPow (β := ℤ) g k.cast *
      Quotient.out
        (Quotient.out
          (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
            (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1)))) =
    if k = 0 then g ^ minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
neg₁ neg₂ :
  HPow.hPow (β := ℤ) g k.cast *
      Quotient.out
        (Quotient.out
          (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
            (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1)))) =
    HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
⊢ HPow.hPow (β := ℤ) g
        (if k = 0 then
          (↑(minimalPeriod (fun (x : G ⧸ H) ↦ g • x)
                (Quotient.out
                  (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                    ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
                    (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
                      ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1))))) :
            ℤ)
        else k.cast) *
      Quotient.out
        (Quotient.out
          (Sigma.fst (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
            ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q)))
            (Sigma.mk (β := fun (q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) ↦
              ZMod (minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q))) q (k - 1)))) =
    if k = 0 then g ^ minimalPeriod (fun (x : G ⧸ H) ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)

Tactic:
rw [if_neg hk, if_neg hk]

Premises used: if_neg
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Type u_2
inst_1 : CommGroup A
ϕ : MonoidHom.{u_1, u_2} (↥H) A
inst_2 : H.FiniteIndex
T : H.LeftTransversal := default
rw : diff ϕ T T = 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) 1 1
⊢ diff ϕ T (HSMul.hSMul (α := G) 1 T) = 1

Tactic:
rw [one_smul, diff_self]

Premises used: Subgroup.leftTransversals.diff_self, one_smul
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Type u_2
inst_1 : CommGroup A
ϕ : MonoidHom.{u_1, u_2} (↥H) A
inst_2 : H.FiniteIndex
T : H.LeftTransversal := default
g h : G
rw : diff ϕ T (g • h • T) = diff ϕ T (g • T) * diff ϕ T (h • T)
rw₁ : diff ϕ T (g • T) * diff ϕ (g • T) (g • h • T) = diff ϕ T (g • T) * diff ϕ T (h • T)
S : H.LeftTransversal
rw₂ : diff ϕ T (g • T) * diff ϕ T (h • T) = diff ϕ T (g • T) * diff ϕ T (h • T)
S₁ : H.LeftTransversal
rw₃ : diff ϕ T (g • T) * diff ϕ T (h • T) = diff ϕ T (g • T) * diff ϕ T (h • T)
S₂ : H.LeftTransversal
⊢ diff ϕ T ((g * h) • T) = diff ϕ T (g • T) * diff ϕ T (h • T)

Tactic:
rw [mul_smul, ← diff_mul_diff, smul_diff_smul]

Premises used: Subgroup.leftTransversals.diff_mul_diff, Subgroup.leftTransversals.smul_diff_smul, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Type u_2
inst_1 : CommGroup A
ϕ : MonoidHom.{u_1, u_2} (↥H) A
T : H.LeftTransversal
inst_2 : H.FiniteIndex
g : G
rw :
  ({ toFun := fun (g : G) ↦ diff ϕ default (HSMul.hSMul (β := H.LeftTransversal) g default), map_one' := ⋯,
          map_mul' := ⋯ } :
        (a : G) → A)
      g =
    diff ϕ default (HSMul.hSMul (β := H.LeftTransversal) g default)
R : H.LeftTransversal
⊢ (ϕ.transfer : (a : G) → A) g = diff ϕ T (g • T)

Tactic:
rw [transfer, ← diff_mul_diff, ← smul_diff_smul, mul_comm, diff_mul_diff]

Premises used: MonoidHom.transfer, Subgroup.leftTransversals.diff_mul_diff, Subgroup.leftTransversals.smul_diff_smul, mul_comm
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Type u_2
inst_1 : CommGroup A
ϕ : MonoidHom.{u_1, u_2} (↥H) A
T : H.LeftTransversal
inst_2 : H.FiniteIndex
g : G
⊢ ({ toFun := fun (g : G) ↦ diff ϕ default (HSMul.hSMul (β := H.LeftTransversal) g default), map_one' := ⋯,
          map_mul' := ⋯ } :
        (a : G) → A)
      g =
    diff ϕ default (HSMul.hSMul (β := H.LeftTransversal) g default)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Type u_2
inst_1 : CommGroup A
ϕ : MonoidHom.{u_1, u_2} (↥H) A
inst_2 : H.FiniteIndex
g : G
inst_3 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ Eq.{u_2 + 1} (α := A) ((ϕ.transfer : (a : G) → A) g : A)
    (∏ q : G ⧸ H,
        (ϕ : (a : ↥H) → A)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((⋯.leftQuotientEquiv (S := (↑(H.transferTransversal g) : Set G)) :
                        (a : G ⧸ H) → (↑(↑(H.transferTransversal g) : Set G) : Type u_1))
                      q) :
                  G)⁻¹
              (↑((⋯.leftQuotientEquiv (S := (↑(g • H.transferTransversal g) : Set G)) :
                      (a : G ⧸ H) → (↑(↑(g • H.transferTransversal g) : Set G) : Type u_1))
                    q) :
                G))
            ⋯) :
      A)

Tactic:
transfer_def ϕ (transferTransversal H g) g

Premises used: Subgroup.leftTransversals.diff, MonoidHom.transfer_def, Subgroup.transferTransversal