awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)))
      ((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))
have 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))
Tactic: simp [field, FractionRing.p_nonzero p k]
-- 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
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)) =
    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))
have 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')
Tactic: convert! congr_arg (fun x => algebraMap (𝕎 k) (FractionRing (𝕎 k)) x) key using 1
-- 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
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')
⊢ 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))
have 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)
Tactic: convert! congr_arg (fun x => algebraMap (𝕎 k) (FractionRing (𝕎 k)) x) key using 1
-- 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)
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
have 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
Tactic: revert ha
Cleared hypotheses: ha
-- 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)
⊢ ∀ (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
have 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
Tactic: refine Localization.induction_on a ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
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
⊢ ∃ (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
have hq0 : q ≠ 0
Tactic: have hq0 : q ≠ 0 := mem_nonZeroDivisors_iff_ne_zero.1 hq
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.FrobeniusFractionField (hypothesis)
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
⊢ ∃ (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
have hr0 : r ≠ 0
Tactic: have hr0 : r ≠ 0 := fun h => hrq (by simp [h])
-- 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)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨m, r', hr', rfl⟩ := exists_eq_pow_p_mul r hr0
Cleared hypotheses: r, hrq, hr0
-- 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)
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
have refine_1 : Ne (α := FractionRing (𝕎 k))
  ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))
  (0 : FractionRing (𝕎 k))
Tactic: refine ⟨algebraMap (𝕎 k) (FractionRing (𝕎 k)) b, ?_, m - n, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (hypothesis)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
⊢ (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) = x * (↑p : 𝕎 R)
have this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦
  (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)
Tactic: have : IsPoly p fun {R} [CommRing R] x ↦ frobenius (verschiebung x) :=
    IsPoly.comp (hg := frobenius_isPoly p) (hf := verschiebung_isPoly)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (hypothesis)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
this :
  IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦
    (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)
⊢ (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) = x * (↑p : 𝕎 R)
have this₁ : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ x * (↑p : 𝕎 R)
Tactic: have : IsPoly p fun {R} [CommRing R] x ↦ x * p := mulN_isPoly p p
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
this_1 :
  IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦
    (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ x * (↑p : 𝕎 R)
⊢ (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) = x * (↑p : 𝕎 R)
have refine_3 : ∀ (R : Type u_1) [R._inst : CommRing R] (x : 𝕎 R) (n : ℕ),
  Eq (α := R)
    ((ghostComponent n : (a : 𝕎 R) → R)
        ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) : 𝕎 R) :
      R)
    ((ghostComponent n : (a : 𝕎 R) → R) (x * (↑p : 𝕎 R)) : R)
Tactic: ghost_calc x
Cleared hypotheses: R, inst, x
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ (verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x = x * (↑p : 𝕎 (ZMod p))
have rw : Eq (α := 𝕎 (ZMod p)) ((verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p))
  ((frobenius : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) ((verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p)) :
    𝕎 (ZMod p))
Tactic: rw [← frobenius_verschiebung, frobenius_zmodp]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
rw :
  Eq (α := 𝕎 (ZMod p)) ((verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p))
    ((frobenius : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) ((verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p)) :
      𝕎 (ZMod p))
⊢ (verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x = x * (↑p : 𝕎 (ZMod p))
have rw₁ : Eq (α := 𝕎 (ZMod p)) ((verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p))
  ((verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p))
Tactic: rw [← frobenius_verschiebung, frobenius_zmodp]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
h : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff (i + 1) = 1
have succ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i * (↑p : 𝕎 R)).coeff (i + 1) = 1
Tactic: rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
h : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1
succ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i * (↑p : 𝕎 R)).coeff (i + 1) = 1
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff (i + 1) = 1
have succ₁ : Eq.{u_1 + 1} (α := R)
  (coeff (p := p)
    ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) : 𝕎 R))
    (i + 1))
  1
Tactic: rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
h : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1
succ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i * (↑p : 𝕎 R)).coeff (i + 1) = 1
succ₁ :
  Eq.{u_1 + 1} (α := R)
    (coeff (p := p)
      ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) : 𝕎 R))
      (i + 1))
    1
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff (i + 1) = 1
have succ₂ : HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) (i + 1)) p = 1
Tactic: rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
h : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1
succ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i * (↑p : 𝕎 R)).coeff (i + 1) = 1
succ₁ :
  Eq.{u_1 + 1} (α := R)
    (coeff (p := p)
      ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) : 𝕎 R))
      (i + 1))
    1
succ₂ :
  HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) (i + 1)) p =
    1
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff (i + 1) = 1
have succ₃ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i ^ p = 1
Tactic: rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]