Theorem: sq_square (UnitConjecture/TorsionFree.lean)

State before:
p q r : ℤ
x : Q
⊢ ((p, q, r), Q.c) * ((p, q, r), Q.c) = (P.sq ((p, q, r), Q.c), Q.e)
Tactic:
aesop (rule_sets [P]) (options := { warnOnNonterminal := false })
State after:
p q r : ℤ
fst snd : Fin 2
⊢ ((p, q, r), Q.c) * ((p, q, r), Q.c) = ((0, 0, r + r + 1), Q.e)

State before:
p q r : ℤ
fst snd : Fin 2
⊢ ((p, q, r), Q.c) * ((p, q, r), Q.c) = ((0, 0, r + r + 1), Q.e)
Tactic:
rw [P.mul]
State after:
p q r : ℤ
fst snd : Fin 2
⊢ ((p, q, r) + ↑(action Q.c) (p, q, r) + cocycle Q.c Q.c, Q.c + Q.c) = ((0, 0, r + r + 1), Q.e)

State before:
p q r : ℤ
fst snd : Fin 2
⊢ ((p, q, r) + ↑(action Q.c) (p, q, r) + cocycle Q.c Q.c, Q.c + Q.c) = ((0, 0, r + r + 1), Q.e)
Tactic:
aesop (rule_sets [P])
State after:
no goals