-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem sqLe_mul {d x y z w : ℕ} :
    (SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1) ∧
      (SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
        (SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
          (SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1)

Proof state:
case refine_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
have :=
  Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy))
    (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))

Result:
case refine_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1

Proof state:
case refine_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ 0 ≤ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z))

Tactic:
convert this using 1

Result:
case h.e'_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z)) =
    (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))

Proof state:
case h.e'_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z)) =
    (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))

Tactic:
simp only [one_mul, Int.ofNat_add, Int.ofNat_mul]

Result:
case h.e'_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) - ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) =
    (↑x * ↑x - ↑d * ↑y * ↑y) * (↑z * ↑z - ↑d * ↑w * ↑w)

Proof state:
case h.e'_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) - ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) =
    (↑x * ↑x - ↑d * ↑y * ↑y) * (↑z * ↑z - ↑d * ↑w * ↑w)

Tactic:
ring

Result:
no goals

Proof state:
case refine_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)

Result:
case refine_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ 0 ≤ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z))

Proof state:
case refine_4
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
intro xy zw

Result:
case refine_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1