case a
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(map (Int.castRingHom ℚ)) (wittOne p n) = ↑(map (Int.castRingHom ℚ)) 0
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ wittOne p n = 0
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
case a
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
case a
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(map (Int.castRingHom ℚ)) (wittOne p n) = ↑(map (Int.castRingHom ℚ)) 0
simp only [wittOne, wittStructureRat, RingHom.map_zero, AlgHom.map_one, RingHom.map_one,
  map_wittStructureInt]
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
case a
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
induction n using Nat.strong_induction_on with | h n IH => ?_
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑(bind₁ fun k => 1)
      ((X n - Finset.sum (Finset.range n) fun i => ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * ↑C (⅟↑p ^ n)) =
    0
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
rw [xInTermsOfW_eq]
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (1 - Finset.sum (Finset.range n) fun x => ↑C (↑p ^ x) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      ↑C (⅟↑p ^ n) =
    0
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑(bind₁ fun k => 1)
      ((X n - Finset.sum (Finset.range n) fun i => ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * ↑C (⅟↑p ^ n)) =
    0
simp only [AlgHom.map_mul, AlgHom.map_sub, AlgHom.map_sum, AlgHom.map_pow, bind₁_X_right,
  bind₁_C_right]
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (⅟↑p ^ n) -
      (Finset.sum (Finset.range n) fun x => ↑C (↑p ^ x) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        ↑C (⅟↑p ^ n) =
    0
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (1 - Finset.sum (Finset.range n) fun x => ↑C (↑p ^ x) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      ↑C (⅟↑p ^ n) =
    0
rw [sub_mul, one_mul]
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (⅟↑p ^ n) - ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) * ↑C (⅟↑p ^ n) = 0

case a.h.h₀
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ∀ (b : ℕ), b ∈ Finset.range n → b ≠ 0 → ↑C (↑p ^ b) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ b) ^ p ^ (n - b) = 0

case a.h.h₁
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ¬0 ∈ Finset.range n → ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (⅟↑p ^ n) -
      (Finset.sum (Finset.range n) fun x => ↑C (↑p ^ x) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        ↑C (⅟↑p ^ n) =
    0
rw [Finset.sum_eq_single 0]
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (↑p ^ n)⁻¹ - ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ n * ↑C (↑p ^ n)⁻¹ = 0
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (⅟↑p ^ n) - ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) * ↑C (⅟↑p ^ n) = 0
simp only [invOf_eq_inv, one_mul, inv_pow, tsub_zero, RingHom.map_one, pow_zero]
no goals
case a.h
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (↑p ^ n)⁻¹ - ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ n * ↑C (↑p ^ n)⁻¹ = 0
simp only [one_pow, one_mul, xInTermsOfW_zero, sub_self, bind₁_X_right]
case a.h.h₀
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i ∈ Finset.range n
hi0 : i ≠ 0
⊢ ↑C (↑p ^ i) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
case a.h.h₀
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ∀ (b : ℕ), b ∈ Finset.range n → b ≠ 0 → ↑C (↑p ^ b) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ b) ^ p ^ (n - b) = 0
intro i hin hi0
case a.h.h₀
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i < n
hi0 : i ≠ 0
⊢ ↑C (↑p ^ i) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
case a.h.h₀
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i ∈ Finset.range n
hi0 : i ≠ 0
⊢ ↑C (↑p ^ i) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
rw [Finset.mem_range] at hin
no goals
case a.h.h₀
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i < n
hi0 : i ≠ 0
⊢ ↑C (↑p ^ i) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
rw [IH _ hin (Nat.pos_of_ne_zero hi0), zero_pow (pow_pos hp.1.pos _), MulZeroClass.mul_zero]
case a.h.h₁
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ¬0 < n → ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
case a.h.h₁
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ¬0 ∈ Finset.range n → ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
rw [Finset.mem_range]
case a.h.h₁
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
a✝ : ¬0 < n
⊢ ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
case a.h.h₁
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ¬0 < n → ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
intro
no goals
case a.h.h₁
p : ℕ
R : Type ?u.47816
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
a✝ : ¬0 < n
⊢ ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
contradiction