[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (↑(bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n))
[PROOFSTEP]
rw [bind₁_bind₁]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ i)) (W_ ℚ n)
[PROOFSTEP]
exact eval₂Hom_congr (RingHom.ext_rat _ _) rfl rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (↑(bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n)) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
[PROOFSTEP]
rw [bind₁_xInTermsOfW_wittPolynomial p _ n, bind₁_X_right]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∃! φ, ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
[PROOFSTEP]
refine' ⟨wittStructureRat p Φ, _, _⟩
[GOAL]
case refine'_1
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ (fun φ => ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ) (wittStructureRat p Φ)
[PROOFSTEP]
intro n
[GOAL]
case refine'_1
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
[PROOFSTEP]
apply wittStructureRat_prop
[GOAL]
case refine'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∀ (y : ℕ → MvPolynomial (idx × ℕ) ℚ),
    (fun φ => ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ) y →
      y = wittStructureRat p Φ
[PROOFSTEP]
intro φ H
[GOAL]
case refine'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
⊢ φ = wittStructureRat p Φ
[PROOFSTEP]
funext n
[GOAL]
case refine'_2.h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ φ n = wittStructureRat p Φ n
[PROOFSTEP]
rw [show φ n = bind₁ φ (bind₁ (W_ ℚ) (xInTermsOfW p ℚ n)) by rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ φ n = ↑(bind₁ φ) (↑(bind₁ (W_ ℚ)) (xInTermsOfW p ℚ n))
[PROOFSTEP]
rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]
[GOAL]
case refine'_2.h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ ↑(bind₁ φ) (↑(bind₁ (W_ ℚ)) (xInTermsOfW p ℚ n)) = wittStructureRat p Φ n
[PROOFSTEP]
rw [bind₁_bind₁]
[GOAL]
case refine'_2.h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ ↑(bind₁ fun i => ↑(bind₁ φ) (W_ ℚ i)) (xInTermsOfW p ℚ n) = wittStructureRat p Φ n
[PROOFSTEP]
exact eval₂Hom_congr (RingHom.ext_rat _ _) (funext H) rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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 in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
have := xInTermsOfW_aux p ℚ n
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this : xInTermsOfW p ℚ n * ↑C (↑p ^ n) = X n - ∑ i in 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 in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
replace := congr_arg (bind₁ fun k : ℕ => bind₁ (fun i => rename (Prod.mk i) (W_ ℚ k)) Φ) this
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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 in 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 in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
rw [AlgHom.map_mul, bind₁_C_right] at this 
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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 in 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 in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
rw [wittStructureRat, this]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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 in 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 in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
clear this
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
conv_lhs => simp only [AlgHom.map_sub, bind₁_X_right]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
| ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
    (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
[PROOFSTEP]
simp only [AlgHom.map_sub, bind₁_X_right]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
| ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
    (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
[PROOFSTEP]
simp only [AlgHom.map_sub, bind₁_X_right]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
| ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
    (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
[PROOFSTEP]
simp only [AlgHom.map_sub, bind₁_X_right]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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)) Φ)
        (∑ x in Finset.range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) =
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
rw [sub_right_inj]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (∑ x in Finset.range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
simp only [AlgHom.map_sum, AlgHom.map_mul, bind₁_C_right, AlgHom.map_pow]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ∑ x in 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 in Finset.range n, ↑C (↑p ^ x) * wittStructureRat p Φ x ^ p ^ (n - x)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n =
    ↑C (1 / ↑p ^ n) *
      (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
        ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))
[PROOFSTEP]
calc
  wittStructureRat p Φ n = C (1 / (p : ℚ) ^ n) * (wittStructureRat p Φ n * C ((p : ℚ) ^ n)) := ?_
  _ = _ := by rw [wittStructureRat_rec_aux]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑C (1 / ↑p ^ n) * (wittStructureRat p Φ n * ↑C (↑p ^ n)) =
    ↑C (1 / ↑p ^ n) *
      (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
        ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))
