match x with
| .e =>
  intro h 
  aesop (rule_sets [P]) (add norm [Int.zero_of_twice_zero]) (options := { warnOnNonterminal := false })
  rw [Prod.mk.injEq] at h
  rw [Prod.mk.injEq] at h
  rw [Prod.mk.injEq] at h
  aesop (rule_sets [P]) (add norm [Int.zero_of_twice_zero])
| .a | .b | .c => 
  intro h
  aesop (rule_sets [P]) (add norm [Int.odd_ne_zero]) (options := { warnOnNonterminal := false })
  all_goals (rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h)
  aesop (rule_sets [P]) (add norm [Int.odd_ne_zero])
p q r : ℤ
x : Q
⊢ ((p, q, r), x) * ((p, q, r), x) = 1 → ((p, q, r), x) = 1
no goals