p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ coeff (teichmullerFun p r) 0 ^ p ^ n = r ^ p ^ n

case h₀
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ∀ (b : ℕ), b ∈ Finset.range (n + 1) → b ≠ 0 → ↑p ^ b * coeff (teichmullerFun p r) b ^ p ^ (n - b) = 0

case h₁
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ¬0 ∈ Finset.range (n + 1) → ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ↑(ghostComponent n) (teichmullerFun p r) = r ^ p ^ n
rw [ghostComponent_apply, aeval_wittPolynomial, Finset.sum_eq_single 0, pow_zero, one_mul,
  tsub_zero]
no goals
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ coeff (teichmullerFun p r) 0 ^ p ^ n = r ^ p ^ n
rfl
case h₀
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ ↑p ^ i * coeff (teichmullerFun p r) i ^ p ^ (n - i) = 0
case h₀
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ∀ (b : ℕ), b ∈ Finset.range (n + 1) → b ≠ 0 → ↑p ^ b * coeff (teichmullerFun p r) b ^ p ^ (n - b) = 0
intro i hi h0
case h.e'_2.h.e'_6
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ coeff (teichmullerFun p r) i ^ p ^ (n - i) = 0
case h₀
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ ↑p ^ i * coeff (teichmullerFun p r) i ^ p ^ (n - i) = 0
convert mul_zero (M₀ := R) _
case h.e'_2.h.e'_5
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ coeff (teichmullerFun p r) i = 0

case h.e'_2.h.e'_6.convert_2
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ 0 < p ^ (n - i)
case h.e'_2.h.e'_6
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ coeff (teichmullerFun p r) i ^ p ^ (n - i) = 0
convert zero_pow (M := R) _
case h.e'_2.h.e'_5.zero
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
hi : Nat.zero ∈ Finset.range (n + 1)
h0 : Nat.zero ≠ 0
⊢ coeff (teichmullerFun p r) Nat.zero = 0

case h.e'_2.h.e'_5.succ
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n n✝ : ℕ
hi : Nat.succ n✝ ∈ Finset.range (n + 1)
h0 : Nat.succ n✝ ≠ 0
⊢ coeff (teichmullerFun p r) (Nat.succ n✝) = 0
case h.e'_2.h.e'_5
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ coeff (teichmullerFun p r) i = 0
cases i
no goals
case h.e'_2.h.e'_5.zero
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
hi : Nat.zero ∈ Finset.range (n + 1)
h0 : Nat.zero ≠ 0
⊢ coeff (teichmullerFun p r) Nat.zero = 0
contradiction
no goals
case h.e'_2.h.e'_5.succ
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n n✝ : ℕ
hi : Nat.succ n✝ ∈ Finset.range (n + 1)
h0 : Nat.succ n✝ ≠ 0
⊢ coeff (teichmullerFun p r) (Nat.succ n✝) = 0
rfl
no goals
case h.e'_2.h.e'_6.convert_2
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ 0 < p ^ (n - i)
exact pow_pos hp.1.pos _
case h₁
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ¬0 < n + 1 → ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
case h₁
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ¬0 ∈ Finset.range (n + 1) → ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
rw [Finset.mem_range]
case h₁
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
h : ¬0 < n + 1
⊢ ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
case h₁
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ¬0 < n + 1 → ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
intro h
no goals
case h₁
p : ℕ
R : Type u_1
S : Type ?u.10109
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
h : ¬0 < n + 1
⊢ ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
exact (h (Nat.succ_pos n)).elim