awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key :
  ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k
refine :
  Eq.{u_1 + 1} (α := G)
    ((fun (a : ↥H) ↦ (↑a : G))
      (List.prod
        (List.map
          (fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
            Subtype.mk (p := fun (x : G) ↦ x ∈ H)
              ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out * Quotient.out q.out)
              ⋯)
          (Finset.toList Finset.univ))))
    ((fun (a : ↥H) ↦ (↑a : G)) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g ^ H.index) ⋯))
⊢ Eq.{u_2 + 1} (α := A)
    ((ϕ : (a : ↥H) → A)
        (List.prod
          (List.map
            (fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
              Subtype.mk (p := fun (x : G) ↦ x ∈ H)
                ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out *
                  Quotient.out q.out)
                ⋯)
            (Finset.toList Finset.univ))) :
      A)
    ((ϕ : (a : ↥H) → A) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g ^ H.index) ⋯) : A)

Tactic:
refine congrArg ϕ (Subtype.coe_injective ?_)

Premises used: congrArg, Subtype.coe_injective, DFunLike.coe
-- 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
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key :
  ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k
dsimp :
  (↑(List.prod
          (List.map
            (fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
              Subtype.mk (p := fun (x : G) ↦ x ∈ H)
                ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out *
                  Quotient.out q.out)
                ⋯)
            (Finset.toList Finset.univ))) :
      G) =
    g ^ H.index
⊢ Eq.{u_1 + 1} (α := G)
    ((fun (a : ↥H) ↦ (↑a : G))
      (List.prod
        (List.map
          (fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
            Subtype.mk (p := fun (x : G) ↦ x ∈ H)
              ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out * Quotient.out q.out)
              ⋯)
          (Finset.toList Finset.univ))))
    ((fun (a : ↥H) ↦ (↑a : G)) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g ^ H.index) ⋯))

Tactic:
dsimp only
-- 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
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key :
  ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k
