[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
R S T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
q : G ⧸ H
x✝ : q ∈ univ
⊢ {
        val :=
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
            ↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q),
        property :=
          (_ :
            (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
                ↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q) ∈
              H) } *
      {
        val :=
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q))⁻¹ *
            ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q),
        property :=
          (_ :
            (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q))⁻¹ *
                ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q) ∈
              H) } =
    {
      val :=
        (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
          ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q),
      property :=
        (_ :
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
              ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q) ∈
            H) }
[PROOFSTEP]
simp_rw [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
R S T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
x✝² : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
x✝¹ : G ⧸ H
x✝ : x✝¹ ∈ univ
⊢ {
      val :=
        (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • S) ∈ leftTransversals ↑H)) x✝¹))⁻¹ *
          ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • T) ∈ leftTransversals ↑H)) x✝¹),
      property :=
        (_ :
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • S) ∈ leftTransversals ↑H)) x✝¹))⁻¹ *
              ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • T) ∈ leftTransversals ↑H)) x✝¹) ∈
            H) } =
    {
      val :=
        (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)))⁻¹ *
          ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)),
      property :=
        (_ :
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)))⁻¹ *
              ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)) ∈
            H) }
[PROOFSTEP]
simp_rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
inst✝ : FiniteIndex H
T : ↑(leftTransversals ↑H) := default
⊢ (fun g => diff ϕ T (g • T)) 1 = 1
[PROOFSTEP]
simp only
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
inst✝ : FiniteIndex H
T : ↑(leftTransversals ↑H) := default
⊢ diff ϕ default (1 • default) = 1
[PROOFSTEP]
rw [one_smul, diff_self]
  -- porting note: added `simp only`
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
inst✝ : FiniteIndex H
T : ↑(leftTransversals ↑H) := default
g h : G
⊢ OneHom.toFun { toFun := fun g => diff ϕ T (g • T), map_one' := (_ : (fun g => diff ϕ T (g • T)) 1 = 1) } (g * h) =
    OneHom.toFun { toFun := fun g => diff ϕ T (g • T), map_one' := (_ : (fun g => diff ϕ T (g • T)) 1 = 1) } g *
      OneHom.toFun { toFun := fun g => diff ϕ T (g • T), map_one' := (_ : (fun g => diff ϕ T (g • T)) 1 = 1) } h
[PROOFSTEP]
simp only
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
inst✝ : FiniteIndex H
T : ↑(leftTransversals ↑H) := default
g h : G
⊢ diff ϕ default ((g * h) • default) = diff ϕ default (g • default) * diff ϕ default (h • default)
[PROOFSTEP]
rw [mul_smul, ← diff_mul_diff, smul_diff_smul]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
⊢ ↑(transfer ϕ) g = diff ϕ T (g • T)
[PROOFSTEP]
rw [transfer, ← diff_mul_diff, ← smul_diff_smul, mul_comm, diff_mul_diff]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
⊢ ↑(let T := default;
        {
          toOneHom :=
            { toFun := fun g => diff ϕ T (g • T), map_one' := (_ : (fun g => diff ϕ default (g • default)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (g h : G),
                OneHom.toFun
                    { toFun := fun g => diff ϕ default (g • default),
                      map_one' := (_ : (fun g => diff ϕ default (g • default)) 1 = 1) }
                    (g * h) =
                  OneHom.toFun
                      { toFun := fun g => diff ϕ default (g • default),
                        map_one' := (_ : (fun g => diff ϕ default (g • default)) 1 = 1) }
                      g *
                    OneHom.toFun
                      { toFun := fun g => diff ϕ default (g • default),
                        map_one' := (_ : (fun g => diff ϕ default (g • default)) 1 = 1) }
                      h) })
      g =
    diff ϕ ?R (g • ?R)
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
⊢ ↑(transfer ϕ) g =
    ∏ q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)),
      ↑ϕ
        {
          val :=
            (Quotient.out' (Quotient.out' q))⁻¹ *
                g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
              Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q) ∈
                H) }
[PROOFSTEP]
classical
letI := H.fintypeQuotientOfFiniteIndex
calc
  transfer ϕ g = ∏ q : G ⧸ H, _ := transfer_def ϕ (transferTransversal H g) g
  _ = _ := ((quotientEquivSigmaZMod H g).symm.prod_comp _).symm
  _ = _ := (Finset.prod_sigma _ _ _)
  _ = _ := by
    refine' Fintype.prod_congr _ _ (fun q => _)
    simp only [quotientEquivSigmaZMod_symm_apply, transferTransversal_apply', transferTransversal_apply'']
    rw [Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod ((· • ·) g) q.out')) _]
    · simp only [if_pos, ZMod.cast_zero, zpow_zero, one_mul, mul_assoc]
    · intro k hk
      simp only [if_neg hk, inv_mul_self]
      exact map_one ϕ
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
⊢ ↑(transfer ϕ) g =
    ∏ q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)),
      ↑ϕ
        {
          val :=
            (Quotient.out' (Quotient.out' q))⁻¹ *
                g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
              Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q) ∈
                H) }
