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 : IsAlgClosed k
a₁ a₂ : 𝕎 k
⊢ ∃ (x : k), x ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0

Tactic:
IsAlgClosed.exists_pow_nat_eq _ <| tsub_pos_of_lt hp.out.one_lt

Premises used: Nat.Prime.one_lt, IsAlgClosed.exists_pow_nat_eq, Fact.out, tsub_pos_of_lt
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ a₂ : 𝕎 k
⊢ solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0

Tactic:
Classical.choose_spec <| solution_pow p a₁ a₂

Premises used: WittVector.RecursionBase.solution, Classical.choose_spec, WittVector.RecursionBase.solution_pow
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
⊢ solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0

Tactic:
have := solution_spec p a₁ a₂
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
rw : ∀ (this : 0 = a₂.coeff 0 / a₁.coeff 0), False
rw₁ : ∀ (this : HPow.hPow (α := k) 0 (p - 1) = a₂.coeff 0 / a₁.coeff 0), p - 1 ≠ 0
⊢ False

Tactic:
rw [h, zero_pow] at this

Premises used: zero_pow
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 = a₂.coeff 0 / a₁.coeff 0
⊢ False

Tactic:
simpa [ha₁, ha₂] using _root_.div_eq_zero_iff.mp this.symm

Premises used: Iff.mp, Eq.symm, div_eq_zero_iff
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : HPow.hPow (α := k) 0 (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ p - 1 ≠ 0

Tactic:
Nat.sub_ne_zero_of_lt hp.out.one_lt

Premises used: Nat.Prime.one_lt, Nat.sub_ne_zero_of_lt, Fact.out
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : HPow.hPow (α := k) 0 (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ p - 1 ≠ 0

Tactic:
exact Nat.sub_ne_zero_of_lt hp.out.one_lt

Premises used: Nat.Prime.one_lt, Nat.sub_ne_zero_of_lt, Fact.out
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
⊢ solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0

Tactic:
have := solution_spec p a₁ a₂
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ ∃ (k : ℕ), p = k.succ

Tactic:
have := Nat.exists_eq_succ_of_ne_zero hp.out.ne_zero
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this_1 : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
this : ∃ (k : ℕ), p = k.succ
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Tactic:
grind
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
apply : solution p a₁ a₂ = 0
⊢ False

Tactic:
apply solution_nonzero p ha₁ ha₂

Premises used: WittVector.RecursionBase.solution_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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ solution p a₁ a₂ = 0

Tactic:
simpa [← h, frobeniusRotation, frobeniusRotationCoeff] using WittVector.zero_coeff p k 0

Premises used: WittVector.frobeniusRotationCoeff, WittVector.frobeniusRotation, WittVector.zero_coeff, OfNat.ofNat
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h :
  ∀ (n : ℕ),
    (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff n =
      (frobeniusRotation p ha₁ ha₂ * a₂).coeff n
⊢ HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁ =
    frobeniusRotation p ha₁ ha₂ * a₂

Tactic:
ext n
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
h :
  (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff 0 =
    (frobeniusRotation p ha₁ ha₂ * a₂).coeff 0
h₁ :
  ∀ (n : ℕ),
    (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff (n + 1) =
      (frobeniusRotation p ha₁ ha₂ * a₂).coeff (n + 1)
⊢ (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff n =
    (frobeniusRotation p ha₁ ha₂ * a₂).coeff n

Tactic:
rcases n with - | n
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
⊢ (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff 0 =
    (frobeniusRotation p ha₁ ha₂ * a₂).coeff 0

Tactic:
simp only [WittVector.mul_coeff_zero, WittVector.coeff_frobenius_charP, frobeniusRotation,
      coeff_mk, frobeniusRotationCoeff]

Premises used: WittVector.frobeniusRotationCoeff, WittVector.frobeniusRotation, WittVector.coeff_frobenius_charP, WittVector.coeff_mk, WittVector.mul_coeff_zero
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Tactic:
solution_spec' _ ha₁ _

Premises used: WittVector.RecursionBase.solution_spec'
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Tactic:
exact solution_spec' _ ha₁ _

Premises used: WittVector.RecursionBase.solution_spec'
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
h :
  succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ ^ p *
          a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂))))
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ *
          a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) (truncateFun (n + 1) a₂)
⊢ (HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) (frobeniusRotation p ha₁ ha₂) : 𝕎 k) a₁).coeff (n + 1) =
    (frobeniusRotation p ha₁ ha₂ * a₂).coeff (n + 1)

Tactic:
simp only [nthRemainder_spec, WittVector.coeff_frobenius_charP,
      frobeniusRotation, coeff_mk, frobeniusRotationCoeff]

