awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k)) (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q')
b : 𝕎 k := frobeniusRotation p hr' hq'
key : HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r' = q' * b
hq'' :
  Ne (α := FractionRing (𝕎 k))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
    (0 : FractionRing (𝕎 k))
simp :
  HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) :
            (a : 𝕎 k) → Localization (nonZeroDivisors (𝕎 k)))
          ((frobenius : (a : 𝕎 k) → 𝕎 k) b) :
        Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) r' : FractionRing (𝕎 k)) =
    HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))
⊢ HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
            (a : FractionRing (𝕎 k)) → Localization (nonZeroDivisors (𝕎 k)))
          ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b) :
        Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 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)) =
    HMul.hMul (β := FractionRing (𝕎 k))
      (HPow.hPow (α := FractionRing (𝕎 k)) (β := ℤ) (↑p : FractionRing (𝕎 k)) (↑m : ℤ) /
        HPow.hPow (α := FractionRing (𝕎 k)) (β := ℤ) (↑p : FractionRing (𝕎 k)) (↑n : ℤ))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))

Tactic:
simp [field, FractionRing.p_nonzero p k]

Premises used: WittVector.FractionRing.p_nonzero
-- 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
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k)) (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q')
b : 𝕎 k := frobeniusRotation p hr' hq'
key : HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r' = q' * b
hq'' :
  Ne (α := FractionRing (𝕎 k))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
    (0 : FractionRing (𝕎 k))
⊢ Eq.{u_1 + 1} (α := FractionRing (𝕎 k))
    ((fun (x : 𝕎 k) ↦ ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) x : FractionRing (𝕎 k)))
      (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r'))
    ((fun (x : 𝕎 k) ↦ ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) x : FractionRing (𝕎 k)))
      (q' * b))

Tactic:
congr_arg (fun x => algebraMap (𝕎 k) (FractionRing (𝕎 k)) x) key

Premises used: Algebra.algebraMap, FractionRing, congr_arg, WittVector, DFunLike.coe
-- 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
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k)) (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q')
b : 𝕎 k := frobeniusRotation p hr' hq'
key : HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r' = q' * b
hq'' :
  Ne (α := FractionRing (𝕎 k))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
    (0 : FractionRing (𝕎 k))
h :
  HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) :
            (a : 𝕎 k) → Localization (nonZeroDivisors (𝕎 k)))
          ((frobenius : (a : 𝕎 k) → 𝕎 k) b) :
        Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) r' : FractionRing (𝕎 k)) =
    (algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k))
      (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r')
h₁ :
  HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k)) =
    (algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) (q' * b)
⊢ HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) :
            (a : 𝕎 k) → Localization (nonZeroDivisors (𝕎 k)))
          ((frobenius : (a : 𝕎 k) → 𝕎 k) b) :
        Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) r' : FractionRing (𝕎 k)) =
    HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))

Tactic:
convert! congr_arg (fun x => algebraMap (𝕎 k) (FractionRing (𝕎 k)) x) key using 1
-- 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
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k)) (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q')
b : 𝕎 k := frobeniusRotation p hr' hq'
key : HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r' = q' * b
hq'' :
  Ne (α := FractionRing (𝕎 k))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
    (0 : FractionRing (𝕎 k))
⊢ HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) :
            (a : 𝕎 k) → Localization (nonZeroDivisors (𝕎 k)))
          ((frobenius : (a : 𝕎 k) → 𝕎 k) b) :
        Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) r' : FractionRing (𝕎 k)) =
    (algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k))
      (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r')

Tactic:
simp only [map_mul]

Premises used: map_mul
-- 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
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k)) (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q')
b : 𝕎 k := frobeniusRotation p hr' hq'
key : HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r' = q' * b
hq'' :
  Ne (α := FractionRing (𝕎 k))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
    (0 : FractionRing (𝕎 k))
⊢ HMul.hMul (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (β :=
      Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k)) =
    (algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) (q' * b)

Tactic:
simp only [map_mul]

Premises used: map_mul
-- 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)
ha : a ≠ 0
revert :
  ∀ (ha : a ≠ 0),
    ∃ (b : FractionRing (𝕎 k)),
      b ≠ 0 ∧
        ∃ (m : ℤ),
          HMul.hMul (α := FractionRing (𝕎 k))
              ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
                    (a : FractionRing (𝕎 k)) → FractionRing (𝕎 k))
                  b :
                FractionRing (𝕎 k))
              a =
            HPow.hPow (α := FractionRing (𝕎 k)) (↑p : FractionRing (𝕎 k)) m * b
⊢ ∃ (b : FractionRing (𝕎 k)),
    b ≠ 0 ∧
      ∃ (m : ℤ),
        HMul.hMul (α := FractionRing (𝕎 k))
            ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
                  (a : FractionRing (𝕎 k)) → FractionRing (𝕎 k))
                b :
              FractionRing (𝕎 k))
            a =
          HPow.hPow (α := FractionRing (𝕎 k)) (↑p : FractionRing (𝕎 k)) m * b