[PROOFSTEP]
rw [wittStructureRat_rec_aux]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n = ↑C (1 / ↑p ^ n) * (wittStructureRat p Φ n * ↑C (↑p ^ n))
[PROOFSTEP]
rw [mul_left_comm, ← C_mul, div_mul_cancel, C_1, mul_one]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑p ^ n ≠ 0
[PROOFSTEP]
exact pow_ne_zero _ (Nat.cast_ne_zero.2 hp.1.ne_zero)
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
[PROOFSTEP]
simp only [map_bind₁, map_rename, map_expand, rename_expand, map_wittPolynomial]
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
have key := (wittStructureRat_prop p (map (Int.castRingHom ℚ) Φ) n).symm
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
apply_fun expand p at key 
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(expand p) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)) =
    ↑(expand p) (↑(bind₁ (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n))
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
simp only [expand_bind₁] at key 
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(expand p) (↑(rename (Prod.mk i)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
rw [key]
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(expand p) (↑(rename (Prod.mk i)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
clear key
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
apply eval₂Hom_congr' rfl _ rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ∀ (i : ℕ),
    i ∈ vars (W_ ℚ n) →
      i ∈ vars (W_ ℚ n) →
        ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
          ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
[PROOFSTEP]
rintro i hi -
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i ∈ vars (W_ ℚ n)
⊢ ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
    ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
[PROOFSTEP]
rw [wittPolynomial_vars, Finset.mem_range] at hi 
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i < n + 1
⊢ ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
    ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
[PROOFSTEP]
simp only [IH i hi]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑C ↑(p ^ n) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
IH :
  ∀ (m : ℕ),
    m < Nat.zero →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑C ↑(p ^ Nat.zero) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ Nat.zero)) Φ -
      ∑ i in Finset.range Nat.zero, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (Nat.zero - i)
[PROOFSTEP]
simp only [isUnit_one, Int.ofNat_zero, Int.ofNat_succ, zero_add, pow_zero, C_1, IsUnit.dvd, Nat.cast_one, Nat.zero_eq]
  -- prepare a useful equation for rewriting
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑C ↑(p ^ Nat.succ n) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ (Nat.succ n))) Φ -
      ∑ i in Finset.range (Nat.succ n), ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (Nat.succ n - i)
[PROOFSTEP]
have key := bind₁_rename_expand_wittPolynomial Φ n IH
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(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 ^ Nat.succ n) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ (Nat.succ n))) Φ -
      ∑ i in Finset.range (Nat.succ n), ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (Nat.succ n - i)
[PROOFSTEP]
apply_fun map (Int.castRingHom (ZMod (p ^ (n + 1)))) at key 
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ ↑C ↑(p ^ Nat.succ n) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ (Nat.succ n))) Φ -
      ∑ i in Finset.range (Nat.succ n), ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (Nat.succ n - i)
[PROOFSTEP]
conv_lhs at key =>
  simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
    -- clean up and massage
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (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))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ)
[PROOFSTEP]
simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
    -- clean up and massage
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (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))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ)
[PROOFSTEP]
simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
    -- clean up and massage
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (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))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ)
[PROOFSTEP]
simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
  -- clean up and massage
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(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))
⊢ ↑C ↑(p ^ Nat.succ n) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ (Nat.succ n))) Φ -
      ∑ i in Finset.range (Nat.succ n), ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (Nat.succ n - i)
[PROOFSTEP]
rw [Nat.succ_eq_add_one, C_dvd_iff_zmod, RingHom.map_sub, sub_eq_zero, map_bind₁]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(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 => ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(rename fun i_1 => (i, i_1)) (W_ ℤ (n + 1))))
      (↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ i in Finset.range (n + 1), ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))
[PROOFSTEP]
simp only [map_rename, map_wittPolynomial, wittPolynomial_zmod_self]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(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)))))
      (∑ x in Finset.range (n + 1), ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))
[PROOFSTEP]
rw [key]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(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)))))
      (∑ x in Finset.range (n + 1), ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))
[PROOFSTEP]
clear key IH
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
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)))))
      (∑ x in Finset.range (n + 1), ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))
[PROOFSTEP]
rw [bind₁, aeval_wittPolynomial, map_sum, map_sum, Finset.sum_congr rfl]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ∀ (x : ℕ),
    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))
[PROOFSTEP]
intro k hk
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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))
[PROOFSTEP]
rw [Finset.mem_range, Nat.lt_succ_iff] at hk 
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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))
[PROOFSTEP]
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]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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))
[PROOFSTEP]
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]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
[PROOFSTEP]
rw [← pow_add, ← add_assoc]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ (k + (n - k) + 1)
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ n = k + (n - k)
[PROOFSTEP]
rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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))
[PROOFSTEP]
rw [this]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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))
[PROOFSTEP]
simp only
  -- Porting note: without this, the next `rw` doesn't do anything
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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))
[PROOFSTEP]
rw [Nat.cast_mul, Nat.cast_pow, Nat.cast_pow]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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))
[PROOFSTEP]
apply mul_dvd_mul_left ((p : MvPolynomial (idx × ℕ) ℤ) ^ k)
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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)
[PROOFSTEP]
rw [show p ^ (n + 1 - k) = p * p ^ (n - k) by rw [← pow_succ, ← tsub_add_eq_add_tsub hk]]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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)
[PROOFSTEP]
rw [← pow_succ, ← tsub_add_eq_add_tsub hk]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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))
[PROOFSTEP]
rw [pow_mul]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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)
[PROOFSTEP]
rw [← Nat.cast_pow]
  -- Porting note: added
    -- the machine!
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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)
[PROOFSTEP]
apply dvd_sub_pow_of_dvd_sub
[GOAL]
case succ.h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
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
[PROOFSTEP]
rw [← C_eq_coe_nat, C_dvd_iff_zmod, RingHom.map_sub, sub_eq_zero, map_expand, RingHom.map_pow, MvPolynomial.expand_zmod]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n
[PROOFSTEP]
induction n using Nat.strong_induction_on with
| h n IH => ?_
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n
[PROOFSTEP]
induction n using Nat.strong_induction_on with
| h n IH => ?_
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n
[PROOFSTEP]
rw [wittStructureInt, map_mapRange_eq_iff, Int.coe_castRingHom]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ∀ (d : idx × ℕ →₀ ℕ),
    (fun x => ↑x) (coeff d (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n)).num =
      coeff d (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n)
[PROOFSTEP]
intro c
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ (fun x => ↑x) (coeff c (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n)).num =
    coeff c (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n)