Premises used: WittVector.frobeniusRotationCoeff, WittVector.frobeniusRotation, WittVector.coeff_frobenius_charP, WittVector.coeff_mk, WittVector.nthRemainder_spec
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ ^ p *
          a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (frobeniusRotationCoeff p ha₁ ha₂ (↑0 : ℕ) ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p)
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ *
          a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * frobeniusRotationCoeff p ha₁ ha₂ (↑0 : ℕ) ^ p ^ (n + 1) +
      nthRemainder p n (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) (truncateFun (n + 1) a₂)

Tactic:
have :=
      succNthVal_spec' p n a₁ a₂ (fun i : Fin (n + 1) => frobeniusRotationCoeff p ha₁ ha₂ i.val)
        ha₁ 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ ^ p *
          a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p)
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ *
          a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) (truncateFun (n + 1) a₂)
⊢ succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ ^ p *
          a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p)
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ *
          a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) (truncateFun (n + 1) a₂)

Tactic:
this
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ ^ p *
          a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p)
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ *
          a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) (truncateFun (n + 1) a₂)
h :
  Eq.{u_1 + 1} (α := Fin (n + 1) → k)
    (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) :
      TruncatedWittVector p (n + 1) k)
    fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p
⊢ succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ ^ p *
          a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂))))
        (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun (i : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑i : ℕ)) ha₁ ha₂ *
          a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) (truncateFun (n + 1) a₂)

Tactic:
convert! this using 3
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
h :
  ∀ (i : Fin (n + 1)),
    Eq.{u_1 + 1} (α := k)
      (TruncatedWittVector.coeff (p := p) i
        (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂)))))
      (TruncatedWittVector.coeff (p := p) i fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p)
⊢ Eq.{u_1 + 1} (α := Fin (n + 1) → k)
    (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂))) :
      TruncatedWittVector p (n + 1) k)
    fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p

Tactic:
apply TruncatedWittVector.ext

Premises used: TruncatedWittVector.ext
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
i : Fin (n + 1)
h :
  (mk p (frobeniusRotationCoeff p ha₁ ha₂)).coeff (↑i : ℕ) ^ p =
    TruncatedWittVector.coeff (p := p) i fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p
⊢ Eq.{u_1 + 1} (α := k)
    (TruncatedWittVector.coeff (p := p) i
      (truncateFun (n + 1) ((frobenius : (a : 𝕎 k) → 𝕎 k) (mk p (frobeniusRotationCoeff p ha₁ ha₂)))))
    (TruncatedWittVector.coeff (p := p) i fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p)

Tactic:
simp only [WittVector.coeff_truncateFun, WittVector.coeff_frobenius_charP]

Premises used: WittVector.coeff_truncateFun, WittVector.coeff_frobenius_charP
-- 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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
i : Fin (n + 1)
⊢ (mk p (frobeniusRotationCoeff p ha₁ ha₂)).coeff (↑i : ℕ) ^ p =
    TruncatedWittVector.coeff (p := p) i fun (v : Fin (n + 1)) ↦ frobeniusRotationCoeff p ha₁ ha₂ (↑v : ℕ) ^ p

Tactic:
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
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'
⊢ HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r' = q' * b

Tactic:
linear_combination frobenius_frobeniusRotation p hr' hq'

Premises used: WittVector.frobenius_frobeniusRotation
-- 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'
⊢ HMul.hMul (α := 𝕎 k) ((frobenius : (a : 𝕎 k) → 𝕎 k) b : 𝕎 k) r' = q' * b

Tactic:
have key : WittVector.frobenius b * r' = q' * b := by
    linear_combination frobenius_frobeniusRotation p hr' 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
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
h : q' = 0
⊢ q'.coeff 0 = 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
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
⊢ q' ≠ 0

Tactic:
have hq''' : q' ≠ 0 := fun h => hq' (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
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''' : q' ≠ 0
⊢ Ne (α := FractionRing (𝕎 k))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
    (0 : FractionRing (𝕎 k))

Tactic:
simpa only [Ne, map_zero] using
      (IsFractionRing.injective (𝕎 k) (FractionRing (𝕎 k))).ne hq'''

Premises used: map_zero, Ne
-- 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
⊢ Ne (α := FractionRing (𝕎 k))
    ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) q' : FractionRing (𝕎 k))
    (0 : FractionRing (𝕎 k))

Tactic:
have hq'' : algebraMap (𝕎 k) (FractionRing (𝕎 k)) q' ≠ 0 := by
    have hq''' : q' ≠ 0 := fun h => hq' (by simp [h])
    simpa only [Ne, map_zero] using
      (IsFractionRing.injective (𝕎 k) (FractionRing (𝕎 k))).ne 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
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))
rw :
  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))
⊢ 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 (α := Localization (M := 𝕎 k) (nonZeroDivisors (𝕎 k))) (↑p : Localization (nonZeroDivisors (𝕎 k)))
        (HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))

Tactic:
rw [zpow_sub₀ (FractionRing.p_nonzero p k)]

Premises used: zpow_sub₀, WittVector.FractionRing.p_nonzero