awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ norm.{wG} (E := G)
      ((f : (a : (i : ι) → E₁ i) → G) fun (j : ι) ↦
          if h : j ∈ s then m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) j ⋯)) j
          else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) j ⋯) :
        G) ≤
    (‖f‖ * ∏ i : { a : ι // a ∉ s }, ‖x i‖) * ∏ i : α, ‖m i‖
have apply : ‖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 sorry)) i
        else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i sorry)) ≤
  (‖f‖ * ∏ i : { a : ι // a ∉ s }, ‖x i‖) * ∏ i : α, ‖m i‖
Tactic: apply (f.le_opNorm _).trans _
-- 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
⊢ ‖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 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 sorry)) i
          else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i sorry)))
      (∏ 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))) ≤
  ‖f‖ * HMul.hMul (α := ℝ) (∏ i : { a : ι // a ∉ s }, ‖x i‖) (∏ i : α, ‖m i‖)
Tactic: rw [← prod_compl_mul_prod s.toFinset, mul_assoc]
-- 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
⊢ ‖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‖)
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 : { a : ι // a ∉ s }, ‖x i‖)
Tactic: gcongr
-- 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
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‖ *
      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‖)
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: gcongr
-- 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
⊢ 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‖)
have hbc : Eq (α := ℝ)
  (∏ 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 : { a : ι // a ∉ s }, ‖x i‖)
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (hypothesis)
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
⊢ Eq (α := ℝ)
    (∏ 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‖)
have this : ∀ (x : ι), x ∈ s.toFinsetᶜ ↔ (fun (x : ι) ↦ x ∉ s) x
Tactic: have : ∀ x, x ∈ s.toFinsetᶜ ↔ (fun x ↦ x ∉ s) x := by simp
-- 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
this : ∀ (x : ι), x ∈ s.toFinsetᶜ ↔ (fun (x : ι) ↦ x ∉ s) x
⊢ Eq (α := ℝ)
    (∏ 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‖)
have hbc : Eq (α := ℝ)
  (∏ a : { x : ι // x ∉ s },
    norm.{wE₁} (E := E₁ (↑a : ι))
      (if h : (↑a : ι) ∈ s then
        m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) (↑a : ι) sorry)) (↑a : ι)
      else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) (↑a : ι) sorry)))
  (∏ i : { a : ι // a ∉ s }, ‖x i‖)
Tactic: rw [prod_subtype _ this]
-- 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
this : ∀ (x : ι), x ∈ s.toFinsetᶜ ↔ (fun (x : ι) ↦ x ∉ s) x
hbc :
  Eq (α := ℝ)
    (∏ a : { x : ι // x ∉ s },
      norm.{wE₁} (E := E₁ (↑a : ι))
        (if h : (↑a : ι) ∈ s then
          m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) (↑a : ι) ⋯)) (↑a : ι)
        else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) (↑a : ι) ⋯)))
    (∏ i : { a : ι // a ∉ s }, ‖x i‖)
⊢ Eq (α := ℝ)
    (∏ 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‖)
have rw : Fintype { x : ι // x ∉ s }
Tactic: rw [prod_subtype _ this]
-- 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
⊢ 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 : α, ‖m i‖)
have hbc : LE.le (α := ℝ)
  (∏ a : Subtype (Membership.mem s),
    norm.{wE₁} (E := E₁ (↑a : ι))
      (if h : (↑a : ι) ∈ s then
        m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) (↑a : ι) sorry)) (↑a : ι)
      else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) (↑a : ι) sorry)))
  (∏ i : (↑s : Type v), ‖m ((e.symm : (a : (↑s : Type v)) → α) i)‖)
Tactic: rw [prod_subtype _ (fun _ ↦ s.mem_toFinset), ← Equiv.prod_comp e.symm]
-- 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
hbc :
  LE.le (α := ℝ)
    (∏ a : Subtype (Membership.mem s),
      norm.{wE₁} (E := E₁ (↑a : ι))
        (if h : (↑a : ι) ∈ s then
          m ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (a : ι) ↦ a ∈ s) (↑a : ι) ⋯)) (↑a : ι)
        else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) (↑a : ι) ⋯)))
    (∏ i : (↑s : Type v), ‖m ((e.symm : (a : (↑s : Type v)) → α) i)‖)
⊢ 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 : α, ‖m i‖)
have rw : Fintype (Subtype (Membership.mem s))
Tactic: rw [prod_subtype _ (fun _ ↦ s.mem_toFinset), ← Equiv.prod_comp e.symm]
-- 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
⊢ ‖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 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 sorry)) i
          else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i sorry)))
      (∏ 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))) ≤
  (‖f‖ * ∏ i : { a : ι // a ∉ s }, ‖x i‖) * ∏ 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
-- 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‖
⊢ ‖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 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 sorry)) i
          else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i sorry)))
      (∏ 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))) ≤
  ‖f‖ * HMul.hMul (α := ℝ) (∏ i : { a : ι // a ∉ s }, ‖x i‖) (∏ 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
-- 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‖)
⊢ ‖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 : { a : ι // a ∉ s }, ‖x 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