-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem wittStructureRat_rec_aux (Φ : MvPolynomial idx ℚ) (n : ℕ) :
    wittStructureRat p Φ n * C ((p : ℚ) ^ n) =
      bind₁ (fun b => rename (fun i => (b, i)) (W_ ℚ n)) Φ -
        ∑ i ∈ range n, C ((p : ℚ) ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ∑ x ∈ Finset.range n,
      C ↑p ^ x * (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ x) ^ p ^ (n - x) =
    ∑ x ∈ Finset.range n, C ↑p ^ x * wittStructureRat p Φ x ^ p ^ (n - x)

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n * C (↑p ^ n)) =
    (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ wittStructureRat p Φ n * C (↑p ^ n) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Tactic:
rw [map_mul, bind₁_C_right] at this

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * C (↑p ^ n) =
    (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ wittStructureRat p Φ n * C (↑p ^ n) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this : xInTermsOfW p ℚ n * C (↑p ^ n) = X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)
⊢ wittStructureRat p Φ n * C (↑p ^ n) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Tactic:
replace := congr_arg (bind₁ fun k : ℕ => bind₁ (fun i => rename (Prod.mk i) (W_ ℚ k)) Φ) this

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n * C (↑p ^ n)) =
    (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ wittStructureRat p Φ n * C (↑p ^ n) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * C (↑p ^ n) =
    (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Tactic:
clear this

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n * C (↑p ^ n) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Tactic:
have := xInTermsOfW_aux p ℚ n

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this : xInTermsOfW p ℚ n * C (↑p ^ n) = X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)
⊢ wittStructureRat p Φ n * C (↑p ^ n) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Tactic:
conv_lhs => simp only [map_sub, bind₁_X_right]

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) Φ -
      (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
        (∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) Φ -
      (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
        (∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Tactic:
rw [sub_right_inj]

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Tactic:
simp only [map_sum, map_mul, bind₁_C_right, map_pow]

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ∑ x ∈ Finset.range n,
      C ↑p ^ x * (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ x) ^ p ^ (n - x) =
    ∑ x ∈ Finset.range n, C ↑p ^ x * wittStructureRat p Φ x ^ p ^ (n - x)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * C (↑p ^ n) =
    (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ wittStructureRat p Φ n * C (↑p ^ n) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Tactic:
rw [wittStructureRat, this]

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * C (↑p ^ n) =
    (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)