-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
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
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
⊢ ∃ (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

Tactic:
obtain ⟨n, q', hq', rfl⟩ := exists_eq_pow_p_mul q hq0

Premises used: WittVector.exists_eq_pow_p_mul, rfl