awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
f : 𝕎 R
n : ℕ
rw :
  coeff (p := p)
      ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R)
        ((map (_root_.frobenius R p) : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
      n =
    f.coeff n
⊢ coeff (p := p)
      ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R)
        ((frobenius : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
      n =
    f.coeff n

Tactic:
rw [frobenius_eq_map_frobenius]

Premises used: WittVector.frobenius_eq_map_frobenius
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
f : 𝕎 R
n : ℕ
⊢ coeff (p := p)
      ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R)
        ((map (_root_.frobenius R p) : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
      n =
    f.coeff n

Tactic:
frobeniusEquiv_symm_apply_frobenius R p _

Premises used: frobeniusEquiv_symm_apply_frobenius
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
f : 𝕎 R
n : ℕ
⊢ coeff (p := p)
      ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R)
        ((map (_root_.frobenius R p) : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
      n =
    f.coeff n

Tactic:
exact frobeniusEquiv_symm_apply_frobenius R p _

Premises used: frobeniusEquiv_symm_apply_frobenius
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
f : 𝕎 R
n : ℕ
rw :
  coeff (p := p)
      ((map (_root_.frobenius R p) : (a : 𝕎 R) → 𝕎 R)
        ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
      n =
    f.coeff n
⊢ coeff (p := p)
      ((frobenius : (a : 𝕎 R) → 𝕎 R)
        ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
      n =
    f.coeff n

Tactic:
rw [frobenius_eq_map_frobenius]

Premises used: WittVector.frobenius_eq_map_frobenius
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
f : 𝕎 R
n : ℕ
⊢ coeff (p := p)
      ((map (_root_.frobenius R p) : (a : 𝕎 R) → 𝕎 R)
        ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
      n =
    f.coeff n

Tactic:
frobenius_apply_frobeniusEquiv_symm R p _

Premises used: frobenius_apply_frobeniusEquiv_symm
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
f : 𝕎 R
n : ℕ
⊢ coeff (p := p)
      ((map (_root_.frobenius R p) : (a : 𝕎 R) → 𝕎 R)
        ((map (↑(RingEquiv.symm (_root_.frobeniusEquiv R p)) : R →+* R) : (a : 𝕎 R) → 𝕎 R) f : 𝕎 R))
      n =
    f.coeff n

Tactic:
exact frobenius_apply_frobeniusEquiv_symm R p _

Premises used: frobenius_apply_frobeniusEquiv_symm
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := 𝕎 R) (β := 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)

Tactic:
(frobeniusEquiv p R).bijective

Premises used: WittVector.frobeniusEquiv, WittVector.mk, RingEquiv.bijective, WittVector.frobeniusFun
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
rw : (HPow.hPow (α := k[X]) X p).degree + 0 = (↑p : WithBot ℕ)
rw₁ : a₁.coeff 0 ^ p ^ (n + 1) ≠ 0
⊢ (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)

Tactic:
rw [degree_mul, degree_C]

Premises used: Polynomial.degree_C, Polynomial.degree_mul
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ (HPow.hPow (α := k[X]) X p).degree + 0 = (↑p : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ a₁.coeff 0 ^ p ^ (n + 1) ≠ 0

Tactic:
pow_ne_zero _ ha₁

Premises used: pow_ne_zero
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ a₁.coeff 0 ^ p ^ (n + 1) ≠ 0

Tactic:
exact pow_ne_zero _ ha₁

Premises used: pow_ne_zero
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)

Tactic:
have : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = (p : WithBot ℕ) := by
    rw [degree_mul, degree_C]
    · simp
    · exact pow_ne_zero _ ha₁
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
rw :
  (HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree <
    (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree
⊢ (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)

Tactic:
rw [degree_sub_eq_left_of_degree_lt, this]

Premises used: Polynomial.degree_sub_eq_left_of_degree_lt
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
rw : LT.lt (α := WithBot ℕ) 1 (↑p : WithBot ℕ)
rw₁ : a₂.coeff 0 ^ p ^ (n + 1) ≠ 0
⊢ (HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree <
    (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree

Tactic:
rw [this, degree_mul, degree_C, degree_X, add_zero]

Premises used: Polynomial.degree_C, Polynomial.degree_X, add_zero, Polynomial.degree_mul
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ) 1 (↑p : WithBot ℕ)

Tactic:
mod_cast hp.out.one_lt

Premises used: Nat.Prime.one_lt, congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, LT.lt, congrFun', Eq.symm, Nat.cast_one, Fact.out, Eq.trans
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ) 1 (↑p : WithBot ℕ)

Tactic:
exact mod_cast hp.out.one_lt

Premises used: Nat.Prime.one_lt, Fact.out
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ a₂.coeff 0 ^ p ^ (n + 1) ≠ 0

Tactic:
pow_ne_zero _ ha₂

Premises used: pow_ne_zero
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ a₂.coeff 0 ^ p ^ (n + 1) ≠ 0

Tactic:
exact pow_ne_zero _ ha₂

Premises used: pow_ne_zero
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)

Tactic:
have : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree =
      (p : WithBot ℕ) := by
    rw [degree_sub_eq_left_of_degree_lt, this]
    rw [this, degree_mul, degree_C, degree_X, add_zero]
    · exact mod_cast hp.out.one_lt
    · exact pow_ne_zero _ ha₂
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this_1 :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
rw :
  degree.{u_1} (R := k)
      ((C : (a : k) → k[X])
        (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
              nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
            a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
          nthRemainder p n bs (truncateFun (n + 1) a₂))) <
    (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree
⊢ degree (succNthDefiningPoly p n a₁ a₂ bs) = (↑p : WithBot ℕ)

Tactic:
rw [succNthDefiningPoly, degree_add_eq_left_of_degree_lt, this]

Premises used: WittVector.RecursionMain.succNthDefiningPoly, Polynomial.degree_add_eq_left_of_degree_lt
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this_1 :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
apply :
  0 <
    (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree
⊢ degree.{u_1} (R := k)
      ((C : (a : k) → k[X])
        (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
              nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
            a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
          nthRemainder p n bs (truncateFun (n + 1) a₂))) <
    (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree

Tactic:
apply lt_of_le_of_lt degree_C_le

Premises used: lt_of_le_of_lt, Polynomial.degree_C_le
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this_1 :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
rw : LT.lt (α := WithBot ℕ) 0 (↑p : WithBot ℕ)
⊢ 0 <
    (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this_1 :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ) 0 (↑p : WithBot ℕ)

Tactic:
mod_cast hp.out.pos

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.Prime.pos, Nat.cast, LT.lt, congrFun', Nat.cast_zero, Eq.symm, Fact.out, Eq.trans
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this_1 :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
this :
  (HMul.hMul (β := k[X]) (HPow.hPow (α := k[X]) X p) ((C : (a : k) → k[X]) (a₁.coeff 0 ^ p ^ (n + 1)) : k[X]) -
        HMul.hMul (α := k[X]) (β := k[X]) X ((C : (a : k) → k[X]) (a₂.coeff 0 ^ p ^ (n + 1)) : k[X])).degree =
    (↑p : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ) 0 (↑p : WithBot ℕ)

Tactic:
exact mod_cast hp.out.pos

Premises used: Nat.Prime.pos, Fact.out
-- 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
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ Polynomial.degree (succNthDefiningPoly p n a₁ a₂ bs) ≠ 0

Tactic:
simp only [succNthDefiningPoly_degree p n a₁ a₂ bs ha₁ ha₂, ne_eq, Nat.cast_eq_zero,
      hp.out.ne_zero, not_false_eq_true]

Premises used: WittVector.RecursionMain.succNthDefiningPoly_degree, ne_eq, Nat.cast_eq_zero, Nat.Prime.ne_zero, not_false_eq_true, Fact.out
-- 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
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ Polynomial.IsRoot (succNthDefiningPoly p n a₁ a₂ bs) (succNthVal p n a₁ a₂ bs ha₁ ha₂)

Tactic:
Classical.choose_spec (root_exists p n a₁ a₂ bs ha₁ ha₂)

Premises used: Classical.choose_spec, WittVector.RecursionMain.succNthVal, WittVector.RecursionMain.root_exists
-- 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
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
rw :
  succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
      nthRemainder p n bs (truncateFun (n + 1) a₂)

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_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
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ Polynomial.IsRoot (succNthDefiningPoly p n a₁ a₂ bs) (succNthVal p n a₁ a₂ bs ha₁ ha₂)

Tactic:
have := succNthVal_spec p n a₁ a₂ bs 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
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : Polynomial.IsRoot (succNthDefiningPoly p n a₁ a₂ bs) (succNthVal p n a₁ a₂ bs ha₁ ha₂)
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
            nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0

Tactic:
simp only [Polynomial.eval_X, Polynomial.eval_C,
    Polynomial.eval_pow, succNthDefiningPoly, Polynomial.eval_mul, Polynomial.eval_add,
    Polynomial.eval_sub, Polynomial.IsRoot.def]
    at this

Premises used: Polynomial.eval_C, Polynomial.eval_X, Polynomial.eval_pow, WittVector.RecursionMain.succNthDefiningPoly, Polynomial.IsRoot.def, Polynomial.eval_mul, Polynomial.eval_add, Polynomial.eval_sub
-- 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
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
            nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
            nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0

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
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
            nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
h :
  succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
            nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂))
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0

Tactic:
convert! this 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
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
            nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
            nthRemainder p n (fun (v : Fin (n + 1)) ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂))

Tactic:
ring