-- 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)
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hr0 : HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r' ≠ 0
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 : 𝕎 k := frobeniusRotation p hr' hq'
refine_1 :
  Ne (α := FractionRing (𝕎 k))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))
    (0 : FractionRing (𝕎 k))
refine_2 :
  HMul.hMul (α := FractionRing (𝕎 k)) (β := FractionRing (𝕎 k))
      ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
            (a : FractionRing (𝕎 k)) → FractionRing (𝕎 k))
          ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 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) =
    HMul.hMul (β := FractionRing (𝕎 k))
      (HPow.hPow (α := FractionRing (𝕎 k)) (↑p : FractionRing (𝕎 k)) (HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))
⊢ ∃ (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:
refine ⟨algebraMap (𝕎 k) (FractionRing (𝕎 k)) b, ?_, m - n, ?_⟩