no goals
R : Type u_1
R' : Type ?u.213053
𝕜 : Type u_2
𝕜₂ : Type ?u.213059
𝕜₃ : Type ?u.213062
𝕝 : Type ?u.213065
E : Type u_3
E₂ : Type ?u.213071
E₃ : Type ?u.213074
F : Type ?u.213077
G : Type ?u.213080
ι : Type ?u.213083
inst✝⁵ : SeminormedRing 𝕜
inst✝⁴ : AddGroup E
inst✝³ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
c : 𝕜
x✝ y✝ : E
r✝ : ℝ
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 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