[PROOFSTEP]
rw [wittStructureRat_rec, coeff_C_mul, mul_comm, mul_div_assoc', mul_one]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ (fun x => ↑x)
      (coeff c
            (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) -
              ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
          ↑p ^ n).num =
    coeff c
        (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) -
          ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
      ↑p ^ n
[PROOFSTEP]
have sum_induction_steps :
  map (Int.castRingHom ℚ) (∑ i in range n, C ((p : ℤ) ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in range n, C ((p : ℚ) ^ i) * wittStructureRat p (map (Int.castRingHom ℚ) Φ) i ^ p ^ (n - i) :=
  by
  rw [map_sum]
  apply Finset.sum_congr rfl
  intro i hi
  rw [Finset.mem_range] at hi 
  simp only [IH i hi, RingHom.map_mul, RingHom.map_pow, map_C]
  rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
[PROOFSTEP]
rw [map_sum]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ ∑ x in Finset.range n, ↑(map (Int.castRingHom ℚ)) (↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ ∀ (x : ℕ),
    x ∈ Finset.range n →
      ↑(map (Int.castRingHom ℚ)) (↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x)) =
        ↑C (↑p ^ x) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) x ^ p ^ (n - x)
[PROOFSTEP]
intro i hi
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
hi : i ∈ Finset.range n
⊢ ↑(map (Int.castRingHom ℚ)) (↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
[PROOFSTEP]
rw [Finset.mem_range] at hi 
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
hi : i < n
⊢ ↑(map (Int.castRingHom ℚ)) (↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
[PROOFSTEP]
simp only [IH i hi, RingHom.map_mul, RingHom.map_pow, map_C]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
hi : i < n
⊢ ↑C (↑(Int.castRingHom ℚ) ↑p) ^ i * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i) =
    ↑C ↑p ^ i * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
[PROOFSTEP]
rfl
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ (fun x => ↑x)
      (coeff c
            (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) -
              ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
          ↑p ^ n).num =
    coeff c
        (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) -
          ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
      ↑p ^ n
[PROOFSTEP]
simp only [← sum_induction_steps, ← map_wittPolynomial p (Int.castRingHom ℚ), ← map_rename, ← map_bind₁, ←
  RingHom.map_sub, coeff_map]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(↑(Int.castRingHom ℚ)
            (coeff c
              (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
                ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))) /
          ↑p ^ n).num =
    ↑(Int.castRingHom ℚ)
        (coeff c
          (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
            ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))) /
      ↑p ^ n
[PROOFSTEP]
rw [show (p : ℚ) ^ n = ((↑(p ^ n) : ℤ) : ℚ) by norm_cast]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑p ^ n = ↑↑(p ^ n)
[PROOFSTEP]
norm_cast
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(↑(Int.castRingHom ℚ)
            (coeff c
              (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
                ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))) /
          ↑↑(p ^ n)).num =
    ↑(Int.castRingHom ℚ)
        (coeff c
          (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
            ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))) /
      ↑↑(p ^ n)
[PROOFSTEP]
rw [← Rat.den_eq_one_iff, eq_intCast, Rat.den_div_cast_eq_one_iff]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ∣
    coeff c
      (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
        ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))
case h.hn
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ≠ 0
[PROOFSTEP]
swap
[GOAL]
case h.hn
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ≠ 0
[PROOFSTEP]
exact_mod_cast pow_ne_zero n hp.1.ne_zero
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ∣
    coeff c
      (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
        ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))
[PROOFSTEP]
revert c
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ∀ (c : idx × ℕ →₀ ℕ),
    ↑(p ^ n) ∣
      coeff c
        (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
          ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))
[PROOFSTEP]
rw [← C_dvd_iff_dvd_coeff]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑C ↑(p ^ n) ∣
    ↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
      ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x)