[PROOFSTEP]
letI := H.fintypeQuotientOfFiniteIndex
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ ↑(transfer ϕ) g =
    ∏ q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)),
      ↑ϕ
        {
          val :=
            (Quotient.out' (Quotient.out' q))⁻¹ *
                g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
              Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q) ∈
                H) }
[PROOFSTEP]
calc
  transfer ϕ g = ∏ q : G ⧸ H, _ := transfer_def ϕ (transferTransversal H g) g
  _ = _ := ((quotientEquivSigmaZMod H g).symm.prod_comp _).symm
  _ = _ := (Finset.prod_sigma _ _ _)
  _ = _ := by
    refine' Fintype.prod_congr _ _ (fun q => _)
    simp only [quotientEquivSigmaZMod_symm_apply, transferTransversal_apply', transferTransversal_apply'']
    rw [Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod ((· • ·) g) q.out')) _]
    · simp only [if_pos, ZMod.cast_zero, zpow_zero, one_mul, mul_assoc]
    · intro k hk
      simp only [if_neg hk, inv_mul_self]
      exact map_one ϕ
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ ∏ a : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H),
      ∏ s in (fun x => Finset.univ) a,
        ↑ϕ
          {
            val :=
              (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(transferTransversal H g) ∈ leftTransversals ↑H))
                      (↑(quotientEquivSigmaZMod H g).symm { fst := a, snd := s })))⁻¹ *
                ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • transferTransversal H g) ∈ leftTransversals ↑H))
                    (↑(quotientEquivSigmaZMod H g).symm { fst := a, snd := s })),
            property :=
              (_ :
                (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(transferTransversal H g) ∈ leftTransversals ↑H))
                          (↑(quotientEquivSigmaZMod H g).symm { fst := a, snd := s })))⁻¹ *
                    ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • transferTransversal H g) ∈ leftTransversals ↑H))
                        (↑(quotientEquivSigmaZMod H g).symm { fst := a, snd := s })) ∈
                  H) } =
    ∏ q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)),
      ↑ϕ
        {
          val :=
            (Quotient.out' (Quotient.out' q))⁻¹ *
                g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
              Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q) ∈
                H) }
[PROOFSTEP]
refine' Fintype.prod_congr _ _ (fun q => _)
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
⊢ ∏ s in (fun x => Finset.univ) q,
      ↑ϕ
        {
          val :=
            (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(transferTransversal H g) ∈ leftTransversals ↑H))
                    (↑(quotientEquivSigmaZMod H g).symm { fst := q, snd := s })))⁻¹ *
              ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • transferTransversal H g) ∈ leftTransversals ↑H))
                  (↑(quotientEquivSigmaZMod H g).symm { fst := q, snd := s })),
          property :=
            (_ :
              (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(transferTransversal H g) ∈ leftTransversals ↑H))
                        (↑(quotientEquivSigmaZMod H g).symm { fst := q, snd := s })))⁻¹ *
                  ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • transferTransversal H g) ∈ leftTransversals ↑H))
                      (↑(quotientEquivSigmaZMod H g).symm { fst := q, snd := s })) ∈
                H) } =
    ↑ϕ
      {
        val :=
          (Quotient.out' (Quotient.out' q))⁻¹ *
              g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
            Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (Quotient.out' (Quotient.out' q))⁻¹ *
                  g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                Quotient.out' (Quotient.out' q) ∈
              H) }
