-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem nonneg_antisymm : ∀ {a : ℤ√d}, Nonneg a → Nonneg (-a) → a = 0
  | ⟨0, 0⟩, _, _ => rfl
  | ⟨-[_+1], -[_+1]⟩, xy, _ => False.elim xy
  | ⟨(_ + 1 : Nat), (_ + 1 : Nat)⟩, _, yx => False.elim yx
  | ⟨-[_+1], 0⟩, xy, _ => absurd xy (not_sqLe_succ _ _ _ (by decide))
  | ⟨(_ + 1 : Nat), 0⟩, _, yx => absurd yx (not_sqLe_succ _ _ _ (by decide))
  | ⟨0, -[_+1]⟩, xy, _ => absurd xy (not_sqLe_succ _ _ _ d_pos)
  | ⟨0, (_ + 1 : Nat)⟩, _, yx => absurd yx (not_sqLe_succ _ _ _ d_pos)
  | ⟨(x + 1 : Nat), -[y+1]⟩, (xy : SqLe _ _ _ _), (yx : SqLe _ _ _ _) => by
    let t := le_antisymm yx xy
    rw [one_mul] at t
    exact absurd t (not_divides_sq _ _)
  | ⟨-[x+1], (y + 1 : Nat)⟩, (xy : SqLe _ _ _ _), (yx : SqLe _ _ _ _) => by
    let t := le_antisymm xy yx
    rw [one_mul] at t
    exact absurd t (not_divides_sq _ _)

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
t : (x + 1) * (x + 1) = d * y.succ * y.succ
⊢ { re := ↑(x + 1), im := -[y+1] } = 0

Tactic:
exact absurd t (not_divides_sq _ _)

Result:
no goals

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
t : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ { re := -[x+1], im := ↑(y + 1) } = 0

Tactic:
exact absurd t (not_divides_sq _ _)

Result:
no goals

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
⊢ { re := ↑(x + 1), im := -[y+1] } = 0

Tactic:
let t := le_antisymm yx xy

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
t : 1 * (x + 1) * (x + 1) = d * y.succ * y.succ := le_antisymm yx xy
⊢ { re := ↑(x + 1), im := -[y+1] } = 0

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
t : 1 * (x + 1) * (x + 1) = d * y.succ * y.succ := le_antisymm yx xy
⊢ { re := ↑(x + 1), im := -[y+1] } = 0

Tactic:
rw [one_mul] at t

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
t : (x + 1) * (x + 1) = d * y.succ * y.succ
⊢ { re := ↑(x + 1), im := -[y+1] } = 0

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
t : 1 * (x + 1) * (x + 1) = d * (y + 1) * (y + 1) := le_antisymm xy yx
⊢ { re := -[x+1], im := ↑(y + 1) } = 0

Tactic:
rw [one_mul] at t

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
t : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ { re := -[x+1], im := ↑(y + 1) } = 0

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
⊢ { re := -[x+1], im := ↑(y + 1) } = 0

Tactic:
let t := le_antisymm xy yx

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
t : 1 * (x + 1) * (x + 1) = d * (y + 1) * (y + 1) := le_antisymm xy yx
⊢ { re := -[x+1], im := ↑(y + 1) } = 0

Proof state:
d : ℕ
dnsq : Nonsquare d
n✝ : ℕ
x✝ : { re := ↑(n✝ + 1), im := 0 }.Nonneg
yx : (-{ re := ↑(n✝ + 1), im := 0 }).Nonneg
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
d : ℕ
dnsq : Nonsquare d
a✝ : ℕ
xy : { re := -[a✝+1], im := 0 }.Nonneg
x✝ : (-{ re := -[a✝+1], im := 0 }).Nonneg
⊢ 0 < 1

Tactic:
decide

Result:
no goals