-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem mul_polyOfInterest_aux1 (n : ℕ) :
    ∑ i ∈ range (n + 1), (p : 𝕄) ^ i * wittMul p i ^ p ^ (n - i) = wittPolyProd p n

Proof state:
case h.e'_2.e_f.h.a
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i)) =
    MvPolynomial.coeff m✝
      ((bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)))

Tactic:
congr 1

Result:
case h.e'_2.e_f.h.a.e_p
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ ↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i) =
    (bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))

Proof state:
case h.e'_2.e_f.h.a.e_p
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ ↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i) =
    (bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))

Tactic:
have hsupp : (Finsupp.single i (p ^ (n - i))).support = {i} := by
  rw [Finsupp.support_eq_singleton]
  simp only [and_true, Finsupp.single_eq_same, eq_self_iff_true, Ne]
  exact pow_ne_zero _ hp.out.ne_zero

Result:
case h.e'_2.e_f.h.a.e_p
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
hsupp : (Finsupp.single i (p ^ (n - i))).support = {i}
⊢ ↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i) =
    (bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) =
    (rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n)

Tactic:
convert wittStructureInt_prop p (X (0 : Fin 2) * X 1) n using 1

Result:
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) =
    (bind₁ (wittStructureInt p (X 0 * X 1))) (wittPolynomial p ℤ n)

case h.e'_3
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n) =
    (bind₁ fun i => (rename (Prod.mk i)) (wittPolynomial p ℤ n)) (X 0 * X 1)

Proof state:
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ x ∈ range (n + 1), ↑p ^ x * wittStructureInt p (X 0 * X 1) x ^ p ^ (n - x) =
    ∑ x ∈ range (n + 1), (bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single x (p ^ (n - x)))) (↑p ^ x))

Tactic:
congr 1 with i

Result:
case h.e'_2.e_f.h.a
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i)) =
    MvPolynomial.coeff m✝
      ((bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)))

Proof state:
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ x ∈ range (n + 1), ↑p ^ x * wittStructureInt p (X 0 * X 1) x ^ p ^ (n - x) =
    (bind₁ (wittStructureInt p (X 0 * X 1))) (∑ i ∈ range (n + 1), (monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))

Tactic:
rw [map_sum]

Result:
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ x ∈ range (n + 1), ↑p ^ x * wittStructureInt p (X 0 * X 1) x ^ p ^ (n - x) =
    ∑ x ∈ range (n + 1), (bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single x (p ^ (n - x)))) (↑p ^ x))

Proof state:
case h.e'_3
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n) =
    (bind₁ fun i => (rename (Prod.mk i)) (wittPolynomial p ℤ n)) (X 0 * X 1)

Tactic:
simp only [map_mul, bind₁_X_right]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ (Finsupp.single i (p ^ (n - i))).support = {i}

Tactic:
rw [Finsupp.support_eq_singleton]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ (Finsupp.single i (p ^ (n - i))) i ≠ 0 ∧
    Finsupp.single i (p ^ (n - i)) = Finsupp.single i ((Finsupp.single i (p ^ (n - i))) i)

Proof state:
case h.e'_2.e_f.h.a.e_p
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
hsupp : (Finsupp.single i (p ^ (n - i))).support = {i}
⊢ ↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i) =
    (bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))

Tactic:
simp only [bind₁_monomial, hsupp, Int.cast_natCast, prod_singleton, eq_intCast,
  Finsupp.single_eq_same, C_pow, mul_eq_mul_left_iff, eq_self_iff_true, Int.cast_pow]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ ¬p ^ (n - i) = 0

Tactic:
exact pow_ne_zero _ hp.out.ne_zero

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ (Finsupp.single i (p ^ (n - i))) i ≠ 0 ∧
    Finsupp.single i (p ^ (n - i)) = Finsupp.single i ((Finsupp.single i (p ^ (n - i))) i)

Tactic:
simp only [and_true, Finsupp.single_eq_same, eq_self_iff_true, Ne]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ ¬p ^ (n - i) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) = wittPolyProd p n

Tactic:
simp only [wittPolyProd]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) =
    (rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n)

Proof state:
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) =
    (bind₁ (wittStructureInt p (X 0 * X 1))) (wittPolynomial p ℤ n)

Tactic:
simp only [wittPolynomial, wittMul]

Result:
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ x ∈ range (n + 1), ↑p ^ x * wittStructureInt p (X 0 * X 1) x ^ p ^ (n - x) =
    (bind₁ (wittStructureInt p (X 0 * X 1))) (∑ i ∈ range (n + 1), (monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))