[PROOFSTEP]
simp only [quotientEquivSigmaZMod_symm_apply, transferTransversal_apply', transferTransversal_apply'']
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
⊢ ∏ x : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out' q)),
      ↑ϕ
        {
          val :=
            (g ^ ↑x * Quotient.out' (Quotient.out' q))⁻¹ *
              if x = 0 then
                g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
              else g ^ ↑x * Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (fun x => x ∈ H)
                ((g ^ ↑x * Quotient.out' (Quotient.out' q))⁻¹ *
                  if x = 0 then
                    g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
                  else g ^ ↑x * Quotient.out' (Quotient.out' q))) } =
    ↑ϕ
      {
        val :=
          (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
            Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (Quotient.out' (Quotient.out' q))⁻¹ *
                  g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                Quotient.out' (Quotient.out' q) ∈
              H) }
[PROOFSTEP]
rw [Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod ((· • ·) g) q.out')) _]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
⊢ ↑ϕ
      {
        val :=
          (g ^ ↑0 * Quotient.out' (Quotient.out' q))⁻¹ *
            if 0 = 0 then
              g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
            else g ^ ↑0 * Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (fun x => x ∈ H)
              ((g ^ ↑0 * Quotient.out' (Quotient.out' q))⁻¹ *
                if 0 = 0 then
                  g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
                else g ^ ↑0 * Quotient.out' (Quotient.out' q))) } =
    ↑ϕ
      {
        val :=
          (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
            Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (Quotient.out' (Quotient.out' q))⁻¹ *
                  g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                Quotient.out' (Quotient.out' q) ∈
              H) }
[PROOFSTEP]
simp only [if_pos, ZMod.cast_zero, zpow_zero, one_mul, mul_assoc]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
⊢ ∀ (x : ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))),
    x ≠ 0 →
      ↑ϕ
          {
            val :=
              (g ^ ↑x * Quotient.out' (Quotient.out' q))⁻¹ *
                if x = 0 then
                  g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
                else g ^ ↑x * Quotient.out' (Quotient.out' q),
            property :=
              (_ :
                (fun x => x ∈ H)
                  ((g ^ ↑x * Quotient.out' (Quotient.out' q))⁻¹ *
                    if x = 0 then
                      g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
                    else g ^ ↑x * Quotient.out' (Quotient.out' q))) } =
        1
[PROOFSTEP]
intro k hk
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
hk : k ≠ 0
⊢ ↑ϕ
      {
        val :=
          (g ^ ↑k * Quotient.out' (Quotient.out' q))⁻¹ *
            if k = 0 then
              g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
            else g ^ ↑k * Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (fun x => x ∈ H)
              ((g ^ ↑k * Quotient.out' (Quotient.out' q))⁻¹ *
                if k = 0 then
                  g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q)
                else g ^ ↑k * Quotient.out' (Quotient.out' q))) } =
    1
[PROOFSTEP]
simp only [if_neg hk, inv_mul_self]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝¹ : FiniteIndex H
g : G
inst✝ : Fintype (Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
hk : k ≠ 0
⊢ ↑ϕ { val := 1, property := (_ : (fun x => x ∈ H) 1) } = 1
[PROOFSTEP]
exact map_one ϕ
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
⊢ g ^ index H ∈ H
[PROOFSTEP]
by_cases hH : H.index = 0
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : index H = 0
⊢ g ^ index H ∈ H
[PROOFSTEP]
rw [hH, pow_zero]
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : index H = 0
⊢ 1 ∈ H
[PROOFSTEP]
exact H.one_mem
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬index H = 0
⊢ g ^ index H ∈ H
[PROOFSTEP]
letI := fintypeOfIndexNeZero hH
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
⊢ g ^ index H ∈ H
[PROOFSTEP]
classical
replace key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H := fun k g₀ hk =>
  (_root_.congr_arg (· ∈ H) (key k g₀ hk)).mp hk
replace key : ∀ q : G ⧸ H, g ^ Function.minimalPeriod ((· • ·) g) q ∈ H := fun q =>
  key (Function.minimalPeriod ((· • ·) g) q) q.out' (QuotientGroup.out'_conj_pow_minimalPeriod_mem H g q)
let f : Quotient (orbitRel (zpowers g) (G ⧸ H)) → zpowers g := fun q =>
  (⟨g, mem_zpowers g⟩ : zpowers g) ^ Function.minimalPeriod ((· • ·) g) q.out'