[PROOFSTEP]
exact C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum Φ n IH
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(bind₁ (wittStructureInt p Φ)) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (↑(bind₁ (wittStructureInt p Φ)) (W_ ℤ n)) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ)
[PROOFSTEP]
have := wittStructureRat_prop p (map (Int.castRingHom ℚ) Φ) n
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
this :
  ↑(bind₁ (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
⊢ ↑(map (Int.castRingHom ℚ)) (↑(bind₁ (wittStructureInt p Φ)) (W_ ℤ n)) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ)
[PROOFSTEP]
simpa only [map_bind₁, ← eval₂Hom_map_hom, eval₂Hom_C_left, map_rename, map_wittPolynomial, AlgHom.coe_toRingHom,
  map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ φ = wittStructureInt p Φ
[PROOFSTEP]
funext k
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ φ k = wittStructureInt p Φ k
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case h.a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (φ k) = ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ k)
[PROOFSTEP]
rw [map_wittStructureInt]
  -- Porting note: was `refine' congr_fun _ k`
[GOAL]
case h.a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
[PROOFSTEP]
revert k
[GOAL]
case h.a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (k : ℕ), ↑(map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
[PROOFSTEP]
refine' congr_fun _
[GOAL]
case h.a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ (fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) = fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
[PROOFSTEP]
apply ExistsUnique.unique (wittStructureRat_existsUnique p (map (Int.castRingHom ℚ) Φ))
[GOAL]
case h.a.py₁
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (n : ℕ),
    ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
      ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
intro n
[GOAL]
case h.a.py₁
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
specialize h n
[GOAL]
case h.a.py₁
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h : ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
apply_fun map (Int.castRingHom ℚ) at h 
[GOAL]
case h.a.py₁
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h :
  ↑(map (Int.castRingHom ℚ)) (↑(bind₁ φ) (W_ ℤ n)) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ)
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
simpa only [map_bind₁, ← eval₂Hom_map_hom, eval₂Hom_C_left, map_rename, map_wittPolynomial, AlgHom.coe_toRingHom] using
  h
[GOAL]
case h.a.py₂
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (n : ℕ),
    ↑(bind₁ fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k) (W_ ℚ n) =
      ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
intro n
[GOAL]
case h.a.py₂
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
n : ℕ
⊢ ↑(bind₁ fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
apply wittStructureRat_prop
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(aeval fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    ↑(aeval fun i => ↑(rename (Prod.mk i)) (W_ R n)) Φ
[PROOFSTEP]
convert congr_arg (map (Int.castRingHom R)) (wittStructureInt_prop p Φ n) using 1
[GOAL]
case h.e'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(aeval fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    ↑(map (Int.castRingHom R)) (↑(bind₁ (wittStructureInt p Φ)) (W_ ℤ n))
[PROOFSTEP]
rw [hom_bind₁]
[GOAL]
case h.e'_3
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(aeval fun i => ↑(rename (Prod.mk i)) (W_ R n)) Φ =
    ↑(map (Int.castRingHom R)) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ)
[PROOFSTEP]
rw [hom_bind₁]
[GOAL]
case h.e'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(aeval fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    ↑(eval₂Hom (RingHom.comp (map (Int.castRingHom R)) C) fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i))
      (W_ ℤ n)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
case h.e'_3
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(aeval fun i => ↑(rename (Prod.mk i)) (W_ R n)) Φ =
    ↑(eval₂Hom (RingHom.comp (map (Int.castRingHom R)) C) fun i =>
          ↑(map (Int.castRingHom R)) (↑(rename (Prod.mk i)) (W_ ℤ n)))
      Φ
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)) = fun i =>
    ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => ↑(rename (Prod.mk i)) (W_ R n)) = fun i => ↑(map (Int.castRingHom R)) (↑(rename (Prod.mk i)) (W_ ℤ n))
[PROOFSTEP]
simp only [map_rename, map_wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ wittStructureInt p (↑(rename f) Φ) n = ↑(rename (Prod.map f id)) (wittStructureInt p Φ n)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittStructureInt p (↑(rename f) Φ) n) =
    ↑(map (Int.castRingHom ℚ)) (↑(rename (Prod.map f id)) (wittStructureInt p Φ n))
