-- Mathlib/RingTheory/WittVector/Compare.lean
theorem eq_of_le_of_cast_pow_eq_zero [CharP R p] (i : ℕ) (hin : i ≤ n)
    (hpi : (p : TruncatedWittVector p n R) ^ i = 0) : i = n

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : Nontrivial R
⊢ ¬1 = 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ↑p ^ i ≠ 0

Tactic:
have : (p : TruncatedWittVector p n R) ^ i = WittVector.truncate n ((p : 𝕎 R) ^ i) := by
  rw [RingHom.map_pow, map_natCast]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = (WittVector.truncate n) (↑p ^ i)
⊢ ↑p ^ i ≠ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hpi : i ≠ n
hin : i < n
⊢ ↑p ^ i ≠ 0

Tactic:
clear hpi

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ↑p ^ i ≠ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i ≤ n
hpi : ↑p ^ i = 0
⊢ i = n

Tactic:
contrapose! hpi

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i ≤ n
hpi : i ≠ n
⊢ ↑p ^ i ≠ 0

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬1 = 0

Tactic:
haveI : Nontrivial R := CharP.nontrivial_of_char_ne_one hp.1.ne_one

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : Nontrivial R
⊢ ¬1 = 0

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬coeff ⟨i, hin⟩ ((WittVector.truncate n) (↑p ^ i)) = coeff ⟨i, hin⟩ 0

Tactic:
rw [WittVector.coeff_truncate, coeff_zero, Fin.val_mk, WittVector.coeff_p_pow]

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬1 = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i ≤ n
hpi : i ≠ n
⊢ ↑p ^ i ≠ 0

Tactic:
replace hin := lt_of_le_of_ne hin hpi

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hpi : i ≠ n
hin : i < n
⊢ ↑p ^ i ≠ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ∃ x, ¬coeff x ((WittVector.truncate n) (↑p ^ i)) = coeff x 0

Tactic:
use ⟨i, hin⟩

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬coeff ⟨i, hin⟩ ((WittVector.truncate n) (↑p ^ i)) = coeff ⟨i, hin⟩ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ↑p ^ i = (WittVector.truncate n) (↑p ^ i)

Tactic:
rw [RingHom.map_pow, map_natCast]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = (WittVector.truncate n) (↑p ^ i)
⊢ ∃ x, ¬coeff x ((WittVector.truncate n) (↑p ^ i)) = coeff x 0

Tactic:
clear this

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ∃ x, ¬coeff x ((WittVector.truncate n) (↑p ^ i)) = coeff x 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = (WittVector.truncate n) (↑p ^ i)
⊢ ↑p ^ i ≠ 0

Tactic:
rw [this, ne_eq, TruncatedWittVector.ext_iff, not_forall]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = (WittVector.truncate n) (↑p ^ i)
⊢ ∃ x, ¬coeff x ((WittVector.truncate n) (↑p ^ i)) = coeff x 0