awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
simp :
  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‖
⊢ norm.{wG} (E := G)
      ((((f.toMultilinearMap (M₁ := E₁).iteratedFDerivComponent (M₁ := E₁) (s := s) e :
                  (a : (i : { a : ι // a ∉ s }) → E₁ (↑i : ι)) → MultilinearMap 𝕜 (fun (x : α) ↦ (i : ι) → E₁ i) G)
                x :
              MultilinearMap 𝕜 (fun (x : α) ↦ (i : ι) → E₁ i) G) :
            (a : (i : α) → (i : ι) → E₁ i) → G)
          m :
        G) ≤
    (‖f‖ * ∏ i : { a : ι // a ∉ s }, ‖x i‖) * ∏ i : α, ‖m i‖

Tactic:
simp only [MultilinearMap.iteratedFDerivComponent, MultilinearMap.domDomRestrictₗ,
      MultilinearMap.coe_mk, MultilinearMap.domDomRestrict_apply, coe_coe]

Premises used: ContinuousMultilinearMap.coe_coe, MultilinearMap.iteratedFDerivComponent, MultilinearMap.coe_mk, MultilinearMap.domDomRestrict_apply, MultilinearMap.domDomRestrictₗ
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
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 ⋯)) i
          else x (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) i ⋯)) ≤
    (‖f‖ * ∏ i : { a : ι // a ∉ s }, ‖x i‖) * ∏ i : α, ‖m 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‖

Tactic:
apply (f.le_opNorm _).trans _

Premises used: ContinuousMultilinearMap.le_opNorm, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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‖ * 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‖

Tactic:
rw [← prod_compl_mul_prod s.toFinset, mul_assoc]

Premises used: mul_assoc, Set.toFinset, Finset.prod_compl_mul_prod
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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‖)
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 : α, ‖m 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‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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 :
  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‖)
⊢ 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‖)

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
⊢ ∀ (x : ι), x ∈ s.toFinsetᶜ ↔ (fun (x : ι) ↦ x ∉ s) x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
⊢ ∀ (x : ι), x ∈ s.toFinsetᶜ ↔ (fun (x : ι) ↦ x ∉ s) x

Tactic:
have : ∀ x, x ∈ s.toFinsetᶜ ↔ (fun x ↦ x ∉ s) x := by simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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‖)
rw : Fintype { x : ι // x ∉ s }
⊢ 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‖)

Tactic:
rw [prod_subtype _ this]

Premises used: Finset.prod_subtype
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
i : { x : ι // x ∉ s }
⊢ 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 : ι) ⋯)) =
    ‖x i‖

Tactic:
simp [i.2]

Premises used: Subtype.property
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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)‖)
rw : Fintype (Subtype (Membership.mem s))
⊢ 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‖)

Tactic:
rw [prod_subtype _ (fun _ ↦ s.mem_toFinset), ← Equiv.prod_comp e.symm]

Premises used: Equiv.prod_comp, Set.mem_toFinset, Equiv.symm, Finset.prod_subtype
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
i : Subtype (Membership.mem s)
h : Membership.mem (γ := Finset (Subtype (Membership.mem s))) univ 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 : ι) ⋯)) ≤
    ‖m ((e.symm : (a : (↑s : Type v)) → α) i)‖

Tactic:
simpa only [i.2, ↓reduceDIte, Subtype.coe_eta] using norm_le_pi_norm (m (e.symm i)) ↑i

