awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H :
  n ∈
    (HMul.hMul (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) j) : MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j)))).vars
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) j ≠ 0
have ind : Ne (α := ℚ) (↑p : ℚ) 0
Tactic: apply pow_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars
⊢ False
have hj₁ : j < n
Tactic: rw [mem_range] at hj
Cleared hypotheses: hj, H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars
⊢ False
have H₁ : n ∈ range (j + 1)
Tactic: replace H := (ih j hj).2 (vars_pow _ _ H)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ range (j + 1)
⊢ False
have H₁ : n < j + 1
Tactic: rw [mem_range] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i ∈ range n
have ind : i < n
Tactic: rw [mem_range]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
⊢ HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (xInTermsOfW p R n)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R) =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
have rw : HMul.hMul (β := MvPolynomial ℕ R)
    (HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X n)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R))
    ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R) =
  HSub.hSub (α := MvPolynomial ℕ R) (X n)
    (∑ i ∈ range n,
      HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
Tactic: rw [xInTermsOfW_eq, mul_assoc, ← C_mul, ← mul_pow, invOf_mul_self,
    one_pow, C_1, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
rw :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (β := MvPolynomial ℕ R)
        (HSub.hSub (α := MvPolynomial ℕ R) (X n)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ R)
              ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
              (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))))
        ((C : (a : R) → MvPolynomial ℕ R)
            (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
          MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R) =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
⊢ HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (xInTermsOfW p R n)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R) =
    HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
have rw₁ : HSub.hSub (α := MvPolynomial ℕ R) (X n)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i)))) *
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R) =
  HSub.hSub (α := MvPolynomial ℕ R) (X n)
    (∑ i ∈ range n,
      HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
Tactic: rw [xInTermsOfW_eq, mul_assoc, ← C_mul, ← mul_pow, invOf_mul_self,
    one_pow, C_1, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
k : ℕ
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (W_ R k) : MvPolynomial ℕ R)
    (X k : MvPolynomial ℕ R)
have rw : Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
  (∑ x ∈ range (k + 1),
    (bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (X x) (p ^ (k - x)))))
  (X k)
Tactic: rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
k : ℕ
⊢ Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
    (∑ x ∈ range (k + 1),
      (bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
        (HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (X x) (p ^ (k - x)))))
    (X k)
have simp : Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
  (∑ x ∈ range (k + 1),
    HPow.hPow (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (↑p : R)) x *
      HPow.hPow (α := MvPolynomial ℕ R)
        ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (X x) : MvPolynomial ℕ R) (p ^ (k - x)))
  (X k)
Tactic: simp only [map_pow, map_mul, algHom_C, algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
k : ℕ
⊢ Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
    (∑ x ∈ range (k + 1),
      HPow.hPow (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (↑p : R)) x *
        HPow.hPow (α := MvPolynomial ℕ R)
          ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (X x) : MvPolynomial ℕ R)
          (p ^ (k - x)))
    (X k)
have rw : HSub.hSub (α := MvPolynomial ℕ R) (X k)
      (∑ i ∈ range k,
        HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (k - i)))) +
    ∑ x ∈ range k,
      HPow.hPow (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (↑p : R)) x *
        HPow.hPow (α := MvPolynomial ℕ R)
          ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (X x) : MvPolynomial ℕ R)
          (p ^ (k - x)) =
  X k
Tactic: rw [sum_range_succ_comm, tsub_self, pow_zero, pow_one, bind₁_X_right, mul_comm, ← C_pow,
    xInTermsOfW_aux]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R n) : MvPolynomial ℕ R)
    (X n : MvPolynomial ℕ R)
have ind : ∀ (n : ℕ)
  (H :
    ∀ m < n,
      Eq (α := MvPolynomial ℕ R)
        ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
        (X m : MvPolynomial ℕ R)),
  Eq (α := MvPolynomial ℕ R)
    ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R n) : MvPolynomial ℕ R)
    (X n : MvPolynomial ℕ R)
