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

State before:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 = 0
Tactic:
apply le_antisymm _ (sq_nonneg x)
State after:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 ≤ 0

State before:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 ≤ 0
Tactic:
rw [← h]
State after:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 ≤ x ^ 2 + y ^ 2

State before:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
h : x ^ 2 + y ^ 2 = 0
⊢ x ^ 2 ≤ x ^ 2 + y ^ 2
Tactic:
apply le_add_of_nonneg_right (sq_nonneg y)
State after:
no goals