-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst_3 : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst_4 : Algebra.IsUnramifiedAt R Q
inst_5 : IsNoetherianRing S
x : Localization.AtPrime Q
rw :
  HPow.hPow (α :=
      HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
        (maximalIdeal (Localization.AtPrime Q)))
      ((Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q)) :
            (a : Localization.AtPrime Q) → Localization.AtPrime Q ⧸ maximalIdeal (Localization.AtPrime Q))
          x :
        HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
          (maximalIdeal (Localization.AtPrime Q)))
      (Nat.card.{u_1}
        (HasQuotient.Quotient R (B := Ideal R)
          (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (maximalIdeal (Localization.AtPrime Q))))) =
    (Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q)) :
        (a : Localization.AtPrime Q) → Localization.AtPrime Q ⧸ maximalIdeal (Localization.AtPrime Q))
      ((H'.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q) x)
⊢ Eq (α :=
    HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
      (maximalIdeal (Localization.AtPrime Q)))
    ((Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q)) :
          (a : Localization.AtPrime Q) → Localization.AtPrime Q ⧸ maximalIdeal (Localization.AtPrime Q))
        ((H.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q) x) :
      HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
        (maximalIdeal (Localization.AtPrime Q)))
    ((Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q)) :
          (a : Localization.AtPrime Q) → Localization.AtPrime Q ⧸ maximalIdeal (Localization.AtPrime Q))
        ((H'.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q) x) :
      HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
        (maximalIdeal (Localization.AtPrime Q)))
have rw₁ : HPow.hPow (α :=
    HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
      (maximalIdeal (Localization.AtPrime Q)))
    ((Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q)) :
          (a : Localization.AtPrime Q) → Localization.AtPrime Q ⧸ maximalIdeal (Localization.AtPrime Q))
        x :
      HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
        (maximalIdeal (Localization.AtPrime Q)))
    (Nat.card.{u_1}
      (HasQuotient.Quotient R (B := Ideal R)
        (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (maximalIdeal (Localization.AtPrime Q))))) =
  HPow.hPow (α :=
    HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
      (maximalIdeal (Localization.AtPrime Q)))
    ((Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q)) :
          (a : Localization.AtPrime Q) → Localization.AtPrime Q ⧸ maximalIdeal (Localization.AtPrime Q))
        x :
      HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
        (maximalIdeal (Localization.AtPrime Q)))
    (Nat.card.{u_1}
      (HasQuotient.Quotient R (B := Ideal R)
        (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (maximalIdeal (Localization.AtPrime Q)))))
Tactic: rw [H.isArithFrobAt_localize.mk_apply, H'.isArithFrobAt_localize.mk_apply]