Theorem: Weight.not_eq_neg_self (Weights/Dimension2.lean)

State before:
d : ℕ
hd : ↑d ≠ 0
⊢ -↑d ≠ ↑d
Tactic:
have hch : ringChar (ZMod 3) ≠ 2 := by rw [ZMod.ringChar_zmod_n]; norm_num
State after:
d : ℕ
hd : ↑d ≠ 0
hch : ringChar (ZMod 3) ≠ 2
⊢ -↑d ≠ ↑d

State before:
d : ℕ
hd : ↑d ≠ 0
hch : ringChar (ZMod 3) ≠ 2
⊢ -↑d ≠ ↑d
Tactic:
exact mt (Ring.eq_self_iff_eq_zero_of_char_ne_two hch).mp hd
State after:
no goals

State before:
d : ℕ
hd : ↑d ≠ 0
⊢ ringChar (ZMod 3) ≠ 2
Tactic:
rw [ZMod.ringChar_zmod_n]
State after:
d : ℕ
hd : ↑d ≠ 0
⊢ 3 ≠ 2

State before:
d : ℕ
hd : ↑d ≠ 0
⊢ 3 ≠ 2
Tactic:
norm_num
State after:
no goals