-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a : FractionRing (𝕎 k)
q : 𝕎 k
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) q
hq0 : q ≠ 0
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hrq :
  Ne (α := FractionRing (𝕎 k))
    (Localization.mk
      (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).1
      (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).2)
    0
hr0 : HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r' ≠ 0
⊢ ∃ (b : FractionRing (𝕎 k)),
    b ≠ 0 ∧
      ∃ (m_1 : ℤ),
        HMul.hMul (α := FractionRing (𝕎 k)) (β := FractionRing (𝕎 k))
            ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
                  (a : FractionRing (𝕎 k)) → FractionRing (𝕎 k))
                b :
              FractionRing (𝕎 k))
            (Localization.mk
              (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
                  Subtype.mk (p := fun (x : 𝕎 k) ↦
                    Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).1
              (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
                  Subtype.mk (p := fun (x : 𝕎 k) ↦
                    Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).2) =
          HPow.hPow (α := FractionRing (𝕎 k)) (↑p : FractionRing (𝕎 k)) m_1 * b
have obtain : ∀ (n : ℕ) (q' : 𝕎 k) (hq' : q'.coeff 0 ≠ 0)
  (hq :
    Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k))
      (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q'))
  (hq0 : HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q' ≠ 0)
  (hrq :
    Ne (α := FractionRing (𝕎 k))
      (Localization.mk
        (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
            Subtype.mk (p := fun (x : 𝕎 k) ↦
              Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
              (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq).1
        (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
            Subtype.mk (p := fun (x : 𝕎 k) ↦
              Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
              (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq).2)
      0),
  ∃ (b : FractionRing (𝕎 k)),
    b ≠ 0 ∧
      ∃ (m_1 : ℤ),
        HMul.hMul (α := FractionRing (𝕎 k)) (β := FractionRing (𝕎 k))
            ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
                  (a : FractionRing (𝕎 k)) → FractionRing (𝕎 k))
                b :
              FractionRing (𝕎 k))
            (Localization.mk
              (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
                  Subtype.mk (p := fun (x : 𝕎 k) ↦
                    Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
                    (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq).1
              (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
                  Subtype.mk (p := fun (x : 𝕎 k) ↦
                    Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
                    (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq).2) =
          HPow.hPow (α := FractionRing (𝕎 k)) (↑p : FractionRing (𝕎 k)) m_1 * b
Tactic: obtain ⟨n, q', hq', rfl⟩ := exists_eq_pow_p_mul q hq0
Cleared hypotheses: q, hq, hq0, hrq