have hf : ∀ q, f q ∈ H.subgroupOf (zpowers g) := fun q => key q.out'
replace key := Subgroup.prod_mem (H.subgroupOf (zpowers g)) fun q (_ : q ∈ Finset.univ) => hf q
simpa only [minimalPeriod_eq_card, Finset.prod_pow_eq_pow_sum, Fintype.card_sigma,
  Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)), index_eq_card] using key
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
⊢ g ^ index H ∈ H
[PROOFSTEP]
replace key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H := fun k g₀ hk =>
  (_root_.congr_arg (· ∈ H) (key k g₀ hk)).mp hk
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H
⊢ g ^ index H ∈ H
[PROOFSTEP]
replace key : ∀ q : G ⧸ H, g ^ Function.minimalPeriod ((· • ·) g) q ∈ H := fun q =>
  key (Function.minimalPeriod ((· • ·) g) q) q.out' (QuotientGroup.out'_conj_pow_minimalPeriod_mem H g q)
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (q : G ⧸ H), g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) q ∈ H
⊢ g ^ index H ∈ H
[PROOFSTEP]
let f : Quotient (orbitRel (zpowers g) (G ⧸ H)) → zpowers g := fun q =>
  (⟨g, mem_zpowers g⟩ : zpowers g) ^ Function.minimalPeriod ((· • ·) g) q.out'
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (q : G ⧸ H), g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) q ∈ H
f : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)) → { x // x ∈ zpowers g } :=
  fun q =>
    { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q)
⊢ g ^ index H ∈ H
[PROOFSTEP]
have hf : ∀ q, f q ∈ H.subgroupOf (zpowers g) := fun q => key q.out'
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (q : G ⧸ H), g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) q ∈ H
f : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)) → { x // x ∈ zpowers g } :=
  fun q =>
    { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q)
hf : ∀ (q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H))), f q ∈ subgroupOf H (zpowers g)
⊢ g ^ index H ∈ H
[PROOFSTEP]
replace key := Subgroup.prod_mem (H.subgroupOf (zpowers g)) fun q (_ : q ∈ Finset.univ) => hf q
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
A : Type u_2
inst✝ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
g : G
hH : ¬index H = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
f : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)) → { x // x ∈ zpowers g } :=
  fun q =>
    { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q)
hf : ∀ (q : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H))), f q ∈ subgroupOf H (zpowers g)
key : ∏ c : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H)), f c ∈ subgroupOf H (zpowers g)
⊢ g ^ index H ∈ H
[PROOFSTEP]
simpa only [minimalPeriod_eq_card, Finset.prod_pow_eq_pow_sum, Fintype.card_sigma,
  Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)), index_eq_card] using key
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
⊢ ↑(transfer ϕ) g = ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
classical
letI := H.fintypeQuotientOfFiniteIndex
change ∀ (k g₀) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑(⟨g₀⁻¹ * g ^ k * g₀, hk⟩ : H) = g ^ k at key 
rw [transfer_eq_prod_quotient_orbitRel_zpowers_quot, ← Finset.prod_to_list]
refine'
  (List.prod_map_hom _ _ _).trans
    _
      -- porting note: this used to be in the `rw`
refine' congrArg ϕ (Subtype.coe_injective _)
simp only
  -- porting note: added `simp only`
rw [H.coe_mk, ← (zpowers g).coe_mk g (mem_zpowers g), ← (zpowers g).coe_pow, index_eq_card,
  Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)), Fintype.card_sigma, ← Finset.prod_pow_eq_pow_sum, ←
  Finset.prod_to_list]
simp only [Subgroup.val_list_prod, List.map_map, ← minimalPeriod_eq_card]
congr
funext
apply key
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
⊢ ↑(transfer ϕ) g = ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
letI := H.fintypeQuotientOfFiniteIndex
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ ↑(transfer ϕ) g = ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
change ∀ (k g₀) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑(⟨g₀⁻¹ * g ^ k * g₀, hk⟩ : H) = g ^ k at key 
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ ↑(transfer ϕ) g = ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
rw [transfer_eq_prod_quotient_orbitRel_zpowers_quot, ← Finset.prod_to_list]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ List.prod
      (List.map
        (fun q =>
          ↑ϕ
            {
              val :=
                (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q),
              property :=
                (_ :
                  (Quotient.out' (Quotient.out' q))⁻¹ *
                        g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                      Quotient.out' (Quotient.out' q) ∈
                    H) })
        (Finset.toList Finset.univ)) =
    ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
