-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
α : Type u_1
inst_11 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_12 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : { a : ι // a ∉ s }) → E₁ (↑i : ι)
m : (i : α) → (i : ι) → E₁ i
rw :
  ‖f‖ *
      HMul.hMul (α := ℝ)
        (∏ i ∈ s.toFinsetᶜ,
          norm.{wE₁} (E := E₁ i)
            (if h : i ∈ s then m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) i ⋯)) i
            else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i ⋯)))
        (∏ i ∈ s.toFinset,
          norm.{wE₁} (E := E₁ i)
            (if h : i ∈ s then m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) i ⋯)) i
            else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i ⋯))) ≤
    (‖f‖ * ∏ i : { a : ι // a ∉ s }, ‖x i‖) * ∏ i : α, ‖m i‖
rw₁ rw₂ rw₃ :
  ‖f‖ *
      HMul.hMul (α := ℝ)
        (∏ i ∈ s.toFinsetᶜ,
          norm.{wE₁} (E := E₁ i)
            (if h : i ∈ s then m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) i ⋯)) i
            else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i ⋯)))
        (∏ i ∈ s.toFinset,
          norm.{wE₁} (E := E₁ i)
            (if h : i ∈ s then m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) i ⋯)) i
            else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i ⋯))) ≤
    ‖f‖ * HMul.hMul (α := ℝ) (∏ i : { a : ι // a ∉ s }, ‖x i‖) (∏ i : α, ‖m i‖)
hbc :
  LE.le (α := ℝ)
    (∏ i ∈ s.toFinsetᶜ,
      norm.{wE₁} (E := E₁ i)
        (if h : i ∈ s then m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) i ⋯)) i
        else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i ⋯)))
    (∏ i : { a : ι // a ∉ s }, ‖x i‖)
⊢ ‖f‖ *
      ∏ i : ι,
        norm.{wE₁} (E := E₁ i)
          (if h : i ∈ s then m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) i ⋯)) i
          else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i ⋯)) ≤
    (‖f‖ * ∏ i : { a : ι // a ∉ s }, ‖x i‖) * ∏ i : α, ‖m i‖
have hbc₁ : LE.le (α := ℝ)
  (∏ i ∈ s.toFinset,
    norm.{wE₁} (E := E₁ i)
      (if h : i ∈ s then m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) i sorry)) i
      else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i sorry)))
  (∏ i : α, ‖m i‖)
Tactic: classical
    rw [← prod_compl_mul_prod s.toFinset, mul_assoc]
    gcongr
    · apply le_of_eq
      have : ∀ x, x ∈ s.toFinsetᶜ ↔ (fun x ↦ x ∉ s) x := by simp
      rw [prod_subtype _ this]
      congr with i
      simp [i.2]
    · rw [prod_subtype _ (fun _ ↦ s.mem_toFinset), ← Equiv.prod_comp e.symm]
      gcongr with i
      simpa only [i.2, ↓reduceDIte, Subtype.coe_eta] using norm_le_pi_norm (m (e.symm i)) ↑i