simp only [Equiv.symm_symm, Equiv.symm_apply_apply, Equiv.piCongrLeft'_apply]
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
⊢ (∀ (y : (a : ι) → D a),
      ‖f ((Equiv.piCongrLeft' D σ).symm ((Equiv.piCongrLeft' D σ).symm.symm y))‖ ≤
        c * ∏ i : ι', ‖(Equiv.piCongrLeft' D σ).symm.symm y i‖) ↔
    ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
⊢ (∀ (y : (a : ι) → D a), ‖f y‖ ≤ c * ∏ x : ι', ‖y (σ.symm x)‖) ↔ ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