awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
R S T : H.LeftTransversal
inst_2 : H.FiniteIndex
q : G ⧸ H
h : Membership.mem (γ := Finset (G ⧸ H)) univ q
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        (HMul.hMul (α := G)
          (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
          (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G))
        ⋯ *
      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)) q) : G)⁻¹
          (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G))
        ⋯ =
    Subtype.mk (p := fun (x : G) ↦ x ∈ H)
      (HMul.hMul (α := G)
        (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
        (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G))
      ⋯
have simp_rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((sorry.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
            (↑((sorry.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G))
          sorry *
        Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((sorry.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G)⁻¹
            (↑((sorry.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G))
          sorry) :
    G) =
  HMul.hMul (α := G) (↑((sorry.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
    (↑((sorry.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G)
Tactic: simp_rw [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
R S T : H.LeftTransversal
inst_2 : H.FiniteIndex
q : G ⧸ H
h : Membership.mem (γ := Finset (G ⧸ H)) univ q
simp_rw :
  (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
              (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G))
            ⋯ *
          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)) q) : G)⁻¹
              (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G))
            ⋯) :
      G) =
    HMul.hMul (α := G) (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
      (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G)
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        (HMul.hMul (α := G)
          (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
          (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G))
        ⋯ *
      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)) q) : G)⁻¹
          (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G))
        ⋯ =
    Subtype.mk (p := fun (x : G) ↦ x ∈ H)
      (HMul.hMul (α := G)
        (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
        (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G))
      ⋯
have simp_rw₁ : HMul.hMul (α := G) (↑((sorry.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
      (↑((sorry.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G) *
    HMul.hMul (α := G) (↑((sorry.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G)⁻¹
      (↑((sorry.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G) =
  HMul.hMul (α := G) (↑((sorry.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
    (↑((sorry.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G)
Tactic: simp_rw [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ (↑(H.transferFunction g q) : G ⧸ H) = q
have rw : (↑(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)))) :
    G ⧸ H) =
  q
Tactic: rw [transferFunction_apply, ← smul_eq_mul, Quotient.coe_smul_out,
    ← quotientEquivSigmaZMod_symm_apply, Sigma.eta, symm_apply_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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))
⊢ (↑((⋯.leftQuotientEquiv (S := (↑(H.transferTransversal g) : Set G)) :
            (a : G ⧸ H) → (↑(↑(H.transferTransversal g) : Set G) : Type u_1))
          (HPow.hPow (β := ℤ) g k.cast • Quotient.out q)) :
      G) =
    HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
have rw : H.transferFunction g (HPow.hPow (β := ℤ) g k.cast • Quotient.out q) =
  HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
Tactic: rw [transferTransversal_apply, transferFunction_apply, ← quotientEquivSigmaZMod_symm_apply,
    apply_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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 :
  H.transferFunction g (HPow.hPow (β := ℤ) g k.cast • Quotient.out q) =
    HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
⊢ (↑((⋯.leftQuotientEquiv (S := (↑(H.transferTransversal g) : Set G)) :
            (a : G ⧸ H) → (↑(↑(H.transferTransversal g) : Set G) : Type u_1))
          (HPow.hPow (β := ℤ) g k.cast • Quotient.out q)) :
      G) =
    HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
have rw₁ : 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)))
                (HPow.hPow (β := ℤ) g k.cast • Quotient.out 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)))
              (HPow.hPow (β := ℤ) g k.cast • Quotient.out 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)))
                    (HPow.hPow (β := ℤ) g k.cast • Quotient.out 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)))
            (HPow.hPow (β := ℤ) g k.cast • Quotient.out q)))) =
  HPow.hPow (β := ℤ) g k.cast * Quotient.out (Quotient.out q)
Tactic: rw [transferTransversal_apply, transferFunction_apply, ← quotientEquivSigmaZMod_symm_apply,
    apply_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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))
⊢ (↑((⋯.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)
have 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)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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))
⊢ 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)
have pos : ∀ (hk : k = 0),
  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: by_cases hk : k = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ 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)
have pos : HPow.hPow (β := ℤ) g
      (↑(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))))) :
        ℤ) *
    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_pos hk, if_pos hk, zpow_natCast]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ 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)
have 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)
Tactic: rw [if_neg hk, if_neg hk]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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)
⊢ 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)
have 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)
Tactic: rw [if_neg hk, if_neg hk]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ diff ϕ T (HSMul.hSMul (α := G) 1 T) = 1
have rw : diff ϕ T T = 1
Tactic: rw [one_smul, diff_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ diff ϕ T (HSMul.hSMul (α := G) 1 T) = 1
have rw₁ : Eq.{u_2 + 1} (α := A) 1 1
Tactic: rw [one_smul, diff_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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
⊢ diff ϕ T ((g * h) • T) = diff ϕ T (g • T) * diff ϕ T (h • T)
have rw : diff ϕ T (g • h • T) = diff ϕ T (g • T) * diff ϕ T (h • T)
Tactic: rw [mul_smul, ← diff_mul_diff, smul_diff_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
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)
⊢ diff ϕ T ((g * h) • T) = diff ϕ T (g • T) * diff ϕ T (h • T)
have rw₁ : diff ϕ T (g • T) * diff ϕ (g • T) (g • h • T) = diff ϕ T (g • T) * diff ϕ T (h • T)
Tactic: rw [mul_smul, ← diff_mul_diff, smul_diff_smul]