-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum (Φ : MvPolynomial idx ℤ) (n : ℕ)
    (IH :
      ∀ m : ℕ,
        m < n →
          map (Int.castRingHom ℚ) (wittStructureInt p Φ m) =
            wittStructureRat p (map (Int.castRingHom ℚ) Φ) m) :
    (C ((p ^ n :) : ℤ) : MvPolynomial (idx × ℕ) ℤ) ∣
      bind₁ (fun b : idx => rename (fun i => (b, i)) (wittPolynomial p ℤ n)) Φ -
        ∑ i ∈ range n, C ((p : ℤ) ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)

Proof state:
case succ.h
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)
⊢ ↑p ∣ (expand p) (wittStructureInt p Φ k) - wittStructureInt p Φ k ^ p

Tactic:
rw [← C_eq_coe_nat, C_dvd_iff_zmod, RingHom.map_sub, sub_eq_zero, map_expand, RingHom.map_pow,
  MvPolynomial.expand_zmod]

Result:
no goals

Proof state:
case succ
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)
⊢ ↑p ^ (n - k + 1) ∣ (expand p) (wittStructureInt p Φ k) ^ 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]]

Result:
case succ
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)
⊢ ↑p ^ (n - k + 1) ∣ (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ (p * p ^ (n - k))

Proof state:
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)
⊢ p ^ (n + 1 - k) = p * p ^ (n - k)

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

Result:
no goals

Proof state:
case succ
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)
⊢ ↑p ^ k * ↑p ^ (n - k + 1) ∣
    ↑p ^ k * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

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

Result:
case succ
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)
⊢ ↑p ^ (n - k + 1) ∣ (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k)

Proof state:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ ↑(p ^ (n + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

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]

Result:
case succ
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)
⊢ ↑(p ^ (n + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Proof state:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ x * (expand p) (wittStructureInt p Φ x) ^ p ^ (n - x)) =
      (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))

Tactic:
intro k hk

Result:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Proof state:
case succ
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)
⊢ ↑(p ^ (n + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
rw [this]

Result:
case succ
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)
⊢ ↑(p ^ k * p ^ (n - k + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Proof state:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (bind₁ fun i => (rename fun i_1 => (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ (bind₁ fun i => (rename fun i_1 => (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))

Tactic:
rw [key]

Result:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (bind₁ fun i => (rename fun i_1 => (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n)) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ (k + (n - k) + 1)

Tactic:
congr 2

Result:
case e_a.e_a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ n = k + (n - k)

Proof state:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k))

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

Result:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ ↑(p ^ (n + 1)) ∣
    ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Proof state:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
⊢ C ↑(p ^ (n + 1)) ∣
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℤ (n + 1))) Φ -
      ∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i)

Tactic:
have key := bind₁_rename_expand_wittPolynomial Φ n IH

Result:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (bind₁ fun b => (rename fun i => (b, i)) ((expand p) (W_ ℤ n))) Φ =
    (bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n)
⊢ C ↑(p ^ (n + 1)) ∣
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℤ (n + 1))) Φ -
      ∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i)