rw :
  Eq.{u_1 + 1} (α := G)
    (↑(List.prod
          (List.map
            (fun
                (q :
                  Quotient (α := G ⧸ H)
                    (orbitRel
                      (↥(zpowers
                          (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯) : G)))
                      (G ⧸ H))) ↦
              Subtype.mk (p := fun (x : G) ↦ x ∈ H)
                ((Quotient.out q.out)⁻¹ *
                    (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯) : G) ^
                      Function.minimalPeriod
                        (fun (x : G ⧸ H) ↦
                          (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯) : G) •
                            x)
                        q.out *
                  Quotient.out q.out)
                ⋯)
            (Finset.toList Finset.univ))) :
      G)
    (↑(List.prod
          (List.map
            (fun (i : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
              HPow.hPow (α := ↥(zpowers g))
                (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯)
                (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
            (Finset.toList Finset.univ))) :
      G)
⊢ (↑(List.prod
          (List.map
            (fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
              Subtype.mk (p := fun (x : G) ↦ x ∈ H)
                ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out *
                  Quotient.out q.out)
                ⋯)
            (Finset.toList Finset.univ))) :
      G) =
    g ^ H.index

Tactic:
rw [H.coe_mk, ← (zpowers g).coe_mk g (mem_zpowers g), ← (zpowers g).coe_pow,
      index_eq_sum_minimalPeriod H g, ← Finset.prod_pow_eq_pow_sum, ← Finset.prod_map_toList]

Premises used: Subgroup.coe_mk, Finset.prod_map_toList, Subgroup.index_eq_sum_minimalPeriod, Subgroup.coe_pow, Subgroup.mem_zpowers, Finset.prod_pow_eq_pow_sum, Subgroup.zpowers
-- 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
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key :
  ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k
simp :
  Eq.{u_1 + 1} (α := G)
    (List.prod
      (List.map (α := Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
        (Function.comp (β := ↥H) (Subtype.val (p := fun (x : G) ↦ x ∈ H))
          fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
          Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out * Quotient.out q.out)
            ⋯)
        (Finset.toList Finset.univ)))
    (List.prod
      (List.map (α := Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
        (Function.comp (β := ↥(zpowers g))
          (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x))
          fun (i : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
          HPow.hPow (α := ↥(zpowers g))
            (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯)
            (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
        (Finset.toList Finset.univ)))
⊢ Eq.{u_1 + 1} (α := G)
    (↑(List.prod
          (List.map
            (fun
                (q :
                  Quotient (α := G ⧸ H)
                    (orbitRel
                      (↥(zpowers
                          (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯) : G)))
                      (G ⧸ H))) ↦
              Subtype.mk (p := fun (x : G) ↦ x ∈ H)
                ((Quotient.out q.out)⁻¹ *
                    (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯) : G) ^
                      Function.minimalPeriod
                        (fun (x : G ⧸ H) ↦
                          (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯) : G) •
                            x)
                        q.out *
                  Quotient.out q.out)
                ⋯)
            (Finset.toList Finset.univ))) :
      G)
    (↑(List.prod
          (List.map
            (fun (i : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
              HPow.hPow (α := ↥(zpowers g))
                (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯)
                (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
            (Finset.toList Finset.univ))) :
      G)

Tactic:
simp only [Subgroup.val_list_prod, List.map_map]

Premises used: Subgroup.val_list_prod, List.map_map
-- 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
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key :
  ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k
e_xs :
  Eq.{u_1 + 1} (α := Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)) → G)
    (Function.comp (β := ↥H) (Subtype.val (p := fun (x : G) ↦ x ∈ H))
      fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
      Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out * Quotient.out q.out) ⋯)
    (Function.comp (β := ↥(zpowers g)) (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x))
      fun (i : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
      HPow.hPow (α := ↥(zpowers g)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯)
        (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
⊢ Eq.{u_1 + 1} (α := G)
    (List.prod
      (List.map (α := Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
        (Function.comp (β := ↥H) (Subtype.val (p := fun (x : G) ↦ x ∈ H))
          fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
          Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out * Quotient.out q.out)
            ⋯)
        (Finset.toList Finset.univ)))
    (List.prod
      (List.map (α := Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
        (Function.comp (β := ↥(zpowers g))
          (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x))
          fun (i : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
          HPow.hPow (α := ↥(zpowers g))
            (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯)
            (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
        (Finset.toList Finset.univ)))

Tactic:
congr 2
-- 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
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key :
  ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k
e_xs :
  ∀ (x : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))),
    Eq (α := G)
      (Function.comp (β := ↥H) (Subtype.val (p := fun (x : G) ↦ x ∈ H))
        (fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
          Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out * Quotient.out q.out)
            ⋯)
        x)
      (Function.comp (β := ↥(zpowers g))
        (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x))
        (fun (i : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
          HPow.hPow (α := ↥(zpowers g))
            (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯)
            (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
        x)
⊢ Eq.{u_1 + 1} (α := Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)) → G)
    (Function.comp (β := ↥H) (Subtype.val (p := fun (x : G) ↦ x ∈ H))
      fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
      Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out * Quotient.out q.out) ⋯)
    (Function.comp (β := ↥(zpowers g)) (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x))
      fun (i : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
      HPow.hPow (α := ↥(zpowers g)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯)
        (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))

Tactic:
funext
-- 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
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key :
  ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H),
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g₀⁻¹ * g ^ k * g₀) hk) : G) = g ^ k
x : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))
⊢ Eq (α := G)
    (Function.comp (β := ↥H) (Subtype.val (p := fun (x : G) ↦ x ∈ H))
      (fun (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
        Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          ((Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out * Quotient.out q.out) ⋯)
      x)
    (Function.comp (β := ↥(zpowers g)) (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x))
      (fun (i : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) ↦
        HPow.hPow (α := ↥(zpowers g))
          (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) g ⋯)
          (Function.minimalPeriod (fun (x : G ⧸ H) ↦ g • x) i.out))
      x)

Tactic:
apply key
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
inst_1 : FiniteIndex (center G)
g : G
k : ℕ
x : G
hk : Membership.mem (γ := Subgroup G) (center G) (x⁻¹ * g ^ k * x)
rw : x⁻¹ * (x⁻¹ * g ^ k * x) = x⁻¹ * g ^ k
a : G
rw₁ : x⁻¹ * g ^ k * x * x⁻¹ = x⁻¹ * g ^ k
rw₂ : G
rw₃ rw₄ : x⁻¹ * g ^ k = x⁻¹ * g ^ k
⊢ x⁻¹ * g ^ k * x = g ^ k

Tactic:
rw [← mul_right_inj, ← hk.comm,
    mul_inv_cancel_right]

Premises used: mul_inv_cancel_right, IsMulCentral.comm, mul_right_inj
-- 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 : FiniteIndex (center G)
a b : G
simp_rw :
  (transfer (id ↥(center G)) : (a : G) → ↥(center G)) (a * b) =
    HMul.hMul (α := ↥(center G)) (β := ↥(center G))
      ((transfer (id ↥(center G)) : (a : G) → ↥(center G)) a : ↥(center G))
      ((transfer (id ↥(center G)) : (a : G) → ↥(center G)) b : ↥(center G))
⊢ Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (center G) x) ((a * b) ^ index (center G)) ⋯ =
    Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (center G) x) (a ^ index (center G)) ⋯ *
      Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (center G) x) (b ^ index (center G)) ⋯

Tactic:
simp_rw [← show ∀ _, (_ : center G) = _ from transfer_center_eq_pow, map_mul]

