awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
succ :
  ∀ x ∈ Finset.range (n + 1),
    Eq (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
            (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
          (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) x *
            HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
              ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ x) :
                MvPolynomial (idx × ℕ) ℤ)
              (p ^ (n - x))) :
        MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
            (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
          (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
            ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x) : MvPolynomial (idx × ℕ) ℤ)
            (wittStructureInt p Φ x ^ p ^ (n + 1 - x))) :
        MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
⊢ Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        ((bind₁ fun (i : ℕ) ↦
                (expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ i) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
            (W_ ℤ n) :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (∑ i ∈ Finset.range (n + 1),
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
            ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
            (wittStructureInt p Φ i ^ p ^ (n + 1 - i))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))

Tactic:
rw [bind₁, aeval_wittPolynomial, map_sum, map_sum, Finset.sum_congr rfl]

Premises used: aeval_wittPolynomial, map_sum, MvPolynomial.bind₁, Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ k ≤ n

Tactic:
rw [Finset.mem_range, Nat.lt_succ_iff] at hk

Premises used: Finset.mem_range, Nat.lt_succ_iff
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
succ :
  (↑(p ^ (n + 1)) : MvPolynomial (idx × ℕ) ℤ) ∣
    (↑(p ^ k) : MvPolynomial (idx × ℕ) ℤ) *
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ)
          (p ^ (n - k)) -
        wittStructureInt p Φ k ^ p ^ (n + 1 - k))
⊢ Eq (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) k *
          HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
            ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
              MvPolynomial (idx × ℕ) ℤ)
            (p ^ (n - k))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
          ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) k) : MvPolynomial (idx × ℕ) ℤ)
          (wittStructureInt p Φ k ^ p ^ (n + 1 - k))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))

Tactic:
rw [← sub_eq_zero, ← map_sub, ← C_dvd_iff_zmod, C_eq_coe_nat, ← Nat.cast_pow,
    ← Nat.cast_pow, C_eq_coe_nat, ← mul_sub]

Premises used: map_sub, mul_sub, sub_eq_zero, MvPolynomial.C_eq_coe_nat, Nat.cast_pow, MvPolynomial.C_dvd_iff_zmod
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
rw : p ^ (n + 1) = p ^ (k + (n - k) + 1)
⊢ p ^ (n + 1) = p ^ k * p ^ (n - k + 1)

Tactic:
rw [← pow_add, ← add_assoc]

Premises used: add_assoc, pow_add
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
e_a : n = k + (n - k)
⊢ p ^ (n + 1) = p ^ (k + (n - k) + 1)

Tactic:
congr 2
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
e_a : n = n - k + k
e_a₁ e_a₂ : n - k = n - k
⊢ n = k + (n - k)

Tactic:
rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk]

Premises used: add_comm, tsub_eq_iff_eq_add_of_le
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ k * p ^ (n - k + 1)

Tactic:
have : p ^ (n + 1) = p ^ k * p ^ (n - k + 1) := by
    rw [← pow_add, ← add_assoc]; congr 2; rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk]
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
succ :
  (↑(p ^ k * p ^ (n - k + 1)) : MvPolynomial (idx × ℕ) ℤ) ∣
    (↑(p ^ k) : MvPolynomial (idx × ℕ) ℤ) *
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ)
          (p ^ (n - k)) -
        wittStructureInt p Φ k ^ p ^ (n + 1 - k))
⊢ (↑(p ^ (n + 1)) : MvPolynomial (idx × ℕ) ℤ) ∣
    (↑(p ^ k) : MvPolynomial (idx × ℕ) ℤ) *
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ)
          (p ^ (n - k)) -
        wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
succ :
  HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) k *
      HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) k *
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ)
          (p ^ (n - k)) -
        wittStructureInt p Φ k ^ p ^ (n + 1 - k))
⊢ (↑(p ^ k * p ^ (n - k + 1)) : MvPolynomial (idx × ℕ) ℤ) ∣
    (↑(p ^ k) : MvPolynomial (idx × ℕ) ℤ) *
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ)
          (p ^ (n - k)) -
        wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
rw [Nat.cast_mul, Nat.cast_pow, Nat.cast_pow]

Premises used: Nat.cast_mul, Nat.cast_pow
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
succ :
  HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      wittStructureInt p Φ k ^ p ^ (n + 1 - k)
⊢ HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) k *
      HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) k *
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ)
          (p ^ (n - k)) -
        wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
apply mul_dvd_mul_left ((p : MvPolynomial (idx × ℕ) ℤ) ^ k)

Premises used: mul_dvd_mul_left, Nat.cast, HPow.hPow
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
rw : p ^ (n + 1 - k) = p ^ (n - k + 1)
rw₁ rw₂ : p ^ (n - k + 1) = p ^ (n - k + 1)
⊢ p ^ (n + 1 - k) = p * p ^ (n - k)

