Theorem: sq_add_sq_eq_zero (MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean)

State before:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x ^ 2 + y ^ 2 = 0 → x = 0 ∧ y = 0

case mpr
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x = 0 ∧ y = 0 → x ^ 2 + y ^ 2 = 0

State before:
case mpr
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x = 0 ∧ y = 0 → x ^ 2 + y ^ 2 = 0
Tactic:
rintro ⟨rfl, rfl⟩
State after:
case mpr.intro
α : Type u_1
inst✝ : LinearOrderedRing α
⊢ 0 ^ 2 + 0 ^ 2 = 0

State before:
case mpr.intro
α : Type u_1
inst✝ : LinearOrderedRing α
⊢ 0 ^ 2 + 0 ^ 2 = 0
Tactic:
norm_num
State after:
no goals

State before:
case mp
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x ^ 2 + y ^ 2 = 0 → x = 0 ∧ y = 0
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x = 0 ∧ y = 0

State before:
case mp
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x = 0 ∧ y = 0
Tactic:
constructor
State after:
case mp.left
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x = 0

case mp.right
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ y = 0

State before:
case mp.right
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ y = 0
Tactic:
rw [add_comm] at h
State after:
case mp.right
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : y ^ 2 + x ^ 2 = 0
⊢ y = 0

State before:
case mp.right
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : y ^ 2 + x ^ 2 = 0
⊢ y = 0
Tactic:
exact aux h
State after:
no goals

State before:
case mp.left
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x = 0
Tactic:
exact aux h
State after:
no goals