Premises used: MonoidHom.transfer_center_eq_pow, map_mul
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
inst_1 : FiniteIndex (center G)
g : G
⊢ (↑((transferCenterPow G : (a : G) → ↥(center G)) g) : G) = g ^ index (center G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
⊢ IsMulCommutative.{u_1} ↥(↑P : Subgroup G)

Tactic:
haveI : IsMulCommutative P :=
    ⟨⟨fun a b => Subtype.ext (hP (le_normalizer b.2) a a.2)⟩⟩
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
g : G
hg : g ∈ P
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : IsMulCommutative.{u_1} ↥(↑P : Subgroup G)
⊢ g ^ k ∈ (↑P : Subgroup G)

Tactic:
replace hg := P.pow_mem hg k
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
g : G
k : ℕ
g₀ : G
h : g₀⁻¹ * g ^ k * g₀ ∈ P
this : IsMulCommutative.{u_1} ↥(↑P : Subgroup G)
hg : g ^ k ∈ (↑P : Subgroup G)
obtain :
  ∀ (n : G) (hn : Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n)
    (h : g₀⁻¹ * g ^ k * g₀ = n⁻¹ * g ^ k * n), g₀⁻¹ * g ^ k * g₀ = g ^ k
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Tactic:
obtain ⟨n, hn, h⟩ := P.conj_eq_normalizer_conj_of_mem (g ^ k) g₀ hg h

Premises used: Sylow.conj_eq_normalizer_conj_of_mem, HPow.hPow
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
g : G
k : ℕ
g₀ : G
h_1 : g₀⁻¹ * g ^ k * g₀ ∈ P
this : IsMulCommutative.{u_1} ↥(↑P : Subgroup G)
hg : g ^ k ∈ (↑P : Subgroup G)
n : G
hn : Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n
h : g₀⁻¹ * g ^ k * g₀ = n⁻¹ * g ^ k * n
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Tactic:
h.trans (Commute.inv_mul_cancel (hP hn (g ^ k) hg).symm)

Premises used: Commute.inv_mul_cancel, HPow.hPow, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
g : G
k : ℕ
g₀ : G
h_1 : g₀⁻¹ * g ^ k * g₀ ∈ P
this : IsMulCommutative.{u_1} ↥(↑P : Subgroup G)
hg : g ^ k ∈ (↑P : Subgroup G)
n : G
hn : Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n
h : g₀⁻¹ * g ^ k * g₀ = n⁻¹ * g ^ k * n
⊢ g₀⁻¹ * g ^ k * g₀ = g ^ k

Tactic:
exact h.trans (Commute.inv_mul_cancel (hP hn (g ^ k) hg).symm)

Premises used: Commute.inv_mul_cancel, HPow.hPow, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
inst_3 : (↑P : Subgroup G).FiniteIndex
g : G
hg : g ∈ P
⊢ (transferSylow P hP : (a : G) → ↥(↑P : Subgroup G)) g =
    Subtype.mk (p := fun (x : G) ↦ x ∈ (↑P : Subgroup G)) (g ^ (↑P : Subgroup G).index) ⋯

Tactic:
haveI : IsMulCommutative P := ⟨⟨fun a b => Subtype.ext (hP (le_normalizer b.2) a a.2)⟩⟩
  transfer_eq_pow _ _ <| transferSylow_eq_pow_aux P hP g hg

Premises used: Sylow.toSubgroup, Membership.mem, Subtype, MonoidHom.id, MonoidHom.transferSylow_eq_pow_aux, MonoidHom.transfer_eq_pow
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
inst_3 : (↑P : Subgroup G).FiniteIndex
⊢ Eq (α := (a : ↥P) → ↥(↑P : Subgroup G)) (⇑((transferSylow P hP).restrict P) : (a : ↥P) → ↥(↑P : Subgroup G))
    fun (x : ↥P) ↦ x ^ (↑P : Subgroup G).index

Tactic:
funext fun g => transferSylow_eq_pow P hP g g.2

Premises used: MonoidHom.transferSylow_eq_pow, funext, Subtype.val, Subtype.property
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
inst_3 : (↑P : Subgroup G).FiniteIndex
⊢ Function.Bijective (α := ↥(↑P : Subgroup G)) (β := ↥(↑P : Subgroup G))
    (⇑((transferSylow P hP).restrict (↑P : Subgroup G)) : (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G))

Tactic:
have hf : Function.Bijective ((transferSylow P hP).restrict (P : Subgroup G)) :=
    (transferSylow_restrict_eq_pow P hP).symm ▸ (P.2.powEquiv' P.not_dvd_index).bijective
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
inst_3 : (↑P : Subgroup G).FiniteIndex
hf :
  Function.Bijective (α := ↥(↑P : Subgroup G)) (β := ↥(↑P : Subgroup G))
    (⇑((transferSylow P hP).restrict (↑P : Subgroup G)) : (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G))
⊢ Function.Injective (α := ↥(↑P : Subgroup G)) (β := ↥(↑P : Subgroup G))
      (⇑((transferSylow P hP).restrict (↑P : Subgroup G)) : (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G)) ∧
    map (transferSylow P hP) (↑P : Subgroup G) = ⊤

Tactic:
rw [Function.Bijective, ← range_eq_top, restrict_range] at hf

Premises used: MonoidHom.restrict_range, MonoidHom.range_eq_top, Function.Bijective
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
inst_3 : (↑P : Subgroup G).FiniteIndex
hf :
  Function.Injective (α := ↥(↑P : Subgroup G)) (β := ↥(↑P : Subgroup G))
      (⇑((transferSylow P hP).restrict (↑P : Subgroup G)) : (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G)) ∧
    map (transferSylow P hP) (↑P : Subgroup G) = ⊤
⊢ Function.Surjective (α := G) (β := ↥(↑P : Subgroup G)) (⇑(transferSylow P hP) : (a : G) → ↥(↑P : Subgroup G))

Tactic:
have := range_eq_top.mp (top_le_iff.mp (hf.2.ge.trans
    (map_le_range (transferSylow P hP) P)))
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
inst_3 : (↑P : Subgroup G).FiniteIndex
hf :
  Function.Injective (α := ↥(↑P : Subgroup G)) (β := ↥(↑P : Subgroup G))
      (⇑((transferSylow P hP).restrict (↑P : Subgroup G)) : (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G)) ∧
    map (transferSylow P hP) (↑P : Subgroup G) = ⊤
this : Function.Surjective (α := G) (β := ↥(↑P : Subgroup G)) (⇑(transferSylow P hP) : (a : G) → ↥(↑P : Subgroup G))
⊢ (transferSylow P hP).ker ⊓ (↑P : Subgroup G) = ⊥ ∧
    (↑(transferSylow P hP).ker : Set G) * (↑(↑P : Subgroup G) : Set G) = Set.univ

Tactic:
rw [← (comap_injective this).eq_iff, comap_top, comap_map_eq, sup_comm, SetLike.ext'_iff,
    normal_mul, ← ker_eq_bot_iff, ← map_subtype_inj,
    ker_restrict, subgroupOf_map_subtype, Subgroup.map_bot, coe_top] at hf

Premises used: Subgroup.map_subtype_inj, Subgroup.comap_injective, Function.Injective.eq_iff, Subgroup.coe_top, Subgroup.map_bot, Subgroup.normal_mul, Subgroup.comap_map_eq, Subgroup.subgroupOf_map_subtype, sup_comm, MonoidHom.ker_eq_bot_iff, SetLike.ext'_iff, Subgroup.comap_top, MonoidHom.ker_restrict
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_1
inst : Group G
p : ℕ
P : Sylow p G
hP : LE.le (α := Subgroup G) (normalizer (↑P : Set G)) (centralizer (↑P : Set G))
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
inst_3 : (↑P : Subgroup G).FiniteIndex
hf :
  Function.Injective (α := ↥(↑P : Subgroup G)) (β := ↥(↑P : Subgroup G))
      (⇑((transferSylow P hP).restrict (↑P : Subgroup G)) : (a : ↥(↑P : Subgroup G)) → ↥(↑P : Subgroup G)) ∧
    map (transferSylow P hP) (↑P : Subgroup G) = ⊤
this : Function.Surjective (α := G) (β := ↥(↑P : Subgroup G)) (⇑(transferSylow P hP) : (a : G) → ↥(↑P : Subgroup G))
hf₁ :
  (transferSylow P hP).ker ⊓ (↑P : Subgroup G) = ⊥ ∧
    (↑(transferSylow P hP).ker : Set G) * (↑(↑P : Subgroup G) : Set G) = Set.univ
⊢ Function.Surjective (α := G) (β := ↥(↑P : Subgroup G)) (⇑(transferSylow P hP) : (a : G) → ↥(↑P : Subgroup G))

Tactic:
rw [← (comap_injective this).eq_iff, comap_top, comap_map_eq, sup_comm, SetLike.ext'_iff,
    normal_mul, ← ker_eq_bot_iff, ← map_subtype_inj,
    ker_restrict, subgroupOf_map_subtype, Subgroup.map_bot, coe_top] at hf

Premises used: Subgroup.map_subtype_inj, Subgroup.comap_injective, Function.Injective.eq_iff, Subgroup.coe_top, Subgroup.map_bot, Subgroup.normal_mul, Subgroup.comap_map_eq, Subgroup.subgroupOf_map_subtype, sup_comm, MonoidHom.ker_eq_bot_iff, SetLike.ext'_iff, Subgroup.comap_top, MonoidHom.ker_restrict