no goals
ι : Type ?u.197400
R : Type u_2
R' : Type ?u.197406
E : Type u_1
F : Type ?u.197412
G : Type ?u.197415
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : NonarchAddGroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
  mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg