awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
a :
  HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
        n -
      HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) (β := ℕ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) 0 *
          HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
            ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ 0) :
              MvPolynomial (Fin 0 × ℕ) ℚ)
            (p ^ (n - 0)) *
        HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
          ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
          n =
    0
a₁ :
  ∀ b ∈ Finset.range n,
    b ≠ 0 →
      HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) b *
          HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
            ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ b) :
              MvPolynomial (Fin 0 × ℕ) ℚ)
            (p ^ (n - b)) =
        0
a₂ :
  0 ∉ Finset.range n →
    HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) (β := ℕ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) 0 *
        HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
          ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ 0) :
            MvPolynomial (Fin 0 × ℕ) ℚ)
          (p ^ (n - 0)) =
      0
⊢ HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
        n -
      (∑ x ∈ Finset.range n,
          HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) x *
            HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
              ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ x) :
                MvPolynomial (Fin 0 × ℕ) ℚ)
              (p ^ (n - x))) *
        HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
          ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
          n =
    0

Tactic:
rw [Finset.sum_eq_single 0]

Premises used: Finset.sum_eq_single, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
a :
  HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
        n -
      HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
          ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ 0) :
            MvPolynomial (Fin 0 × ℕ) ℚ)
          (p ^ (n - 0)) *
        HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
          ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
          n =
    0
⊢ HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
        n -
      HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) (β := ℕ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) 0 *
          HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
            ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ 0) :
              MvPolynomial (Fin 0 × ℕ) ℚ)
            (p ^ (n - 0)) *
        HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
          ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
          n =
    0

Tactic:
simp only [one_mul, pow_zero]

Premises used: pow_zero, one_mul
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
⊢ HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
        n -
      HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
          ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ 0) :
            MvPolynomial (Fin 0 × ℕ) ℚ)
          (p ^ (n - 0)) *
        HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
          ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
          n =
    0

Tactic:
simp only [one_pow, one_mul, xInTermsOfW_zero, sub_self, bind₁_X_right]

Premises used: one_pow, sub_self, xInTermsOfW_zero, MvPolynomial.bind₁_X_right, one_mul
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
i : ℕ
hin : i ∈ Finset.range n
hi0 : i ≠ 0
⊢ i < n

Tactic:
rw [Finset.mem_range] at hin

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
i : ℕ
hin : i ∈ Finset.range n
hi0 : i ≠ 0
hin₁ : i < n
⊢ i ≠ 0

Tactic:
rw [Finset.mem_range] at hin

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
i : ℕ
hin : i < n
hi0 : i ≠ 0
a :
  HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) i *
      HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) 0 (p ^ (n - i)) =
    0
a₁ : HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) i * 0 = 0
a₂ a₃ : Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ) 0 0
⊢ HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) i *
      HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ i) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (p ^ (n - i)) =
    0

Tactic:
rw [IH _ hin (Nat.pos_of_ne_zero hi0), zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero]

Premises used: pow_ne_zero, MulZeroClass.mul_zero, Nat.pos_of_ne_zero, Nat.Prime.ne_zero, zero_pow, Fact.out
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
⊢ 0 ∉ Finset.range n →
    HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) (β := ℕ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) 0 *
        HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
          ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ 0) :
            MvPolynomial (Fin 0 × ℕ) ℚ)
          (p ^ (n - 0)) =
      0

Tactic:
grind
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a :
  Eq (α := MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ) (wittAdd p 0) :
      MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ)
        (HAdd.hAdd (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))) :
      MvPolynomial (Fin 2 × ℕ) ℚ)
⊢ wittAdd p 0 = HAdd.hAdd (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Premises used: Rat, MvPolynomial.map_injective, Int.castRingHom, Int.cast_injective
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ) (wittAdd p 0) :
      MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ)
        (HAdd.hAdd (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))) :
      MvPolynomial (Fin 2 × ℕ) ℚ)

Tactic:
simp only [wittAdd, wittStructureRat, map_add, rename_X, xInTermsOfW_zero, map_X,
    wittPolynomial_zero, bind₁_X_right, map_wittStructureInt]