Tactic:
rw [← pow_succ', ← tsub_add_eq_add_tsub hk]

Premises used: tsub_add_eq_add_tsub, pow_succ'
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
succ :
  HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      wittStructureInt p Φ k ^ (p * p ^ (n - k))
⊢ HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      wittStructureInt p Φ k ^ p ^ (n + 1 - k)

Tactic:
rw [show p ^ (n + 1 - k) = p * p ^ (n - k) by rw [← pow_succ', ← tsub_add_eq_add_tsub hk]]
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
succ :
  HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      (wittStructureInt p Φ k ^ p) ^ p ^ (n - k)
⊢ HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      wittStructureInt p Φ k ^ (p * p ^ (n - k))

Tactic:
rw [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
succ :
  (↑p : MvPolynomial (idx × ℕ) ℤ) ∣
    HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ)
      ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
        MvPolynomial (idx × ℕ) ℤ)
      (wittStructureInt p Φ k ^ p)
⊢ HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) (n - k + 1) ∣
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      (wittStructureInt p Φ k ^ p) ^ p ^ (n - k)

Tactic:
apply dvd_sub_pow_of_dvd_sub

Premises used: dvd_sub_pow_of_dvd_sub
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ n) :
      MvPolynomial (idx × ℕ) ℚ)
    (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n :
      MvPolynomial (idx × ℕ) ℚ)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
h :
  ∀ (n : ℕ)
    (IH :
      ∀ m < n,
        Eq (α := MvPolynomial (idx × ℕ) ℚ)
          ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
              (wittStructureInt p Φ m) :
            MvPolynomial (idx × ℕ) ℚ)
          (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
            MvPolynomial (idx × ℕ) ℚ)),
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ n) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n :
        MvPolynomial (idx × ℕ) ℚ)
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ n) :
      MvPolynomial (idx × ℕ) ℚ)
    (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n :
      MvPolynomial (idx × ℕ) ℚ)

Tactic:
induction n using Nat.strong_induction_on with | h n IH => ?_
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
h :
  ∀ (d : idx × ℕ →₀ ℕ),
    (fun (x : ℤ) ↦ ((↑x : ℚ) : ℚ))
        (coeff d
            (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n)).num =
      coeff d (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n)
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ n) :
      MvPolynomial (idx × ℕ) ℚ)
    (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n :
      MvPolynomial (idx × ℕ) ℚ)

Tactic:
rw [wittStructureInt, map_mapRange_eq_iff, Int.coe_castRingHom]

Premises used: MvPolynomial.map_mapRange_eq_iff, Int.coe_castRingHom, wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
c : idx × ℕ →₀ ℕ
h :
  (fun (x : ℤ) ↦ ((↑x : ℚ) : ℚ))
      (coeff c
            (HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
              ((bind₁ fun (b : idx) ↦
                      (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
                    (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
                  ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
                MvPolynomial (idx × ℕ) ℚ)
              (∑ i ∈ Finset.range n,
                  HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
                    ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) :
                      MvPolynomial (idx × ℕ) ℚ)
                    (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
                      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ)
                        i)
                      (p ^ (n - i))) :
                MvPolynomial (idx × ℕ) ℚ)) /
          HPow.hPow (α := ℚ) (↑p : ℚ) n).num =
    coeff c
        (HSub.hSub (α := MvPolynomial (idx × ℕ) ℚ) (β := MvPolynomial (idx × ℕ) ℚ)
          ((bind₁ fun (b : idx) ↦
                  (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
            MvPolynomial (idx × ℕ) ℚ)
          (∑ i ∈ Finset.range n,
              HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
                ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
                (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
                  (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
                  (p ^ (n - i))) :
            MvPolynomial (idx × ℕ) ℚ)) /
      HPow.hPow (α := ℚ) (↑p : ℚ) n
⊢ (fun (x : ℤ) ↦ ((↑x : ℚ) : ℚ))
      (coeff c
          (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n)).num =
    coeff c (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n)

Tactic:
rw [wittStructureRat_rec, coeff_C_mul, mul_comm, mul_div_assoc', mul_one]

Premises used: MvPolynomial.coeff_C_mul, mul_div_assoc', wittStructureRat_rec, mul_comm, mul_one
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
c : idx × ℕ →₀ ℕ
rw :
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    (∑ x ∈ Finset.range n,
      (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
          ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x) : MvPolynomial (idx × ℕ) ℤ)
          (wittStructureInt p Φ x ^ p ^ (n - x))))
    (∑ i ∈ Finset.range n,
      HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
        (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
          (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
          (p ^ (n - i))))
⊢ Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        (∑ i ∈ Finset.range n,
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
            ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
            (wittStructureInt p Φ i ^ p ^ (n - i))) :
      MvPolynomial (idx × ℕ) ℚ)
    (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
          ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
          (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
            (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
            (p ^ (n - i))) :
      MvPolynomial (idx × ℕ) ℚ)

Tactic:
rw [map_sum]

Premises used: map_sum
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
c : idx × ℕ →₀ ℕ
apply :
  ∀ x ∈ Finset.range n,
    (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
          ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x) : MvPolynomial (idx × ℕ) ℤ)
          (wittStructureInt p Φ x ^ p ^ (n - x))) =
      HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) x) : MvPolynomial (idx × ℕ) ℚ)
        (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
          (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) x)
          (p ^ (n - x)))
⊢ Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    (∑ x ∈ Finset.range n,
      (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
          ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x) : MvPolynomial (idx × ℕ) ℤ)
          (wittStructureInt p Φ x ^ p ^ (n - x))))
    (∑ i ∈ Finset.range n,
      HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
        (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
          (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
          (p ^ (n - i))))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
c : idx × ℕ →₀ ℕ
i : ℕ
hi : i ∈ Finset.range n
⊢ i < n

Tactic:
rw [Finset.mem_range] at hi

Premises used: Finset.mem_range