Tactic:
revert ha
-- 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)
⊢ ∀ (ha : a ≠ 0),
    ∃ (b : FractionRing (𝕎 k)),
      b ≠ 0 ∧
        ∃ (m : ℤ),
          HMul.hMul (α := FractionRing (𝕎 k))
              ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
                    (a : FractionRing (𝕎 k)) → FractionRing (𝕎 k))
                  b :
                FractionRing (𝕎 k))
              a =
            HPow.hPow (α := FractionRing (𝕎 k)) (↑p : FractionRing (𝕎 k)) m * b

Tactic:
Localization.induction_on a ?_

Premises used: Localization.induction_on
-- 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)
refine :
  ∀ (y : 𝕎 k × ↥(nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)))
    (ha : Ne (α := FractionRing (𝕎 k)) (Localization.mk y.1 y.2) 0),
    ∃ (b : FractionRing (𝕎 k)),
      b ≠ 0 ∧
        ∃ (m : ℤ),
          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 y.1 y.2) =
            HPow.hPow (α := FractionRing (𝕎 k)) (↑p : FractionRing (𝕎 k)) m * b
⊢ ∀ (ha : a ≠ 0),
    ∃ (b : FractionRing (𝕎 k)),
      b ≠ 0 ∧
        ∃ (m : ℤ),
          HMul.hMul (α := FractionRing (𝕎 k))
              ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
                    (a : FractionRing (𝕎 k)) → FractionRing (𝕎 k))
                  b :
                FractionRing (𝕎 k))
              a =
            HPow.hPow (α := FractionRing (𝕎 k)) (↑p : FractionRing (𝕎 k)) m * b

Tactic:
refine Localization.induction_on a ?_
-- 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)
r q : 𝕎 k
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) q
hrq :
  Ne (α := FractionRing (𝕎 k))
    (Localization.mk
      (r,
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).1
      (r,
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).2)
    0
⊢ q ≠ 0

Tactic:
have hq0 : q ≠ 0 := mem_nonZeroDivisors_iff_ne_zero.1 hq
-- 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)
r q : 𝕎 k
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) q
hrq :
  Ne (α := FractionRing (𝕎 k))
    (Localization.mk
      (r,
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).1
      (r,
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).2)
    0
hq0 : q ≠ 0
h : r = 0
⊢ Eq (α := FractionRing (𝕎 k))
    (Localization.mk
      (r,
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).1
      (r,
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).2)
    0

Tactic:
simp [h]
-- 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)
r q : 𝕎 k
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) q
hrq :
  Ne (α := FractionRing (𝕎 k))
    (Localization.mk
      (r,
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).1
      (r,
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).2)
    0
hq0 : q ≠ 0
⊢ r ≠ 0

Tactic:
have hr0 : r ≠ 0 := fun h => hrq (by simp [h])
-- 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)
r q : 𝕎 k
hq : Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) q
hrq :
  Ne (α := FractionRing (𝕎 k))
    (Localization.mk
      (r,
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).1
      (r,
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).2)
    0
hq0 : q ≠ 0
hr0 : r ≠ 0
obtain :
  ∀ (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
⊢ ∃ (b : FractionRing (𝕎 k)),
    b ≠ 0 ∧
      ∃ (m : ℤ),
        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
              (r,
                  Subtype.mk (p := fun (x : 𝕎 k) ↦
                    Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x) q hq).1
              (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 * b

Tactic:
obtain ⟨m, r', hr', rfl⟩ := exists_eq_pow_p_mul r hr0

Premises used: WittVector.exists_eq_pow_p_mul, rfl
-- 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'
⊢ ∃ (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:
⟨algebraMap (𝕎 k) (FractionRing (𝕎 k)) b, ?_, m - n, ?_⟩

Premises used: Algebra.algebraMap, HSub.hSub, FractionRing, Nat.cast, WittVector, And.intro, Exists.intro, DFunLike.coe
-- 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'
⊢ Ne (α := FractionRing (𝕎 k))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))
    (0 : FractionRing (𝕎 k))

Tactic:
simpa only [map_zero] using
      (IsFractionRing.injective (WittVector p k) (FractionRing (WittVector p k))).ne
        (frobeniusRotation_nonzero p hr' hq')

Premises used: IsFractionRing.injective, FractionRing, Function.Injective.ne, map_zero, WittVector, WittVector.frobeniusRotation_nonzero
-- 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'
⊢ 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))

Tactic:
exists_frobenius_solution_fractionRing_aux p m n r' q' hr' hq' hq

Premises used: WittVector.exists_frobenius_solution_fractionRing_aux