[PROOFSTEP]
simp only [map_rename, map_wittStructureInt, wittStructureRat, rename_bind₁, rename_rename, bind₁_rename]
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(bind₁ ((fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) ∘ f)) (↑(map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n) =
    ↑(bind₁ fun i =>
          ↑(bind₁ fun i_1 => ↑(rename (Prod.map f id ∘ Prod.mk i_1)) (W_ ℚ i)) (↑(map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ↑constantCoeff (wittStructureRat p Φ 0) = ↑constantCoeff Φ
[PROOFSTEP]
simp only [wittStructureRat, bind₁, map_aeval, xInTermsOfW_zero, constantCoeff_rename, constantCoeff_wittPolynomial,
  aeval_X, constantCoeff_comp_algebraMap, eval₂Hom_zero'_apply, RingHom.id_apply]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
h : ↑constantCoeff Φ = 0
n : ℕ
⊢ ↑constantCoeff (wittStructureRat p Φ n) = 0
[PROOFSTEP]
simp only [wittStructureRat, eval₂Hom_zero'_apply, h, bind₁, map_aeval, constantCoeff_rename,
  constantCoeff_wittPolynomial, constantCoeff_comp_algebraMap, RingHom.id_apply, constantCoeff_xInTermsOfW]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ ↑constantCoeff (wittStructureInt p Φ 0) = ↑constantCoeff Φ
[PROOFSTEP]
have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ Function.Injective ↑(Int.castRingHom ℚ)
[PROOFSTEP]
intro m n
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
m n : ℤ
⊢ ↑(Int.castRingHom ℚ) m = ↑(Int.castRingHom ℚ) n → m = n
[PROOFSTEP]
exact Int.cast_inj.mp
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑constantCoeff (wittStructureInt p Φ 0) = ↑constantCoeff Φ
[PROOFSTEP]
apply inj
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑(Int.castRingHom ℚ) (↑constantCoeff (wittStructureInt p Φ 0)) = ↑(Int.castRingHom ℚ) (↑constantCoeff Φ)
[PROOFSTEP]
rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat_zero, constantCoeff_map]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n : ℕ
⊢ ↑constantCoeff (wittStructureInt p Φ n) = 0
[PROOFSTEP]
have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n : ℕ
⊢ Function.Injective ↑(Int.castRingHom ℚ)
[PROOFSTEP]
intro m n
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n✝ : ℕ
m n : ℤ
⊢ ↑(Int.castRingHom ℚ) m = ↑(Int.castRingHom ℚ) n → m = n
[PROOFSTEP]
exact Int.cast_inj.mp
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑constantCoeff (wittStructureInt p Φ n) = 0
[PROOFSTEP]
apply inj
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑(Int.castRingHom ℚ) (↑constantCoeff (wittStructureInt p Φ n)) = ↑(Int.castRingHom ℚ) 0
[PROOFSTEP]
rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat, RingHom.map_zero]
[GOAL]
case a.h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑constantCoeff (↑(map (Int.castRingHom ℚ)) Φ) = 0
[PROOFSTEP]
rw [constantCoeff_map, h, RingHom.map_zero]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ vars (wittStructureRat p Φ n) ⊆ Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
rw [wittStructureRat]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)) ⊆
    Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
intro x hx
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
⊢ x ∈ Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
simp only [Finset.mem_product, true_and_iff, Finset.mem_univ, Finset.mem_range]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
⊢ x.snd < n + 1
[PROOFSTEP]
obtain ⟨k, hk, hx'⟩ := mem_vars_bind₁ _ _ hx
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' : x ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
⊢ x.snd < n + 1
[PROOFSTEP]
obtain ⟨i, -, hx''⟩ := mem_vars_bind₁ _ _ hx'
[GOAL]
case intro.intro.intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' : x ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
i : idx
hx'' : x ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ x.snd < n + 1
[PROOFSTEP]
obtain ⟨j, hj, rfl⟩ := mem_vars_rename _ _ hx''
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j ∈ vars (W_ ℚ k)
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ (i, j).snd < n + 1
[PROOFSTEP]
rw [wittPolynomial_vars, Finset.mem_range] at hj 
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ (i, j).snd < n + 1
[PROOFSTEP]
replace hk := xInTermsOfW_vars_subset p _ hk
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
hk : k ∈ Finset.range (n + 1)
⊢ (i, j).snd < n + 1
[PROOFSTEP]
rw [Finset.mem_range] at hk 
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
hk : k < n + 1
⊢ (i, j).snd < n + 1
[PROOFSTEP]
exact lt_of_lt_of_le hj hk
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ vars (wittStructureInt p Φ n) ⊆ Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
have : Function.Injective (Int.castRingHom ℚ) := Int.cast_injective
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ↑(Int.castRingHom ℚ)
⊢ vars (wittStructureInt p Φ n) ⊆ Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
rw [← vars_map_of_injective _ this, map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ↑(Int.castRingHom ℚ)
⊢ vars (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n) ⊆ Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
apply wittStructureRat_vars