Premises used: map_add, WittVector.wittAdd, wittStructureRat, xInTermsOfW_zero, MvPolynomial.rename_X, wittPolynomial_zero, MvPolynomial.bind₁_X_right, map_wittStructureInt, MvPolynomial.map_X
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a :
  Eq (α := MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ) (wittSub p 0) :
      MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ)
        (HSub.hSub (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))) :
      MvPolynomial (Fin 2 × ℕ) ℚ)
⊢ wittSub p 0 = HSub.hSub (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Premises used: Rat, MvPolynomial.map_injective, Int.castRingHom, Int.cast_injective
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ) (wittSub p 0) :
      MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ)
        (HSub.hSub (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))) :
      MvPolynomial (Fin 2 × ℕ) ℚ)

Tactic:
simp only [wittSub, wittStructureRat, map_sub, rename_X, xInTermsOfW_zero, map_X,
    wittPolynomial_zero, bind₁_X_right, map_wittStructureInt]

Premises used: map_sub, wittStructureRat, xInTermsOfW_zero, MvPolynomial.rename_X, WittVector.wittSub, wittPolynomial_zero, MvPolynomial.bind₁_X_right, map_wittStructureInt, MvPolynomial.map_X
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a :
  Eq (α := MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ) (wittMul p 0) :
      MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ)
        (HMul.hMul (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))) :
      MvPolynomial (Fin 2 × ℕ) ℚ)
⊢ wittMul p 0 = HMul.hMul (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Premises used: Rat, MvPolynomial.map_injective, Int.castRingHom, Int.cast_injective
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ) (wittMul p 0) :
      MvPolynomial (Fin 2 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → MvPolynomial (Fin 2 × ℕ) ℚ)
        (HMul.hMul (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))) :
      MvPolynomial (Fin 2 × ℕ) ℚ)

Tactic:
simp only [wittMul, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero,
    map_mul, bind₁_X_right, map_wittStructureInt]

Premises used: WittVector.wittMul, wittStructureRat, xInTermsOfW_zero, map_mul, MvPolynomial.rename_X, wittPolynomial_zero, MvPolynomial.bind₁_X_right, map_wittStructureInt, MvPolynomial.map_X
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a :
  Eq (α := MvPolynomial (Fin 1 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → MvPolynomial (Fin 1 × ℕ) ℚ) (wittNeg p 0) :
      MvPolynomial (Fin 1 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → MvPolynomial (Fin 1 × ℕ) ℚ) (-X (0, 0)) :
      MvPolynomial (Fin 1 × ℕ) ℚ)
⊢ wittNeg p 0 = -X (0, 0)

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Premises used: Rat, MvPolynomial.map_injective, Int.castRingHom, Int.cast_injective
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := MvPolynomial (Fin 1 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → MvPolynomial (Fin 1 × ℕ) ℚ) (wittNeg p 0) :
      MvPolynomial (Fin 1 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → MvPolynomial (Fin 1 × ℕ) ℚ) (-X (0, 0)) :
      MvPolynomial (Fin 1 × ℕ) ℚ)

Tactic:
simp only [wittNeg, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero,
    map_neg, bind₁_X_right, map_wittStructureInt]

Premises used: map_neg, WittVector.wittNeg, wittStructureRat, xInTermsOfW_zero, MvPolynomial.rename_X, wittPolynomial_zero, MvPolynomial.bind₁_X_right, map_wittStructureInt, MvPolynomial.map_X
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
apply :
  Eq (α := ℤ)
    ((constantCoeff : (a : MvPolynomial (Fin 2) ℤ) → ℤ) (HAdd.hAdd (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) : ℤ)
    (0 : ℤ)
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (wittAdd p n) : ℤ) (0 : ℤ)

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Premises used: constantCoeff_wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℤ)
    ((constantCoeff : (a : MvPolynomial (Fin 2) ℤ) → ℤ) (HAdd.hAdd (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) : ℤ)
    (0 : ℤ)

Tactic:
simp only [add_zero, map_add, constantCoeff_X]

Premises used: map_add, MvPolynomial.constantCoeff_X, add_zero
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
apply :
  Eq (α := ℤ)
    ((constantCoeff : (a : MvPolynomial (Fin 2) ℤ) → ℤ) (HSub.hSub (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) : ℤ)
    (0 : ℤ)
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (wittSub p n) : ℤ) (0 : ℤ)

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Premises used: constantCoeff_wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℤ)
    ((constantCoeff : (a : MvPolynomial (Fin 2) ℤ) → ℤ) (HSub.hSub (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) : ℤ)
    (0 : ℤ)

Tactic:
simp only [sub_zero, map_sub, constantCoeff_X]

Premises used: map_sub, sub_zero, MvPolynomial.constantCoeff_X
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
apply :
  Eq (α := ℤ)
    ((constantCoeff : (a : MvPolynomial (Fin 2) ℤ) → ℤ) (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) : ℤ)
    (0 : ℤ)
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (wittMul p n) : ℤ) (0 : ℤ)

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Premises used: constantCoeff_wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℤ)
    ((constantCoeff : (a : MvPolynomial (Fin 2) ℤ) → ℤ) (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) : ℤ)
    (0 : ℤ)

Tactic:
simp only [mul_zero, map_mul, constantCoeff_X]

Premises used: MulZeroClass.mul_zero, MvPolynomial.constantCoeff_X, map_mul
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
apply : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 1) ℤ) → ℤ) (-X 0) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → ℤ) (wittNeg p n) : ℤ) (0 : ℤ)

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Premises used: constantCoeff_wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 1) ℤ) → ℤ) (-X 0) : ℤ) (0 : ℤ)

Tactic:
simp only [neg_zero, map_neg, constantCoeff_X]

Premises used: map_neg, MvPolynomial.constantCoeff_X, neg_zero
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
apply :
  Eq (α := ℤ)
    ((constantCoeff : (a : MvPolynomial (Fin 1) ℤ) → ℤ) (HSMul.hSMul (β := MvPolynomial (Fin 1) ℤ) m (X 0)) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → ℤ) (wittNSMul p m n) : ℤ) (0 : ℤ)

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Premises used: constantCoeff_wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
⊢ Eq (α := ℤ)
    ((constantCoeff : (a : MvPolynomial (Fin 1) ℤ) → ℤ) (HSMul.hSMul (β := MvPolynomial (Fin 1) ℤ) m (X 0)) : ℤ) (0 : ℤ)

Tactic:
simp only [smul_zero, map_nsmul, constantCoeff_X]

Premises used: smul_zero, MvPolynomial.constantCoeff_X, map_nsmul
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
n : ℕ
apply :
  Eq (α := ℤ)
    ((constantCoeff : (a : MvPolynomial (Fin 1) ℤ) → ℤ) (HSMul.hSMul (β := MvPolynomial (Fin 1) ℤ) z (X 0)) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → ℤ) (wittZSMul p z n) : ℤ) (0 : ℤ)

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Premises used: constantCoeff_wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
n : ℕ
⊢ Eq (α := ℤ)
    ((constantCoeff : (a : MvPolynomial (Fin 1) ℤ) → ℤ) (HSMul.hSMul (β := MvPolynomial (Fin 1) ℤ) z (X 0)) : ℤ) (0 : ℤ)

Tactic:
simp only [smul_zero, map_zsmul, constantCoeff_X]

Premises used: smul_zero, MvPolynomial.constantCoeff_X, map_zsmul
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) (σ := Fin 0 × ℕ)
              (Function.uncurry fun (i : Fin 0) ↦ coeff (p := p) (![] i)) :
            MvPolynomial (Fin 0 × ℕ) ℤ →ₐ[ℤ] R) :
          (a : MvPolynomial (Fin 0 × ℕ) ℤ) → R)
        (wittZero p n) :
      R)
    (0 : R)

