d : ℕ
a : ℤ√↑d
n : ℕ
ha : Nonneg a
⊢ Nonneg (↑↑n * a)
d : ℕ
a : ℤ√↑d
n : ℕ
ha : Nonneg a
⊢ Nonneg (↑n * a)
rw [← Int.cast_ofNat n]
no goals
d : ℕ
a : ℤ√↑d
n : ℕ
ha : Nonneg a
⊢ Nonneg (↑↑n * a)
exact
  match a, nonneg_cases ha, ha with
  | _, ⟨x, y, Or.inl rfl⟩, _ => by rw [smul_val]; trivial
  | _, ⟨x, y, Or.inr <| Or.inl rfl⟩, ha => by
    rw [smul_val]; simpa using nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)
  | _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ha => by
    rw [smul_val]; simpa using nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)
d : ℕ
a : ℤ√↑d
n : ℕ
ha : Nonneg a
x y : ℕ
x✝ : Nonneg { re := ↑x, im := ↑y }
⊢ Nonneg { re := ↑n * ↑x, im := ↑n * ↑y }
d : ℕ
a : ℤ√↑d
n : ℕ
ha : Nonneg a
x y : ℕ
x✝ : Nonneg { re := ↑x, im := ↑y }
⊢ Nonneg (↑↑n * { re := ↑x, im := ↑y })
rw [smul_val]
no goals
d : ℕ
a : ℤ√↑d
n : ℕ
ha : Nonneg a
x y : ℕ
x✝ : Nonneg { re := ↑x, im := ↑y }
⊢ Nonneg { re := ↑n * ↑x, im := ↑n * ↑y }
trivial
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ Nonneg { re := ↑n * ↑x, im := ↑n * -↑y }
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ Nonneg (↑↑n * { re := ↑x, im := -↑y })
rw [smul_val]
no goals
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := ↑x, im := -↑y }
⊢ Nonneg { re := ↑n * ↑x, im := ↑n * -↑y }
simpa using nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ Nonneg { re := ↑n * -↑x, im := ↑n * ↑y }
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ Nonneg (↑↑n * { re := -↑x, im := ↑y })
rw [smul_val]
no goals
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : Nonneg a
x y : ℕ
ha : Nonneg { re := -↑x, im := ↑y }
⊢ Nonneg { re := ↑n * -↑x, im := ↑n * ↑y }
simpa using nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)