∀ {𝕜 : Type u_4} {ι : Type u_2} {E : ι → Type u_3} {G : Type u_1} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  {f : ContinuousMultilinearMap 𝕜 E G} (x : ℝ)
  (motive : x ∈ {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i, ‖m i‖} → Prop)
  (x_1 : x ∈ {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i, ‖m i‖}),
  (∀ (hn : 0 ≤ x) (right : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ x * ∏ i, ‖m i‖), motive ⋯) → motive x_1