refine'
  (List.prod_map_hom _ _ _).trans
    _
      -- porting note: this used to be in the `rw`
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ ↑ϕ
      (List.prod
        (List.map
          (fun q =>
            {
              val :=
                (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q),
              property :=
                (_ :
                  (Quotient.out' (Quotient.out' q))⁻¹ *
                        g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                      Quotient.out' (Quotient.out' q) ∈
                    H) })
          (Finset.toList Finset.univ))) =
    ↑ϕ { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
refine' congrArg ϕ (Subtype.coe_injective _)
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ (fun a => ↑a)
      (List.prod
        (List.map
          (fun q =>
            {
              val :=
                (Quotient.out' (Quotient.out' q))⁻¹ *
                    g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q),
              property :=
                (_ :
                  (Quotient.out' (Quotient.out' q))⁻¹ *
                        g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                      Quotient.out' (Quotient.out' q) ∈
                    H) })
          (Finset.toList Finset.univ))) =
    (fun a => ↑a) { val := g ^ index H, property := (_ : g ^ index H ∈ H) }
[PROOFSTEP]
simp only
  -- porting note: added `simp only`
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ ↑(List.prod
        (List.map
          (fun q =>
            {
              val :=
                (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q),
              property :=
                (_ :
                  (Quotient.out' (Quotient.out' q))⁻¹ *
                        g ^ Function.minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q) *
                      Quotient.out' (Quotient.out' q) ∈
                    H) })
          (Finset.toList Finset.univ))) =
    g ^ index H
[PROOFSTEP]
rw [H.coe_mk, ← (zpowers g).coe_mk g (mem_zpowers g), ← (zpowers g).coe_pow, index_eq_card,
  Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)), Fintype.card_sigma, ← Finset.prod_pow_eq_pow_sum, ←
  Finset.prod_to_list]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ ↑(List.prod
        (List.map
          (fun q =>
            {
              val :=
                (Quotient.out' (Quotient.out' q))⁻¹ *
                    ↑{ val := g, property := (_ : g ∈ zpowers g) } ^
                      Function.minimalPeriod (fun x => ↑{ val := g, property := (_ : g ∈ zpowers g) } • x)
                        (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q),
              property :=
                (_ :
                  (Quotient.out' (Quotient.out' q))⁻¹ *
                        ↑{ val := g, property := (_ : g ∈ zpowers g) } ^
                          Function.minimalPeriod ((fun x x_1 => x • x_1) ↑{ val := g, property := (_ : g ∈ zpowers g) })
                            (Quotient.out' q) *
                      Quotient.out' (Quotient.out' q) ∈
                    H) })
          (Finset.toList Finset.univ))) =
    ↑(List.prod
        (List.map
          (fun i =>
            { val := g, property := (_ : g ∈ zpowers g) } ^
              Fintype.card ↑(orbit { x // x ∈ zpowers g } (Quotient.out' i)))
          (Finset.toList Finset.univ)))
[PROOFSTEP]
simp only [Subgroup.val_list_prod, List.map_map, ← minimalPeriod_eq_card]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ List.prod
      (List.map
        (Subtype.val ∘ fun q =>
          {
            val :=
              (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
                Quotient.out' (Quotient.out' q),
            property :=
              (_ :
                (Quotient.out' (Quotient.out' q))⁻¹ *
                      ↑{ val := g, property := (_ : g ∈ zpowers g) } ^
                        Function.minimalPeriod ((fun x x_1 => x • x_1) ↑{ val := g, property := (_ : g ∈ zpowers g) })
                          (Quotient.out' q) *
                    Quotient.out' (Quotient.out' q) ∈
                  H) })
        (Finset.toList Finset.univ)) =
    List.prod
      (List.map
        (Subtype.val ∘ fun i =>
          { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' i))
        (Finset.toList Finset.univ))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
⊢ (Subtype.val ∘ fun q =>
      {
        val :=
          (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
            Quotient.out' (Quotient.out' q),
        property :=
          (_ :
            (Quotient.out' (Quotient.out' q))⁻¹ *
                  ↑{ val := g, property := (_ : g ∈ zpowers g) } ^
                    Function.minimalPeriod ((fun x x_1 => x • x_1) ↑{ val := g, property := (_ : g ∈ zpowers g) })
                      (Quotient.out' q) *
                Quotient.out' (Quotient.out' q) ∈
              H) }) =
    Subtype.val ∘ fun i =>
      { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' i)
[PROOFSTEP]
funext
[GOAL]
case e_a.e_f.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑{ val := g₀⁻¹ * g ^ k * g₀, property := hk } = g ^ k
x✝ : Quotient (orbitRel { x // x ∈ zpowers g } (G ⧸ H))
⊢ (Subtype.val ∘ fun q =>
        {
          val :=
            (Quotient.out' (Quotient.out' q))⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) *
              Quotient.out' (Quotient.out' q),
          property :=
            (_ :
              (Quotient.out' (Quotient.out' q))⁻¹ *
                    ↑{ val := g, property := (_ : g ∈ zpowers g) } ^
                      Function.minimalPeriod ((fun x x_1 => x • x_1) ↑{ val := g, property := (_ : g ∈ zpowers g) })
                        (Quotient.out' q) *
                  Quotient.out' (Quotient.out' q) ∈
                H) })
      x✝ =
    (Subtype.val ∘ fun i =>
        { val := g, property := (_ : g ∈ zpowers g) } ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' i))
      x✝
[PROOFSTEP]
apply key
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex (center G)
g : G
k : ℕ
x✝ : G
hk : x✝⁻¹ * g ^ k * x✝ ∈ center G
⊢ x✝⁻¹ * g ^ k * x✝ = g ^ k
[PROOFSTEP]
rw [← mul_right_inj, hk, mul_inv_cancel_right]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex (center G)
a b : G
⊢ OneHom.toFun
      { toFun := fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) },
        map_one' :=
          (_ : (fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) }) 1 = 1) }
      (a * b) =
    OneHom.toFun
        { toFun := fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) },
          map_one' :=
            (_ : (fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) }) 1 = 1) }
        a *
      OneHom.toFun
        { toFun := fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) },
          map_one' :=
            (_ : (fun g => { val := g ^ index (center G), property := (_ : g ^ index (center G) ∈ center G) }) 1 = 1) }
        b