Premises used: reduceDIte, norm_le_pi_norm, Subtype.coe_eta, Equiv.symm, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
v : (i : { a : ι // a ∉ s }) → E₁ (↑i : ι)
w : α → (i : ι) → E₁ i
⊢ Eq.{wG + 1} (α := G)
    ((((f.iteratedFDerivComponent (E₁ := E₁) (s := s) e :
                (a : (i : { a : ι // a ∉ s }) → E₁ (↑i : ι)) →
                  ContinuousMultilinearMap 𝕜 (fun (x : α) ↦ (i : ι) → E₁ i) G)
              v :
            ContinuousMultilinearMap 𝕜 (fun (x : α) ↦ (i : ι) → E₁ i) G) :
          (a : (i : α) → (i : ι) → E₁ i) → G)
        w :
      G)
    ((f : (a : (i : ι) → E₁ i) → G) fun (j : ι) ↦
        if h : j ∈ s then w ((e.symm : (a : (↑s : Type v)) → α) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) j h)) j
        else v (Subtype.mk (p := fun (a : ι) ↦ a ∉ s) j h) :
      G)

Tactic:
simp [iteratedFDerivComponent, MultilinearMap.iteratedFDerivComponent,
    MultilinearMap.domDomRestrictₗ]

Premises used: MultilinearMap.iteratedFDerivComponent, ContinuousMultilinearMap.iteratedFDerivComponent, MultilinearMap.domDomRestrictₗ
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : ι) → E₁ i
h₁ : ‖f.iteratedFDerivComponent (E₁ := E₁) (s := s) e‖ ≤ ‖f‖
h₂ :
  ∀ (i : { a : ι // a ∉ s }),
    Membership.mem (γ := Finset { a : ι // a ∉ s }) univ i → norm (E := E₁ (↑i : ι)) (x (↑i : ι)) ≤ ‖x‖
⊢ ‖f.iteratedFDerivComponent (E₁ := E₁) (s := s) e‖ * ∏ i : { a : ι // a ∉ s }, norm (E := E₁ (↑i : ι)) (x (↑i : ι)) ≤
    ‖f‖ * ∏ _i : { a : ι // a ∉ s }, ‖x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : ι) → E₁ i
⊢ ‖f.iteratedFDerivComponent (E₁ := E₁) (s := s) e‖ ≤ ‖f‖

Tactic:
MultilinearMap.mkContinuousMultilinear_norm_le _ (norm_nonneg _) _

Premises used: MultilinearMap.mkContinuousMultilinear_norm_le, ContinuousMultilinearMap.iteratedFDerivComponent, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : ι) → E₁ i
⊢ ‖f.iteratedFDerivComponent (E₁ := E₁) (s := s) e‖ ≤ ‖f‖

Tactic:
exact MultilinearMap.mkContinuousMultilinear_norm_le _ (norm_nonneg _) _

Premises used: MultilinearMap.mkContinuousMultilinear_norm_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : ι) → E₁ i
i : { a : ι // a ∉ s }
h : Membership.mem (γ := Finset { a : ι // a ∉ s }) univ i
⊢ norm (E := E₁ (↑i : ι)) (x (↑i : ι)) ≤ ‖x‖

Tactic:
norm_le_pi_norm _ _

Premises used: norm_le_pi_norm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : ι) → E₁ i
i : { a : ι // a ∉ s }
h : Membership.mem (γ := Finset { a : ι // a ∉ s }) univ i
⊢ norm (E := E₁ (↑i : ι)) (x (↑i : ι)) ≤ ‖x‖

Tactic:
exact norm_le_pi_norm _ _

Premises used: norm_le_pi_norm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : ι) → E₁ i
rw : ‖f‖ * ‖x‖ ^ card.{v} (α := { a : ι // a ∉ s }) univ = ‖f‖ * ‖x‖ ^ Fintype.card.{v} { a : ι // a ∉ s }
rw₁ rw₂ : ‖f‖ * ‖x‖ ^ Fintype.card.{v} { a : ι // a ∉ s } = ‖f‖ * ‖x‖ ^ Fintype.card.{v} { a : ι // a ∉ s }
⊢ ‖f‖ * ∏ _i : { a : ι // a ∉ s }, ‖x‖ = ‖f‖ * ‖x‖ ^ Fintype.card.{v} { a : ι // a ∉ s }

Tactic:
rw [prod_const, card_univ]

Premises used: Finset.card_univ, Finset.prod_const
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : ι) → E₁ i
⊢ ‖f‖ * ‖x‖ ^ Fintype.card.{v} { a : ι // a ∉ s } = ‖f‖ * ‖x‖ ^ (Fintype.card ι - Fintype.card α)

Tactic:
simp [Fintype.card_congr e]

Premises used: Fintype.card_congr
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
⊢ ‖f.iteratedFDeriv (E₁ := E₁) k x‖ ≤
    ∑ e : Fin k ↪ ι,
      norm (E := ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
        ((f.iteratedFDerivComponent (E₁ := E₁) (s := Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι)) e.toEquivRange :
            (a : (i : { a : ι // a ∉ Set.range (⇑e : (a : Fin k) → ι) }) → E₁ (↑i : ι)) →
              ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
          fun (i : { a : ι // a ∉ Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι) }) ↦ x (↑i : ι))

Tactic:
norm_sum_le _ _

Premises used: Set.Mem, ContinuousMultilinearMap.iteratedFDeriv, norm_sum_le