awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
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
⊢ HSub.hSub (α := MvPolynomial (Fin 0 × ℕ) ℚ) 1
        (∑ 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
have a : 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 [sub_mul, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
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 -
      (∑ 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
have 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
Tactic: rw [Finset.sum_eq_single 0]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
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
⊢ 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
have 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
Tactic: rw [Finset.sum_eq_single 0]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
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
⊢ 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
have 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
Tactic: rw [Finset.sum_eq_single 0]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
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 × ℕ) ℚ) (β := ℕ) ((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
have 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
Tactic: simp only [one_mul, pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (hypothesis)
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
⊢ 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
have hin₁ : i < n
Tactic: rw [Finset.mem_range] at hin
Cleared hypotheses: hin, hi0
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
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
⊢ 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
have a : HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) i *
    HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) 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]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
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
⊢ 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
have a₁ : HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) i * 0 = 0
Tactic: rw [IH _ hin (Nat.pos_of_ne_zero hi0), zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
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
⊢ 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
have a₂ : Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ) 0 0
Tactic: rw [IH _ hin (Nat.pos_of_ne_zero hi0), zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittAdd p 0 = HAdd.hAdd (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))
have 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 × ℕ) ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittSub p 0 = HSub.hSub (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))
have 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 × ℕ) ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittMul p 0 = HMul.hMul (α := MvPolynomial (Fin 2 × ℕ) ℤ) (X (0, 0)) (X (1, 0))
have 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 × ℕ) ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittNeg p 0 = -X (0, 0)
have 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 × ℕ) ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (wittAdd p n) : ℤ) (0 : ℤ)
have apply : Eq (α := ℤ)
  ((constantCoeff : (a : MvPolynomial (Fin 2) ℤ) → ℤ) (HAdd.hAdd (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) : ℤ) (0 : ℤ)
Tactic: apply constantCoeff_wittStructureInt p _ _ n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (wittSub p n) : ℤ) (0 : ℤ)
have apply : Eq (α := ℤ)
  ((constantCoeff : (a : MvPolynomial (Fin 2) ℤ) → ℤ) (HSub.hSub (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) : ℤ) (0 : ℤ)
Tactic: apply constantCoeff_wittStructureInt p _ _ n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (wittMul p n) : ℤ) (0 : ℤ)
have apply : Eq (α := ℤ)
  ((constantCoeff : (a : MvPolynomial (Fin 2) ℤ) → ℤ) (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) : ℤ) (0 : ℤ)
Tactic: apply constantCoeff_wittStructureInt p _ _ n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → ℤ) (wittNeg p n) : ℤ) (0 : ℤ)
have apply : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 1) ℤ) → ℤ) (-X 0) : ℤ) (0 : ℤ)
Tactic: apply constantCoeff_wittStructureInt p _ _ n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → ℤ) (wittNSMul p m n) : ℤ) (0 : ℤ)
have apply : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 1) ℤ) → ℤ) (HSMul.hSMul (β := MvPolynomial (Fin 1) ℤ) m (X 0)) : ℤ)
  (0 : ℤ)
Tactic: apply constantCoeff_wittStructureInt p _ _ n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
n : ℕ
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 1 × ℕ) ℤ) → ℤ) (wittZSMul p z n) : ℤ) (0 : ℤ)
have apply : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (Fin 1) ℤ) → ℤ) (HSMul.hSMul (β := MvPolynomial (Fin 1) ℤ) z (X 0)) : ℤ)
  (0 : ℤ)
Tactic: apply constantCoeff_wittStructureInt p _ _ n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
Goal:
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
i : Fin 2
⊢ (![x, y] i).coeff = ![x.coeff, y.coeff] i
have 0 : (![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))).coeff = ![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Defs (goal)
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, ⋯⟩)
⊢ (![x, y] i).coeff = ![x.coeff, y.coeff] i
have 1 : (![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))).coeff = ![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
⊢ A * { coeff := inverseCoeff a A : 𝕎 k } = 1
have h : ∀ (n : ℕ), (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
⊢ (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
have h : ∀ (n : ℕ),
  (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n →
    (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) = coeff (p := p) 1 (n + 1)
Tactic: induction n with
    | zero => simp [WittVector.mul_coeff_zero, inverseCoeff, hA]
    | succ n => ?_
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
⊢ (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) = coeff (p := p) 1 (n + 1)
have H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
Tactic: have H := Units.mul_inv (a ^ p ^ (n + 1))
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
⊢ (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) = coeff (p := p) 1 (n + 1)
have a₁ : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) + -H_coeff * 1 -
    (coeff (p := p) 1 (n + 1) + -H_coeff * ((↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k))) =
  0
Tactic: linear_combination (norm := skip) -H_coeff * H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.DiscreteValuationRing (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
⊢ (↑a : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1)) : k)
have norm_cast : a ^ p ^ (n + 1) = a ^ p ^ (n + 1)
Tactic: norm_cast