case zero
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)

case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
cases' n with n
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
have key := bind₁_rename_expand_wittPolynomial Φ n IH
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
apply_fun map (Int.castRingHom (ZMod (p ^ (n + 1))))  at key
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
conv_lhs at key => simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
rw [Nat.succ_eq_add_one, C_dvd_iff_zmod, RingHom.map_sub, sub_eq_zero, map_bind₁]
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
simp only [map_rename, map_wittPolynomial, wittPolynomial_zMod_self]
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
rw [key]
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
clear key IH
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
rw [bind₁, aeval_wittPolynomial, map_sum, map_sum, Finset.sum_congr rfl]
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
intro k hk
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
rw [Finset.mem_range, Nat.lt_succ_iff] at hk
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
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]
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
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]
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
rw [this]
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
simp only
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
rw [Nat.cast_mul, Nat.cast_pow, Nat.cast_pow]
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
apply mul_dvd_mul_left ((p : MvPolynomial (idx × ℕ) ℤ) ^ k)
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
rw [show p ^ (n + 1 - k) = p * p ^ (n - k) by rw [← pow_succ, ← tsub_add_eq_add_tsub hk]]
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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))
rw [pow_mul]
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
rw [← Nat.cast_pow]
case succ.h
p : ℕ
R : Type ?u.932563
idx : Type u_1
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
case succ
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
apply dvd_sub_pow_of_dvd_sub
no goals
case succ.h
p : ℕ
R : Type ?u.932563
idx : Type u_1
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
rw [← C_eq_coe_nat, C_dvd_iff_zmod, RingHom.map_sub, sub_eq_zero, map_expand, RingHom.map_pow,
  MvPolynomial.expand_zmod]
no goals
case zero
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
simp only [isUnit_one, Int.ofNat_zero, Int.ofNat_succ, zero_add, pow_zero, C_1, IsUnit.dvd,
  Nat.cast_one, Nat.zero_eq]
p : ℕ
R : Type ?u.932563
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ (k + (n - k) + 1)
p : ℕ
R : Type ?u.932563
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
rw [← pow_add, ← add_assoc]
case e_a.e_a
p : ℕ
R : Type ?u.932563
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ n = k + (n - k)
p : ℕ
R : Type ?u.932563
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ (k + (n - k) + 1)
congr 2
no goals
case e_a.e_a
p : ℕ
R : Type ?u.932563
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ n = k + (n - k)
rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk]
no goals
p : ℕ
R : Type ?u.932563
idx : Type u_1
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)
rw [← pow_succ, ← tsub_add_eq_add_tsub hk]