Theorem: square_free (UnitConjecture/TorsionFree.lean)

State before:
p q r : ℤ
x : Q
⊢ ((p, q, r), x) * ((p, q, r), x) = 1 → ((p, q, r), x) = 1
Tactic:
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])
State after:
no goals

State before:
p q r : ℤ
x : Q
⊢ ((p, q, r), Q.e) * ((p, q, r), Q.e) = 1 → ((p, q, r), Q.e) = 1
Tactic:
intro h
State after:
p q r : ℤ
x : Q
h : ((p, q, r), Q.e) * ((p, q, r), Q.e) = 1
⊢ ((p, q, r), Q.e) = 1

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

State before:
p q r : ℤ
h : ((p + p, q + q, r + r), Q.e) = ((0, 0, 0), Q.e)
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
State after:
p q r : ℤ
h : (p + p, q + q, r + r) = (0, 0, 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)

State before:
p q r : ℤ
h : (p + p, q + q, r + r) = (0, 0, 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
State after:
p q r : ℤ
h : (p + p = 0 ∧ (q + q, r + r) = (0, 0)) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)

State before:
p q r : ℤ
h : (p + p = 0 ∧ (q + q, r + r) = (0, 0)) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
State after:
p q r : ℤ
h : (p + p = 0 ∧ q + q = 0 ∧ r + r = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)

State before:
p q r : ℤ
h : (p + p = 0 ∧ q + q = 0 ∧ r + r = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Tactic:
aesop (rule_sets [P]) (add norm [Int.zero_of_twice_zero])
State after:
no goals

State before:
p q r : ℤ
x : Q
⊢ ((p, q, r), Q.c) * ((p, q, r), Q.c) = 1 → ((p, q, r), Q.c) = 1
Tactic:
intro h
State after:
p q r : ℤ
x : Q
h : ((p, q, r), Q.c) * ((p, q, r), Q.c) = 1
⊢ ((p, q, r), Q.c) = 1

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

State before:
p q r : ℤ
h : ((0, 0, r + r + 1), Q.e) = ((0, 0, 0), Q.e)
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
all_goals (rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h)
State after:
p q r : ℤ
h : (0 = 0 ∧ 0 = 0 ∧ r + r + 1 = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)

State before:
p q r : ℤ
h : (0 = 0 ∧ 0 = 0 ∧ r + r + 1 = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
aesop (rule_sets [P]) (add norm [Int.odd_ne_zero])
State after:
no goals

State before:
p q r : ℤ
h : ((0, 0, r + r + 1), Q.e) = ((0, 0, 0), Q.e)
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
(rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h)
State after:
p q r : ℤ
h : (0 = 0 ∧ 0 = 0 ∧ r + r + 1 = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)

State before:
p q r : ℤ
h : ((0, 0, r + r + 1), Q.e) = ((0, 0, 0), Q.e)
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
State after:
p q r : ℤ
h : (0, 0, r + r + 1) = (0, 0, 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)

State before:
p q r : ℤ
h : (0, 0, r + r + 1) = (0, 0, 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
State after:
p q r : ℤ
h : (0 = 0 ∧ (0, r + r + 1) = (0, 0)) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)

State before:
p q r : ℤ
h : (0 = 0 ∧ (0, r + r + 1) = (0, 0)) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
State after:
p q r : ℤ
h : (0 = 0 ∧ 0 = 0 ∧ r + r + 1 = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)