case h
R : Type u_1
R' : Type ?u.658025
𝕜 : Type u_2
𝕜₂ : Type ?u.658031
𝕜₃ : Type ?u.658034
𝕝 : Type ?u.658037
E : Type u_3
E₂ : Type ?u.658043
E₃ : Type ?u.658046
F : Type ?u.658049
G : Type ?u.658052
ι : Type ?u.658055
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x : E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ ↑(r • (p ⊓ q)) x✝ = ↑(r • p ⊓ r • q) x✝
R : Type u_1
R' : Type ?u.658025
𝕜 : Type u_2
𝕜₂ : Type ?u.658031
𝕜₃ : Type ?u.658034
𝕝 : Type ?u.658037
E : Type u_3
E₂ : Type ?u.658043
E₃ : Type ?u.658046
F : Type ?u.658049
G : Type ?u.658052
ι : Type ?u.658055
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x : E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
⊢ r • (p ⊓ q) = r • p ⊓ r • q
ext
no goals
case h
R : Type u_1
R' : Type ?u.658025
𝕜 : Type u_2
𝕜₂ : Type ?u.658031
𝕜₃ : Type ?u.658034
𝕝 : Type ?u.658037
E : Type u_3
E₂ : Type ?u.658043
E₃ : Type ?u.658046
F : Type ?u.658049
G : Type ?u.658052
ι : Type ?u.658055
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x : E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ ↑(r • (p ⊓ q)) x✝ = ↑(r • p ⊓ r • q) x✝
simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
  smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]