Tactic:
simp only [wittZero_eq_zero, map_zero]

Premises used: map_zero, WittVector.wittZero_eq_zero
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := R)
    (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) (σ := Fin 0 × ℕ)
              (Function.uncurry fun (i : Fin 0) ↦ coeff (p := p) (![] i)) :
            MvPolynomial (Fin 0 × ℕ) ℤ →ₐ[ℤ] R) :
          (a : MvPolynomial (Fin 0 × ℕ) ℤ) → R)
        (wittOne p 0) :
      R)
    (1 : R)

Tactic:
simp only [wittOne_zero_eq_one, map_one]

Premises used: map_one, WittVector.wittOne_zero_eq_one
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
n : ℕ
hn : 0 < n
⊢ Eq.{u_1 + 1} (α := R)
    (((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) (σ := Fin 0 × ℕ)
              (Function.uncurry fun (i : Fin 0) ↦ coeff (p := p) (![] i)) :
            MvPolynomial (Fin 0 × ℕ) ℤ →ₐ[ℤ] R) :
          (a : MvPolynomial (Fin 0 × ℕ) ℤ) → R)
        (wittOne p n) :
      R)
    (0 : R)

Tactic:
simp only [hn, wittOne_pos_eq_zero, map_zero]

Premises used: map_zero, WittVector.wittOne_pos_eq_zero
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
i : Fin 2
0 : (![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).coeff = ![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
1 : (![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).coeff = ![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (![x, y] i).coeff = ![x.coeff, y.coeff] i

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
⊢ (![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).coeff = ![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
⊢ (![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).coeff = ![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x y : 𝕎 R
n : ℕ
⊢ (x + y).coeff n = peval (wittAdd p n) ![x.coeff, y.coeff]

Tactic:
simp [(· + ·), Add.add, eval]

Premises used: WittVector.eval, Add.add, HAdd.hAdd
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x y : 𝕎 R
n : ℕ
⊢ (x - y).coeff n = peval (wittSub p n) ![x.coeff, y.coeff]

Tactic:
simp [(· - ·), Sub.sub, eval]

Premises used: HSub.hSub, WittVector.eval, Sub.sub
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x y : 𝕎 R
n : ℕ
⊢ (x * y).coeff n = peval (wittMul p n) ![x.coeff, y.coeff]

Tactic:
simp [(· * ·), Mul.mul, eval]

Premises used: HMul.hMul, WittVector.eval, Mul.mul
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ (-x).coeff n = peval (wittNeg p n) ![x.coeff]

Tactic:
simp [Neg.neg, eval, Matrix.cons_fin_one]

Premises used: Matrix.cons_fin_one, WittVector.eval, Neg.neg
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ (m • x).coeff n = peval (wittNSMul p m n) ![x.coeff]

Tactic:
simp [(· • ·), SMul.smul, eval, Matrix.cons_fin_one]

Premises used: Matrix.cons_fin_one, WittVector.eval, HSMul.hSMul, SMul.smul
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
m : ℤ
x : 𝕎 R
n : ℕ
⊢ (m • x).coeff n = peval (wittZSMul p m n) ![x.coeff]

Tactic:
simp [(· • ·), SMul.smul, eval, Matrix.cons_fin_one]

Premises used: Matrix.cons_fin_one, WittVector.eval, HSMul.hSMul, SMul.smul
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ (x ^ m).coeff n = peval (wittPow p m n) ![x.coeff]

Tactic:
simp [(· ^ ·), Pow.pow, eval, Matrix.cons_fin_one]

Premises used: Matrix.cons_fin_one, Pow.pow, WittVector.eval, HPow.hPow
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x y : 𝕎 R
⊢ (x + y).coeff 0 = x.coeff 0 + y.coeff 0

Tactic:
simp [add_coeff, peval, Function.uncurry]

Premises used: WittVector.peval, Function.uncurry, WittVector.add_coeff