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 ι
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
⊢ 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‖) ⋯
have 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‖) sorry :
          (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‖) sorry :
          (a : (i : ι') → E' i) → G)
        x_1 :
      G)
Tactic: ext1
-- 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 ι
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‖
have refine : max (C * ∏ i : ι, ‖m i‖) 0 = max C 0 * ∏ i : ι, ‖m i‖
Tactic: refine ((f m).mkContinuous_norm_le' _).trans_eq ?_
-- 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 ι
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
⊢ max (C * ∏ i : ι, ‖m i‖) 0 = max C 0 * ∏ i : ι, ‖m i‖
have hc : LE.le (α := ℝ) 0 (∏ i : ι, ‖m i‖)
Tactic: rw [max_mul_of_nonneg, zero_mul]
-- 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 ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
x : G
⊢ norm.{wG'} (E := G')
      (({
              toFun := fun (x : G) ↦
                (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
                    (a : (i : ι) → E i) → G')
                  m,
              map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' } :
            (a : G) → G')
          x :
        G') ≤
    (‖f‖ * ∏ i : ι, ‖m i‖) * ‖x‖
have rw : norm.{wG'} (E := G')
    (({
            toFun := fun (x : G) ↦
              (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
                  (a : (i : ι) → E i) → G')
                m,
            map_add' := sorry, map_smul' := sorry : G →ₗ[𝕜] G' } :
          (a : G) → G')
        x :
      G') ≤
  ‖f‖ * ‖x‖ * ∏ i : ι, ‖m i‖
Tactic: rw [mul_right_comm]
-- 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 ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
inst_11 : DecidableEq ι
m : (i : ι) → E i
i : ι
c : 𝕜
x : E i
⊢ LinearMap.mkContinuous
      {
        toFun := fun (x_1 : G) ↦
          (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_1 : ContinuousMultilinearMap 𝕜 E G') :
              (a : (i : ι) → E i) → G')
            (update (β := E) m i (c • x)),
        map_add' := ⋯, map_smul' := ⋯ }
      (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i (c • x) i_1‖) ⋯ =
    HSMul.hSMul (β := G →L[𝕜] G') c
      (LinearMap.mkContinuous
        {
          toFun := fun (x_1 : G) ↦
            (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_1 : ContinuousMultilinearMap 𝕜 E G') :
                (a : (i : ι) → E i) → G')
              (update (β := E) m i x),
          map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' }
        (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯)
have h : ∀ (x_1 : G),
  Eq.{wG' + 1} (α := G')
    ((LinearMap.mkContinuous
            {
              toFun := fun (x_2 : G) ↦
                (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_2 : ContinuousMultilinearMap 𝕜 E G') :
                    (a : (i : ι) → E i) → G')
                  (update (β := E) m i (c • x)),
              map_add' := sorry, map_smul' := sorry }
            (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i (c • x) i_1‖) sorry :
          (a : G) → G')
        x_1 :
      G')
    ((HSMul.hSMul (β := G →L[𝕜] G') c
            (LinearMap.mkContinuous
              {
                toFun := fun (x_2 : G) ↦
                  (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_2 : ContinuousMultilinearMap 𝕜 E G') :
                      (a : (i : ι) → E i) → G')
                    (update (β := E) m i x),
                map_add' := sorry, map_smul' := sorry : G →ₗ[𝕜] G' }
              (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) sorry) :
          (a : G) → G')
        x_1 :
      G')
Tactic: ext1
-- 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 ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x y : G
⊢ MultilinearMap.mk (M₁ := E)
      (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') (x + y)) ⋯ ⋯ =
    HAdd.hAdd (α := MultilinearMap 𝕜 E G')
      (MultilinearMap.mk (M₁ := E)
        (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x) ⋯ ⋯)
      (MultilinearMap.mk (M₁ := E)
        (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') y) ⋯ ⋯)
have H : ∀ (x_1 : (i : ι) → E i),
  Eq.{wG' + 1} (α := G')
    ((MultilinearMap.mk (M₁ := E)
            (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') (x + y))
            sorry sorry :
          (a : (i : ι) → E i) → G')
        x_1 :
      G')
    ((HAdd.hAdd (α := MultilinearMap 𝕜 E G')
            (MultilinearMap.mk (M₁ := E)
              (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x) sorry
              sorry)
            (MultilinearMap.mk (M₁ := E)
              (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') y) sorry
              sorry) :
          (a : (i : ι) → E i) → G')
        x_1 :
      G')
Tactic: ext1
-- 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 ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
c : 𝕜
x : G
⊢ MultilinearMap.mk (M₁ := E)
      (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') (c • x)) ⋯ ⋯ =
    HSMul.hSMul (α := 𝕜) (β := MultilinearMap 𝕜 E G') ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (MultilinearMap.mk (M₁ := E)
        (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x) ⋯ ⋯)
have H : ∀ (x_1 : (i : ι) → E i),
  Eq.{wG' + 1} (α := G')
    ((MultilinearMap.mk (M₁ := E)
            (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') (c • x))
            sorry sorry :
          (a : (i : ι) → E i) → G')
        x_1 :
      G')
    ((HSMul.hSMul (α := 𝕜) (β := MultilinearMap 𝕜 E G') ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            (MultilinearMap.mk (M₁ := E)
              (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x) sorry
              sorry) :
          (a : (i : ι) → E i) → G')
        x_1 :
      G')
Tactic: ext1
-- 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 ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
m : (i : ι) → E i
⊢ norm.{wG'} (E := G')
      (((({
                    toFun := fun (x : G) ↦
                      MultilinearMap.mk (M₁ := E)
                        (fun (m : (i : ι) → E i) ↦
                          (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x)
                        ⋯ ⋯,
                    map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] MultilinearMap 𝕜 E G' } :
                  (a : G) → MultilinearMap 𝕜 E G')
                x :
              MultilinearMap 𝕜 E G') :
            (a : (i : ι) → E i) → G')
          m :
        G') ≤
    ‖f‖ * ‖x‖ * ∏ i : ι, ‖m i‖
have rw : norm.{wG'} (E := G') ((((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x : G') ≤
  (‖f‖ * ∏ i : ι, ‖m i‖) * ‖x‖
Tactic: rw [LinearMap.coe_mk, AddHom.coe_mk, MultilinearMap.coe_mk, mul_right_comm]
-- 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 ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
m : (i : ι) → E i
⊢ norm.{wG'} (E := G') ((((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x : G') ≤
    (‖f‖ * ∏ i : ι, ‖m i‖) * ‖x‖
have apply : norm (E := G →L[𝕜] G') ((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') * ‖x‖ ≤ (‖f‖ * ∏ i : ι, ‖m i‖) * ‖x‖
Tactic: apply ((f m).le_opNorm x).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 ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
m : (i : ι) → E i
⊢ norm (E := G →L[𝕜] G') ((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') * ‖x‖ ≤ (‖f‖ * ∏ i : ι, ‖m i‖) * ‖x‖
have hbc : norm (E := G →L[𝕜] G') ((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') ≤ ‖f‖ * ∏ 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 ι
f g : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ (f + g).flipMultilinear (E := E) = f.flipMultilinear (E := E) + g.flipMultilinear (E := E)
have H : ∀ (x : (i : ι) → E i) (x_1 : G),
  Eq.{wG' + 1} (α := G')
    (((((f + g).flipMultilinear (E := E) : (a : (i : ι) → E i) → G →L[𝕜] G') x : G →L[𝕜] G') : (a : G) → G') x_1 : G')
    ((((f.flipMultilinear (E := E) + g.flipMultilinear (E := E) : (a : (i : ι) → E i) → G →L[𝕜] G') x : G →L[𝕜] G') :
          (a : G) → G')
        x_1 :
      G')
Tactic: ext
-- 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 ι
c : 𝕜
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ (c • f).flipMultilinear (E := E) =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (f.flipMultilinear (E := E))
have H : ∀ (x : (i : ι) → E i) (x_1 : G),
  Eq.{wG' + 1} (α := G')
    (((((c • f).flipMultilinear (E := E) : (a : (i : ι) → E i) → G →L[𝕜] G') x : G →L[𝕜] G') : (a : G) → G') x_1 : G')
    ((((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (f.flipMultilinear (E := E)) :
                (a : (i : ι) → E i) → G →L[𝕜] G')
              x :
            G →L[𝕜] G') :
          (a : G) → G')
        x_1 :
      G')
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
m : (i : ι) → E i
⊢ ‖g‖ * ∏ i : ι, norm.{wE₁} (E := E₁ i) ((f i : (a : E i) → E₁ i) (m i) : E₁ i) ≤ ‖g‖ * ∏ i : ι, ‖f i‖ * ‖m i‖
have hbc : ∀ (i : ι),
  Membership.mem (γ := Finset ι) univ i → norm.{wE₁} (E := E₁ i) ((f i : (a : E i) → E₁ i) (m i) : E₁ i) ≤ ‖f i‖ * ‖m i‖
Tactic: gcongr with i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
m : (i : ι) → E i
⊢ ‖g‖ * ∏ i : ι, ‖f i‖ * ‖m i‖ = (‖g‖ * ∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖
have rw : ‖g‖ * HMul.hMul (α := ℝ) (∏ x : ι, ‖f x‖) (∏ x : ι, ‖m x‖) = (‖g‖ * ∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖
Tactic: rw [prod_mul_distrib, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
m : (i : ι) → E i
rw : ‖g‖ * HMul.hMul (α := ℝ) (∏ x : ι, ‖f x‖) (∏ x : ι, ‖m x‖) = (‖g‖ * ∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖
⊢ ‖g‖ * ∏ i : ι, ‖f i‖ * ‖m i‖ = (‖g‖ * ∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖
have rw₁ : ‖g‖ * HMul.hMul (α := ℝ) (∏ x : ι, ‖f x‖) (∏ x : ι, ‖m x‖) = ‖g‖ * HMul.hMul (α := ℝ) (∏ i : ι, ‖f i‖) (∏ i : ι, ‖m i‖)
Tactic: rw [prod_mul_distrib, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometry.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
⊢ norm (E := ContinuousMultilinearMap 𝕜 E G)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toContinuousLinearMap) ≤
    ‖g‖
have refine : ∀ (m : (i : ι) → E i),
  norm.{wG} (E := G)
      ((g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toContinuousLinearMap :
            (a : (i : ι) → E i) → G)
          m :
        G) ≤
    ‖g‖ * ∏ i : ι, ‖m i‖
Tactic: refine opNorm_le_bound (norm_nonneg _) fun m => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometry.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
m : (i : ι) → E i
⊢ norm.{wG} (E := G)
      ((g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toContinuousLinearMap :
            (a : (i : ι) → E i) → G)
          m :
        G) ≤
    ‖g‖ * ∏ i : ι, ‖m i‖
have apply : ‖g‖ *
    ∏ i : ι,
      norm.{wE₁} (E := E₁ i)
        ((((fun (i : ι) ↦
                    ((↑((fun (i : ι) ↦ (f i).toContinuousLinearMap) i) :
                        LinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) :
                      LinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)))
                  i :
                LinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) :
              (a : E i) → E₁ i)
            (m i) :
          E₁ i) ≤
  ‖g‖ * ∏ i : ι, ‖m i‖
Tactic: apply (g.le_opNorm _).trans _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometryEquiv.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
⊢ norm (E := ContinuousMultilinearMap 𝕜 E G)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i)) =
    ‖g‖
have apply : ‖g‖ ≤
  norm (E := ContinuousMultilinearMap 𝕜 E G)
    (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toLinearIsometry.toContinuousLinearMap)
Tactic: apply le_antisymm (g.norm_compContinuous_linearIsometry_le fun i => (f i).toLinearIsometry)