[PROOFSTEP]
simp_rw [← show ∀ _, (_ : center G) = _ from transfer_center_eq_pow, map_mul]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
[PROOFSTEP]
haveI : (P : Subgroup G).IsCommutative := ⟨⟨fun a b => Subtype.ext (hP (le_normalizer b.2) a a.2)⟩⟩
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
[PROOFSTEP]
replace hg := (P : Subgroup G).pow_mem hg k
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
hg : g ^ k ∈ ↑P
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
[PROOFSTEP]
obtain ⟨n, hn, h⟩ := P.conj_eq_normalizer_conj_of_mem (g ^ k) g₀ hg h
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
g : G
k : ℕ
g₀ : G
h✝ : g₀⁻¹ * g ^ k * g₀ ∈ P
this : Subgroup.IsCommutative ↑P
hg : g ^ k ∈ ↑P
n : G
hn : n ∈ normalizer ↑P
h : g₀⁻¹ * g ^ k * g₀ = n⁻¹ * g ^ k * n
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k
[PROOFSTEP]
exact h.trans (Commute.inv_mul_cancel (hP hn (g ^ k) hg).symm)
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type u_2
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
[PROOFSTEP]
have hf : Function.Bijective ((transferSylow P hP).restrict (P : Subgroup G)) :=
  (transferSylow_restrict_eq_pow P hP).symm ▸
    (P.2.powEquiv' (not_dvd_index_sylow P (mt index_eq_zero_of_relindex_eq_zero index_ne_zero_of_finite))).bijective
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type u_2
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Bijective ↑(restrict (transferSylow P hP) ↑P)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
[PROOFSTEP]
rw [Function.Bijective, ← range_top_iff_surjective, restrict_range] at hf 
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type u_2
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
[PROOFSTEP]
have := range_top_iff_surjective.mp (top_le_iff.mp (hf.2.ge.trans (map_le_range (transferSylow P hP) P)))
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type u_2
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
this : Function.Surjective ↑(transferSylow P hP)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
[PROOFSTEP]
rw [← (comap_injective this).eq_iff, comap_top, comap_map_eq, sup_comm, SetLike.ext'_iff, normal_mul, ← ker_eq_bot_iff,
  ← (map_injective (P : Subgroup G).subtype_injective).eq_iff, ker_restrict, subgroupOf_map_subtype, Subgroup.map_bot,
  coe_top] at hf 
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type u_2
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf✝ : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ ker (transferSylow P hP) ⊔ ↑P = ⊤
hf : ker (transferSylow P hP) ⊓ ↑P = ⊥ ∧ ↑(ker (transferSylow P hP)) * ↑↑P = Set.univ
this : Function.Surjective ↑(transferSylow P hP)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
[PROOFSTEP]
exact isComplement'_of_disjoint_and_mul_eq_univ (disjoint_iff.2 hf.1) hf.2
