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 : ContinuousMultilinearMap 𝕜 E 𝕜
c : 𝕜
x : G
H :
  ∀ (x_1 : (i : ι) → E i),
    Eq.{wG + 1} (α := G) ((f.smulRight (M₁ := E) (c • x) : (a : (i : ι) → E i) → G) x_1 : G)
      ((HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
              (f.smulRight (M₁ := E) x) :
            (a : (i : ι) → E i) → G)
          x_1 :
        G)
⊢ f.smulRight (M₁ := E) (c • x) =
    HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (f.smulRight (M₁ := E) x)

Tactic:
ext
-- 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 : ContinuousMultilinearMap 𝕜 E 𝕜
c : 𝕜
x : G
x_1 : (i : ι) → E i
⊢ Eq.{wG + 1} (α := G) ((f.smulRight (M₁ := E) (c • x) : (a : (i : ι) → E i) → G) x_1 : G)
    ((HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            (f.smulRight (M₁ := E) x) :
          (a : (i : ι) → E i) → G)
        x_1 :
      G)

Tactic:
simp [smul_smul, mul_comm]

Premises used: smul_smul, mul_comm
-- 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 : ContinuousMultilinearMap 𝕜 E 𝕜
h :
  ∀ (x : G) (x_1 : (i : ι) → E i),
    Eq.{wG + 1} (α := G)
      (((({ toFun := fun (z : G) ↦ (f + g).smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ } :
                  (a : G) → ContinuousMultilinearMap 𝕜 E G)
                x :
              ContinuousMultilinearMap 𝕜 E G) :
            (a : (i : ι) → E i) → G)
          x_1 :
        G)
      ((((HAdd.hAdd (α := G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G)
                    { toFun := fun (z : G) ↦ f.smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ :
                      G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G }
                    { toFun := fun (z : G) ↦ g.smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ :
                      G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G } :
                  (a : G) → ContinuousMultilinearMap 𝕜 E G)
                x :
              ContinuousMultilinearMap 𝕜 E G) :
            (a : (i : ι) → E i) → G)
          x_1 :
        G)
⊢ { toFun := fun (z : G) ↦ (f + g).smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G)
      { toFun := fun (z : G) ↦ f.smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ :
        G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G }
      { toFun := fun (z : G) ↦ g.smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ :
        G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G }

Tactic:
ext
-- 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 : ContinuousMultilinearMap 𝕜 E 𝕜
x : G
x_1 : (i : ι) → E i
⊢ Eq.{wG + 1} (α := G)
    (((({ toFun := fun (z : G) ↦ (f + g).smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ } :
                (a : G) → ContinuousMultilinearMap 𝕜 E G)
              x :
            ContinuousMultilinearMap 𝕜 E G) :
          (a : (i : ι) → E i) → G)
        x_1 :
      G)
    ((((HAdd.hAdd (α := G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G)
                  { toFun := fun (z : G) ↦ f.smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ :
                    G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G }
                  { toFun := fun (z : G) ↦ g.smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ :
                    G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G } :
                (a : G) → ContinuousMultilinearMap 𝕜 E G)
              x :
            ContinuousMultilinearMap 𝕜 E G) :
          (a : (i : ι) → E i) → G)
        x_1 :
      G)

Tactic:
simp [add_smul]

