-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
x g : G
hx : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) x
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
z : G
hz : z ∈ (↑(↑P : Subgroup G) : Set G)
hy : z * (g⁻¹ * x * g) = g⁻¹ * x * g * z
rwa :
  ∀ (hy : z * (g⁻¹ * x) * g = g⁻¹ * x * g * z),
    HMul.hMul (α := G)
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            z :
          G)
        x =
      HMul.hMul (β := G) x
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            z :
          G)
rwa₁ :
  ∀ (hy : z * (g⁻¹ * x) = g⁻¹ * x * g * z * g⁻¹),
    HMul.hMul (α := G)
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            z :
          G)
        x =
      HMul.hMul (β := G) x
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            z :
          G)
rwa₂ :
  ∀ (hy : z * (g⁻¹ * x) = g⁻¹ * x * g * (z * g⁻¹)),
    HMul.hMul (α := G)
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            z :
          G)
        x =
      HMul.hMul (β := G) x
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            z :
          G)
rwa₃ :
  ∀ (hy : z * (g⁻¹ * x) = g⁻¹ * x * (g * (z * g⁻¹))),
    HMul.hMul (α := G)
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            z :
          G)
        x =
      HMul.hMul (β := G) x
        ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                  ((MulAut.conj : (a : G) → MulAut G) g) :
                Monoid.End G) :
              (a : G) → G)
            z :
          G)
⊢ HMul.hMul (α := G)
      ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                ((MulAut.conj : (a : G) → MulAut G) g) :
              Monoid.End G) :
            (a : G) → G)
          z :
        G)
      x =
    HMul.hMul (β := G) x
      ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                ((MulAut.conj : (a : G) → MulAut G) g) :
              Monoid.End G) :
            (a : G) → G)
          z :
        G)
have rwa₄ : ∀ (hy : z * (g⁻¹ * x) = g⁻¹ * (x * (g * (z * g⁻¹)))),
  HMul.hMul (α := G)
      ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                ((MulAut.conj : (a : G) → MulAut G) g) :
              Monoid.End G) :
            (a : G) → G)
          z :
        G)
      x =
    HMul.hMul (β := G) x
      ((((MulDistribMulAction.toMonoidEnd (MulAut G) G : (a : MulAut G) → Monoid.End G)
                ((MulAut.conj : (a : G) → MulAut G) g) :
              Monoid.End G) :
            (a : G) → G)
          z :
        G)
Tactic: rwa [← mul_assoc, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_assoc, mul_assoc, ← mul_assoc,
      eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc] at hy
Cleared hypotheses: hy