case a
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑(bind₁ onePoly) (wittPolynomial p ℤ n)) = MvPolynomial.coeff m✝ 1
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑(bind₁ onePoly) (wittPolynomial p ℤ n) = 1
ext
case a
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑(bind₁ onePoly) (↑C (↑p ^ 0) * X 0 ^ p ^ (n - 0))) = MvPolynomial.coeff m✝ 1

case a.h₀
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ ∀ (b : ℕ), b ∈ Finset.range (n + 1) → b ≠ 0 → ↑(bind₁ onePoly) (↑C (↑p ^ b) * X b ^ p ^ (n - b)) = 0

case a.h₁
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ ¬0 ∈ Finset.range (n + 1) → ↑(bind₁ onePoly) (↑C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0
case a
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑(bind₁ onePoly) (wittPolynomial p ℤ n)) = MvPolynomial.coeff m✝ 1
rw [wittPolynomial_eq_sum_c_mul_x_pow, AlgHom.map_sum, Finset.sum_eq_single 0]
no goals
case a
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑(bind₁ onePoly) (↑C (↑p ^ 0) * X 0 ^ p ^ (n - 0))) = MvPolynomial.coeff m✝ 1
simp only [onePoly, one_pow, one_mul, AlgHom.map_pow, C_1, pow_zero, bind₁_X_right, if_true,
  eq_self_iff_true]
case a.h₀
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
i : ℕ
_hi : i ∈ Finset.range (n + 1)
hi0 : i ≠ 0
⊢ ↑(bind₁ onePoly) (↑C (↑p ^ i) * X i ^ p ^ (n - i)) = 0
case a.h₀
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ ∀ (b : ℕ), b ∈ Finset.range (n + 1) → b ≠ 0 → ↑(bind₁ onePoly) (↑C (↑p ^ b) * X b ^ p ^ (n - b)) = 0
intro i _hi hi0
no goals
case a.h₀
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
i : ℕ
_hi : i ∈ Finset.range (n + 1)
hi0 : i ≠ 0
⊢ ↑(bind₁ onePoly) (↑C (↑p ^ i) * X i ^ p ^ (n - i)) = 0
simp only [onePoly, if_neg hi0, zero_pow (pow_pos hp.1.pos _), MulZeroClass.mul_zero,
  AlgHom.map_pow, bind₁_X_right, AlgHom.map_mul]
case a.h₁
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ ¬0 < n + 1 → ↑(bind₁ onePoly) (↑C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0
case a.h₁
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ ¬0 ∈ Finset.range (n + 1) → ↑(bind₁ onePoly) (↑C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0
rw [Finset.mem_range]
no goals
case a.h₁
p : ℕ
R S : Type u
σ : Type ?u.671892
idx : Type ?u.671895
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
m✝ : ℕ →₀ ℕ
⊢ ¬0 < n + 1 → ↑(bind₁ onePoly) (↑C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0
simp only [add_pos_iff, or_true, not_true, pow_zero, map_one, ge_iff_le, nonpos_iff_eq_zero,
  tsub_zero, one_mul, gt_iff_lt, IsEmpty.forall_iff]