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

State before:
d a b i₁ i₂ : ℕ
hd : ↑d ≠ 0
rel : ↑a * (3 * ↑i₂ - ↑d) = ↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂)
⊢ ↑a = ↑b
Tactic:
reduce_mod_3 rel
State after:
d a b i₁ i₂ : ℕ
hd : ↑d ≠ 0
H₁✝ : 3 = 0
H₂✝ : 2 = -1
rel : ↑a = ↑b ∨ ↑d = 0
⊢ ↑a = ↑b

State before:
d a b i₁ i₂ : ℕ
hd : ↑d ≠ 0
H₁✝ : 3 = 0
H₂✝ : 2 = -1
rel : ↑a = ↑b ∨ ↑d = 0
⊢ ↑a = ↑b
Tactic:
exact rel.resolve_right hd
State after:
no goals