Premises used: add_smul
-- 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 ι
c : 𝕜
f : ContinuousMultilinearMap 𝕜 E 𝕜
h :
  ∀ (x : G) (x_1 : (i : ι) → E i),
    Eq.{wG + 1} (α := G)
      (((({ toFun := fun (z : G) ↦ (c • f).smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ } :
                  (a : G) → ContinuousMultilinearMap 𝕜 E G)
                x :
              ContinuousMultilinearMap 𝕜 E G) :
            (a : (i : ι) → E i) → G)
          x_1 :
        G)
      ((((HSMul.hSMul (α := 𝕜) (β := G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
                    { toFun := fun (z : G) ↦ f.smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ :
                      G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G } :
                  (a : G) → ContinuousMultilinearMap 𝕜 E G)
                x :
              ContinuousMultilinearMap 𝕜 E G) :
            (a : (i : ι) → E i) → G)
          x_1 :
        G)
⊢ { toFun := fun (z : G) ↦ (c • f).smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := 𝕜) (β := G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      { toFun := fun (z : G) ↦ f.smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ :
        G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G }

Tactic:
ext
-- 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 ι
c : 𝕜
f : ContinuousMultilinearMap 𝕜 E 𝕜
x : G
x_1 : (i : ι) → E i
⊢ Eq.{wG + 1} (α := G)
    (((({ toFun := fun (z : G) ↦ (c • f).smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ } :
                (a : G) → ContinuousMultilinearMap 𝕜 E G)
              x :
            ContinuousMultilinearMap 𝕜 E G) :
          (a : (i : ι) → E i) → G)
        x_1 :
      G)
    ((((HSMul.hSMul (α := 𝕜) (β := G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
                  { toFun := fun (z : G) ↦ f.smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ :
                    G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G } :
                (a : G) → ContinuousMultilinearMap 𝕜 E G)
              x :
            ContinuousMultilinearMap 𝕜 E G) :
          (a : (i : ι) → E i) → G)
        x_1 :
      G)

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- 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 : ContinuousMultilinearMap 𝕜 E 𝕜
z : G
⊢ norm (E := ContinuousMultilinearMap 𝕜 E G)
      (((({
                    toFun := fun (f : ContinuousMultilinearMap 𝕜 E 𝕜) ↦
                      { toFun := fun (z : G) ↦ f.smulRight (M₁ := E) z, map_add' := ⋯, map_smul' := ⋯ :
                        G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G },
                    map_add' := ⋯, map_smul' := ⋯ :
                    ContinuousMultilinearMap 𝕜 E 𝕜 →ₗ[𝕜] G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G } :
                  (a : ContinuousMultilinearMap 𝕜 E 𝕜) → G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G)
                f :
              G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G) :
            (a : G) → ContinuousMultilinearMap 𝕜 E G)
          z :
        ContinuousMultilinearMap 𝕜 E G) ≤
    1 * ‖f‖ * ‖z‖

Tactic:
simp [norm_smulRight]

Premises used: ContinuousMultilinearMap.norm_smulRight
-- 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 𝕜
z : G
⊢ Eq (α := ContinuousMultilinearMap 𝕜 E G)
    ((((smulRightL 𝕜 E G : (a : ContinuousMultilinearMap 𝕜 E 𝕜) → G →L[𝕜] ContinuousMultilinearMap 𝕜 E G) f :
            G →L[𝕜] ContinuousMultilinearMap 𝕜 E G) :
          (a : G) → ContinuousMultilinearMap 𝕜 E G)
        z :
      ContinuousMultilinearMap 𝕜 E G)
    (f.smulRight (M₁ := E) z : ContinuousMultilinearMap 𝕜 E G)

Tactic:
rfl

Premises used: ContinuousMultilinearMap.smulRight, rfl
-- 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 ι
⊢ norm (E := ContinuousMultilinearMap 𝕜 E 𝕜 →L[𝕜] G →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (smulRightL 𝕜 E G) ≤ 1

Tactic:
LinearMap.mkContinuous₂_norm_le _ zero_le_one _

Premises used: zero_le_one, LinearMap.mkContinuous₂_norm_le, ContinuousMultilinearMap.smulRightL
-- 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 ι
z z' : G
h :
  Eq.{wG + 1} (α := G) ((ContinuousMultilinearMap.mkPiRing 𝕜 ι (z + z') : (a : (i : ι) → 𝕜) → G) fun (x : ι) ↦ 1 : G)
    ((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) (ContinuousMultilinearMap.mkPiRing 𝕜 ι z)
            (ContinuousMultilinearMap.mkPiRing 𝕜 ι z') :
          (a : (i : ι) → 𝕜) → G)
        fun (x : ι) ↦ 1 :
      G)
⊢ ContinuousMultilinearMap.mkPiRing 𝕜 ι (z + z') =
    HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) (ContinuousMultilinearMap.mkPiRing 𝕜 ι z)
      (ContinuousMultilinearMap.mkPiRing 𝕜 ι z')

Tactic:
ext
-- 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 ι
z z' : G
⊢ Eq.{wG + 1} (α := G) ((ContinuousMultilinearMap.mkPiRing 𝕜 ι (z + z') : (a : (i : ι) → 𝕜) → G) fun (x : ι) ↦ 1 : G)
    ((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) (ContinuousMultilinearMap.mkPiRing 𝕜 ι z)
            (ContinuousMultilinearMap.mkPiRing 𝕜 ι z') :
          (a : (i : ι) → 𝕜) → G)
        fun (x : ι) ↦ 1 :
      G)

Tactic:
simp [smul_add]

Premises used: smul_add
-- 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 ι
c : 𝕜
z : G
h :
  Eq.{wG + 1} (α := G) ((ContinuousMultilinearMap.mkPiRing 𝕜 ι (c • z) : (a : (i : ι) → 𝕜) → G) fun (x : ι) ↦ 1 : G)
    ((HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            (ContinuousMultilinearMap.mkPiRing 𝕜 ι z) :
          (a : (i : ι) → 𝕜) → G)
        fun (x : ι) ↦ 1 :
      G)
⊢ ContinuousMultilinearMap.mkPiRing 𝕜 ι (c • z) =
    HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (ContinuousMultilinearMap.mkPiRing 𝕜 ι z)

Tactic:
ext
-- 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 ι
c : 𝕜
z : G
⊢ Eq.{wG + 1} (α := G) ((ContinuousMultilinearMap.mkPiRing 𝕜 ι (c • z) : (a : (i : ι) → 𝕜) → G) fun (x : ι) ↦ 1 : G)
    ((HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            (ContinuousMultilinearMap.mkPiRing 𝕜 ι z) :
          (a : (i : ι) → 𝕜) → G)
        fun (x : ι) ↦ 1 :
      G)

Tactic:
simp [smul_smul, mul_comm]

Premises used: smul_smul, mul_comm
-- 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 ι
z : G
⊢ (fun (f : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) ↦ ((f : (a : (i : ι) → 𝕜) → G) fun (x : ι) ↦ 1 : G))
      ((fun (z : G) ↦ (ContinuousMultilinearMap.mkPiRing 𝕜 ι z : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G)) z) =
    z

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 ι
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 y : G
H₁ :
  ∀ (x_1 : (i : ι) → E i),
    Eq.{wG' + 1} (α := G')
      ((mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') (x + y)) (C * ‖x + y‖) ⋯ :
            (a : (i : ι) → E i) → G')
          x_1 :
        G')
      ((mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') x) (C * ‖x‖) ⋯ +
              mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') y) (C * ‖y‖) ⋯ :
            (a : (i : ι) → E i) → G')
          x_1 :
        G')
⊢ mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') (x + y)) (C * ‖x + y‖) ⋯ =
    mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') x) (C * ‖x‖) ⋯ +
      mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') y) (C * ‖y‖) ⋯

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 ι
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 y : G
x_1 : (i : ι) → E i
⊢ Eq.{wG' + 1} (α := G')
    ((mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') (x + y)) (C * ‖x + y‖) ⋯ : (a : (i : ι) → E i) → G')
        x_1 :
      G')
    ((mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') x) (C * ‖x‖) ⋯ +
            mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') y) (C * ‖y‖) ⋯ :
          (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 ι
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‖
c : 𝕜
x : G
H₁ :
  ∀ (x_1 : (i : ι) → E i),
    Eq.{wG' + 1} (α := G')
      ((mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') (c • x)) (C * ‖c • x‖) ⋯ :
            (a : (i : ι) → E i) → G')
          x_1 :
        G')
      ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
              (mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') x) (C * ‖x‖) ⋯) :
            (a : (i : ι) → E i) → G')
          x_1 :
        G')
⊢ mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') (c • x)) (C * ‖c • x‖) ⋯ =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') x) (C * ‖x‖) ⋯)

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 ι
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‖
c : 𝕜
x : G
x_1 : (i : ι) → E i
⊢ Eq.{wG' + 1} (α := G')
    ((mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') (c • x)) (C * ‖c • x‖) ⋯ : (a : (i : ι) → E i) → G')
        x_1 :
      G')
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            (mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') x) (C * ‖x‖) ⋯) :
          (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 ι
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
rw : max (C * ‖x‖) 0 = max (C * ‖x‖) (0 * ‖x‖)
rw₁ rw₂ : max (C * ‖x‖) 0 = max (C * ‖x‖) 0
⊢ max (C * ‖x‖) 0 = max C 0 * ‖x‖

Tactic:
rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]

Premises used: max_mul_of_nonneg, MulZeroClass.zero_mul, norm_nonneg