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

State before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
⊢ ↑a = ↑d ∨ ↑a = -↑d
Tactic:
have hdd := not_eq_neg_self hd
State after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
⊢ ↑a = ↑d ∨ ↑a = -↑d

State before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
⊢ ↑a = ↑d ∨ ↑a = -↑d
Tactic:
by_contra! H
State after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
⊢ False

State before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
⊢ False
Tactic:
have help : ∀ {a d : ZMod 3}, -d ≠ d → (a ≠ d ∧ a ≠ -d) → a = 0 := by decide
State after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
⊢ False

State before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
⊢ False
Tactic:
have ha₀ := (ZMod.nat_cast_zmod_eq_zero_iff_dvd a 3).mp <| help hdd H
State after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
ha₀ : 3 ∣ a
⊢ False

State before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
ha₀ : 3 ∣ a
⊢ False
Tactic:
have hb₀ := (ZMod.nat_cast_zmod_eq_zero_iff_dvd b 3).mp <| (help hdd H ▸ hab).symm
State after:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
ha₀ : 3 ∣ a
hb₀ : 3 ∣ b
⊢ False

State before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
help : ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
ha₀ : 3 ∣ a
hb₀ : 3 ∣ b
⊢ False
Tactic:
exact Nat.Prime.not_coprime_iff_dvd.mpr ⟨3, Nat.prime_three, ha₀, hb₀⟩ hcop
State after:
no goals

State before:
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
hab : ↑a = ↑b
hdd : -↑d ≠ ↑d
H : ↑a ≠ ↑d ∧ ↑a ≠ -↑d
⊢ ∀ {a d : ZMod 3}, -d ≠ d → a ≠ d ∧ a ≠ -d → a = 0
Tactic:
decide
State after:
no goals