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 ι
f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
C : ℝ
H :
  ∀ (x : G) (m : (i : ι) → E i),
    norm.{wG'} (E := G')
        ((((f : (a : G) → MultilinearMap 𝕜 E G') x : MultilinearMap 𝕜 E G') : (a : (i : ι) → E i) → G') m : G') ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
x : G
⊢ norm (E := ContinuousMultilinearMap 𝕜 E G')
      (({ toFun := fun (x : G) ↦ mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') x) (C * ‖x‖) ⋯,
              map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G' } :
            (a : G) → ContinuousMultilinearMap 𝕜 E G')
          x :
        ContinuousMultilinearMap 𝕜 E G') ≤
    max C 0 * ‖x‖

Tactic:
simpa using ((f x).mkContinuous_norm_le' _).trans_eq <| by
        rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]

Premises used: LE.le.trans_eq, DFunLike.coe, MultilinearMap.mkContinuous_norm_le'
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
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 : SeminormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
inst_7 : Fintype ι
f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
C : ℝ
H :
  ∀ (x : G) (m : (i : ι) → E i),
    norm.{wG'} (E := G')
        ((((f : (a : G) → MultilinearMap 𝕜 E G') x : MultilinearMap 𝕜 E G') : (a : (i : ι) → E i) → G') m : G') ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ norm (E := G →L[𝕜] ContinuousMultilinearMap 𝕜 E G')
      (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := ContinuousMultilinearMap 𝕜 E G') (σ := RingHom.id 𝕜)
        { toFun := fun (x : G) ↦ mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') x) (C * ‖x‖) ⋯,
          map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G' }
        (max C 0) ⋯) ≤
    max C 0

Tactic:
LinearMap.mkContinuous_norm_le _ (le_max_right _ _) _

Premises used: le_max_right, LinearMap.mkContinuous_norm_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
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 : SeminormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
inst_7 : Fintype ι
f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
C : ℝ
H :
  ∀ (x : G) (m : (i : ι) → E i),
    norm.{wG'} (E := G')
        ((((f : (a : G) → MultilinearMap 𝕜 E G') x : MultilinearMap 𝕜 E G') : (a : (i : ι) → E i) → G') m : G') ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ norm (E := G →L[𝕜] ContinuousMultilinearMap 𝕜 E G')
      (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := ContinuousMultilinearMap 𝕜 E G') (σ := RingHom.id 𝕜)
        { toFun := fun (x : G) ↦ mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') x) (C * ‖x‖) ⋯,
          map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G' }
        (max C 0) ⋯) ≤
    max C 0

Tactic:
exact LinearMap.mkContinuous_norm_le _ (le_max_right _ _) _

Premises used: le_max_right, LinearMap.mkContinuous_norm_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
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 : SeminormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
inst_7 : Fintype ι
f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
C : ℝ
hC : 0 ≤ C
H :
  ∀ (x : G) (m : (i : ι) → E i),
    norm.{wG'} (E := G')
        ((((f : (a : G) → MultilinearMap 𝕜 E G') x : MultilinearMap 𝕜 E G') : (a : (i : ι) → E i) → G') m : G') ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ ‖mkContinuousLinear (E := E) f C H‖ ≤ C

Tactic:
(mkContinuousLinear_norm_le' f C H).trans_eq (max_eq_left hC)

Premises used: LE.le.trans_eq, max_eq_left, MultilinearMap.mkContinuousLinear_norm_le'
-- 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 ι
inst_11 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_12 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
inst_13 : DecidableEq ι
m : (i : ι) → E i
i : ι
x y : E i
H₁ :
  ∀ (x_1 : (i : ι') → E' i),
    Eq.{wG + 1} (α := G)
      ((mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i (x + y)))
              (C * ∏ i_1 : ι, ‖update (β := E) m i (x + y) i_1‖) ⋯ :
            (a : (i : ι') → E' i) → G)
          x_1 :
        G)
      ((mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i x))
                (C * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯ +
              mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i y))
                (C * ∏ i_1 : ι, ‖update (β := E) m i y i_1‖) ⋯ :
            (a : (i : ι') → E' i) → G)
          x_1 :
        G)
⊢ mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i (x + y)))
      (C * ∏ i_1 : ι, ‖update (β := E) m i (x + y) i_1‖) ⋯ =
    mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i x))
        (C * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯ +
      mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i y))
        (C * ∏ i_1 : ι, ‖update (β := E) m i y i_1‖) ⋯

Tactic:
ext1
-- 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 ι
inst_11 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_12 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
inst_13 : DecidableEq ι
m : (i : ι) → E i
i : ι
x y : E i
x_1 : (i : ι') → E' i
⊢ Eq.{wG + 1} (α := G)
    ((mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i (x + y)))
            (C * ∏ i_1 : ι, ‖update (β := E) m i (x + y) i_1‖) ⋯ :
          (a : (i : ι') → E' i) → G)
        x_1 :
      G)
    ((mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i x))
              (C * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯ +
            mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i y))
              (C * ∏ i_1 : ι, ‖update (β := E) m i y i_1‖) ⋯ :
          (a : (i : ι') → E' i) → G)
        x_1 :
      G)

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 ι
inst_11 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_12 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
inst_13 : DecidableEq ι
m : (i : ι) → E i
i : ι
c : 𝕜
x : E i
H₁ :
  ∀ (x_1 : (i : ι') → E' i),
    Eq.{wG + 1} (α := G)
      ((mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i (c • x)))
              (C * ∏ i_1 : ι, ‖update (β := E) m i (c • x) i_1‖) ⋯ :
            (a : (i : ι') → E' i) → G)
          x_1 :
        G)
      ((c •
              mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i x))
                (C * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯ :
            (a : (i : ι') → E' i) → G)
          x_1 :
        G)
⊢ mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i (c • x)))
      (C * ∏ i_1 : ι, ‖update (β := E) m i (c • x) i_1‖) ⋯ =
    c •
      mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i x))
        (C * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯

Tactic:
ext1
-- 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 ι
inst_11 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_12 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
inst_13 : DecidableEq ι
m : (i : ι) → E i
i : ι
c : 𝕜
x : E i
x_1 : (i : ι') → E' i
⊢ Eq.{wG + 1} (α := G)
    ((mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i (c • x)))
            (C * ∏ i_1 : ι, ‖update (β := E) m i (c • x) i_1‖) ⋯ :
          (a : (i : ι') → E' i) → G)
        x_1 :
      G)
    ((c •
            mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) (update (β := E) m i x))
              (C * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯ :
          (a : (i : ι') → E' i) → G)
        x_1 :
      G)

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 ι
inst_11 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_12 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : (i : ι) → E i
⊢ ‖mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m) (C * ∏ i : ι, ‖m i‖) ⋯‖ ≤
    max C 0 * ∏ i : ι, ‖m i‖

Tactic:
((f m).mkContinuous_norm_le' _).trans_eq ?_

Premises used: LE.le.trans_eq, DFunLike.coe, MultilinearMap.mkContinuous_norm_le'
-- 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 ι
inst_11 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_12 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : (i : ι) → E i
refine : max (C * ∏ i : ι, ‖m i‖) 0 = max C 0 * ∏ i : ι, ‖m i‖
⊢ ‖mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m) (C * ∏ i : ι, ‖m i‖) ⋯‖ ≤
    max C 0 * ∏ i : ι, ‖m i‖

Tactic:
refine ((f m).mkContinuous_norm_le' _).trans_eq ?_

Premises used: LE.le.trans_eq, DFunLike.coe, MultilinearMap.mkContinuous_norm_le'
-- 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 ι
inst_11 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_12 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : (i : ι) → E i
hc : LE.le (α := ℝ) 0 (∏ i : ι, ‖m i‖)
⊢ max (C * ∏ i : ι, ‖m i‖) 0 = max C 0 * ∏ i : ι, ‖m i‖

Tactic:
rw [max_mul_of_nonneg, zero_mul]

Premises used: max_mul_of_nonneg, MulZeroClass.zero_mul
-- 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 ι
inst_11 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_12 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : (i : ι) → E i
⊢ LE.le (α := ℝ) 0 (∏ i : ι, ‖m i‖)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
G : Type wG
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
inst_6 : Fintype ι
inst_7 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_8 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : (i : ι) → E i
⊢ Eq (α := (a : (i : ι') → E' i) → G)
    (⇑((f.mkContinuousMultilinear (E := E) (E' := E') C H : (a : (i : ι) → E i) → ContinuousMultilinearMap 𝕜 E' G) m :
          ContinuousMultilinearMap 𝕜 E' G) :
      (a : (i : ι') → E' i) → G)
    (⇑((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
G : Type wG
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
inst_6 : Fintype ι
inst_7 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_8 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 E (ContinuousMultilinearMap 𝕜 E' G))
      (mkContinuous (E := E)
        (mk (M₁ := E)
          (fun (m : (i : ι) → E i) ↦
            mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m) (C * ∏ i : ι, ‖m i‖) ⋯)
          ⋯ ⋯)
        (max C 0) ⋯) ≤
    max C 0

Tactic:
mkContinuous_norm_le _ (le_max_right _ _) _

Premises used: le_max_right, MultilinearMap.mkContinuous_norm_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
G : Type wG
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
inst_6 : Fintype ι
inst_7 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_8 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 E (ContinuousMultilinearMap 𝕜 E' G))
      (mkContinuous (E := E)
        (mk (M₁ := E)
          (fun (m : (i : ι) → E i) ↦
            mkContinuous (E := E') ((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m) (C * ∏ i : ι, ‖m i‖) ⋯)
          ⋯ ⋯)
        (max C 0) ⋯) ≤
    max C 0

Tactic:
exact mkContinuous_norm_le _ (le_max_right _ _) _

Premises used: le_max_right, MultilinearMap.mkContinuous_norm_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
G : Type wG
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
inst_6 : Fintype ι
inst_7 : (i : ι') → SeminormedAddCommGroup (E' i)
inst_8 : (i : ι') → NormedSpace.{u, wE'} 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
hC : 0 ≤ C
H :
  ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
    norm.{wG} (E := G)
        ((((f : (a : (i : ι) → E i) → MultilinearMap 𝕜 E' G) m₁ : MultilinearMap 𝕜 E' G) : (a : (i : ι') → E' i) → G)
            m₂ :
          G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ ‖f.mkContinuousMultilinear (E := E) (E' := E') C H‖ ≤ C

Tactic:
(mkContinuousMultilinear_norm_le' f C H).trans_eq (max_eq_left hC)

Premises used: LE.le.trans_eq, max_eq_left, MultilinearMap.mkContinuousMultilinear_norm_le'
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
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 : SeminormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
inst_7 : Fintype ι
g : G →L[𝕜] G'
f : ContinuousMultilinearMap 𝕜 E G
⊢ 0 ≤ ‖g‖ * ‖f‖

Tactic:
positivity
-- 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 ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
x y : G
⊢ (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') (x + y) : ContinuousMultilinearMap 𝕜 E G') :
        (a : (i : ι) → E i) → G')
      m =
    HAdd.hAdd (α := G') (β := G')
      ((((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
            (a : (i : ι) → E i) → G')
          m :
        G')
      ((((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') y : ContinuousMultilinearMap 𝕜 E G') :
            (a : (i : ι) → E i) → G')
          m :
        G')

Tactic:
simp only [map_add, ContinuousMultilinearMap.add_apply]

Premises used: map_add, ContinuousMultilinearMap.add_apply