Tactic: induction n using Nat.strongRecOn with | ind n H => ?_
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
⊢ X n =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
have rw : X n =
  X n *
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
Tactic: rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
rw :
  X n =
    X n *
      HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R)
            (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
          MvPolynomial ℕ R)
⊢ X n =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
have rw₁ : X n =
  HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
    ((C : (a : R) → MvPolynomial ℕ R)
        (HPow.hPow (α := R) (↑p : R) n *
          HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
      MvPolynomial ℕ R)
Tactic: rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
rw :
  X n =
    X n *
      HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R)
            (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
          MvPolynomial ℕ R)
rw₁ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (↑p : R) n *
            HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
⊢ X n =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
have rw₂ : X n =
  HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
    ((C : (a : R) → MvPolynomial ℕ R)
        (HMul.hMul (α := R) (↑p : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) ^ n) :
      MvPolynomial ℕ R)
Tactic: rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
rw :
  X n =
    X n *
      HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R)
            (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
          MvPolynomial ℕ R)
rw₁ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (↑p : R) n *
            HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
rw₂ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HMul.hMul (α := R) (↑p : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) ^ n) :
        MvPolynomial ℕ R)
⊢ X n =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
have rw₃ : X n =
  HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
    ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) 1 n) : MvPolynomial ℕ R)
Tactic: rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
rw :
  X n =
    X n *
      HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R)
            (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
          MvPolynomial ℕ R)
rw₁ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (↑p : R) n *
            HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
rw₂ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HMul.hMul (α := R) (↑p : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) ^ n) :
        MvPolynomial ℕ R)
rw₃ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) 1 n) : MvPolynomial ℕ R)
⊢ X n =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
have rw₄ : X n = HMul.hMul (α := MvPolynomial ℕ R) (X n) ((C : (a : R) → MvPolynomial ℕ R) 1)
Tactic: rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
rw :
  X n =
    X n *
      HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R)
            (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
          MvPolynomial ℕ R)
rw₁ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (↑p : R) n *
            HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
rw₂ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HMul.hMul (α := R) (↑p : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) ^ n) :
        MvPolynomial ℕ R)
rw₃ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) 1 n) : MvPolynomial ℕ R)
rw₄ : X n = HMul.hMul (α := MvPolynomial ℕ R) (X n) ((C : (a : R) → MvPolynomial ℕ R) 1)
⊢ X n =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
have rw₅ : X n = HMul.hMul (α := MvPolynomial ℕ R) (X n) 1
Tactic: rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
rw :
  X n =
    X n *
      HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R)
            (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
          MvPolynomial ℕ R)
rw₁ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (↑p : R) n *
            HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
rw₂ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HMul.hMul (α := R) (↑p : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) ^ n) :
        MvPolynomial ℕ R)
rw₃ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) 1 n) : MvPolynomial ℕ R)
rw₄ : X n = HMul.hMul (α := MvPolynomial ℕ R) (X n) ((C : (a : R) → MvPolynomial ℕ R) 1)
rw₅ : X n = HMul.hMul (α := MvPolynomial ℕ R) (X n) 1
⊢ X n =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
have rw₆ : Eq.{u_1 + 1} (α := MvPolynomial ℕ R) (X n) (X n)
Tactic: rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R n) : MvPolynomial ℕ R)
    (X n : MvPolynomial ℕ R)
have ind : HMul.hMul (β := MvPolynomial ℕ R)
    (HSub.hSub (α := MvPolynomial ℕ R) (W_ R n)
      (∑ x ∈ range n,
        (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          (HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x))))))
    ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R)
        (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
      MvPolynomial ℕ R) =
  HMul.hMul (β := MvPolynomial ℕ R)
    (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
    ((C : (a : R) → MvPolynomial ℕ R)
        (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
      MvPolynomial ℕ R)
Tactic: rw [xInTermsOfW_eq, map_mul, map_sub, bind₁_X_right, algHom_C, map_sum,
    show X n = (X n * C ((p : R) ^ n)) * C ((⅟p : R) ^ n) by
      rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]]