awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
⊢ ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)
have refine_2 : ∀ (hz : ‖z‖₊ = 0), ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)
Tactic: obtain hz | hz := eq_zero_or_pos ‖z‖₊
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
refine_2 : ∀ (hz : ‖z‖₊ = 0), ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)
⊢ ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)
have refine_2₁ : ∀ (hz : 0 < ‖z‖₊), ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)
Tactic: obtain hz | hz := eq_zero_or_pos ‖z‖₊
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
hz : 0 < ‖z‖₊
⊢ ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)
have refine_2 : ∀ (m : (i : ι) → E i),
  nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) ≤
    nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) / ‖z‖₊ * ∏ i : ι, ‖m i‖₊
Tactic: rw [← le_div_iff₀ hz, opNNNorm_le_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
hz : 0 < ‖z‖₊
m : (i : ι) → E i
⊢ nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) ≤
    nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) / ‖z‖₊ * ∏ i : ι, ‖m i‖₊
have refine_2 : nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) * ‖z‖₊ ≤
  nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) * ∏ i : ι, ‖m i‖₊
Tactic: rw [div_mul_eq_mul_div, le_div_iff₀ hz]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
hz : 0 < ‖z‖₊
m : (i : ι) → E i
⊢ nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) * ‖z‖₊ ≤
    nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) * ∏ i : ι, ‖m i‖₊
have refine_2 : nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) * ‖z‖₊ ≤
  nnnorm.{wG} (E := G) ((f.smulRight (M₁ := E) z : (a : (i : ι) → E i) → G) m : G)
Tactic: refine le_trans ?_ ((f.smulRight z).le_opNNNorm m)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
hz : 0 < ‖z‖₊
m : (i : ι) → E i
⊢ nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) * ‖z‖₊ ≤
    nnnorm.{wG} (E := G) ((f.smulRight (M₁ := E) z : (a : (i : ι) → E i) → G) m : G)
have refine_2 : nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) * ‖z‖₊ ≤
  ‖HSMul.hSMul.{u, wG, wG} (α := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) z‖₊
Tactic: rw [smulRight_apply, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
hz : 0 < ‖z‖₊
m : (i : ι) → E i
refine_2 :
  nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) * ‖z‖₊ ≤
    ‖HSMul.hSMul.{u, wG, wG} (α := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) z‖₊
⊢ nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) * ‖z‖₊ ≤
    nnnorm.{wG} (E := G) ((f.smulRight (M₁ := E) z : (a : (i : ι) → E i) → G) m : G)
have refine_2₁ : nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) * ‖z‖₊ ≤
  nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) * ‖z‖₊
Tactic: rw [smulRight_apply, nnnorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : Fintype ι
z : G
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) (ContinuousMultilinearMap.mkPiRing 𝕜 ι z) = ‖z‖
have rw : norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G)
    (smulRight (M₁ := fun (x : ι) ↦ 𝕜) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) z) =
  ‖z‖
Tactic: rw [ContinuousMultilinearMap.mkPiRing, norm_smulRight, norm_mkPiAlgebra, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : Fintype ι
z : G
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G)
      (smulRight (M₁ := fun (x : ι) ↦ 𝕜) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) z) =
    ‖z‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) (ContinuousMultilinearMap.mkPiRing 𝕜 ι z) = ‖z‖
have rw₁ : norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜)
      (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜 : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) *
    ‖z‖ =
  ‖z‖
Tactic: rw [ContinuousMultilinearMap.mkPiRing, norm_smulRight, norm_mkPiAlgebra, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : Fintype ι
z : G
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G)
      (smulRight (M₁ := fun (x : ι) ↦ 𝕜) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) z) =
    ‖z‖
rw₁ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜)
        (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜 : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) *
      ‖z‖ =
    ‖z‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) (ContinuousMultilinearMap.mkPiRing 𝕜 ι z) = ‖z‖
have rw₂ : 1 * ‖z‖ = ‖z‖
Tactic: rw [ContinuousMultilinearMap.mkPiRing, norm_smulRight, norm_mkPiAlgebra, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : Fintype ι
z : G
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G)
      (smulRight (M₁ := fun (x : ι) ↦ 𝕜) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜) z) =
    ‖z‖
rw₁ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜)
        (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜 : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) 𝕜) *
      ‖z‖ =
    ‖z‖
rw₂ : 1 * ‖z‖ = ‖z‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) (ContinuousMultilinearMap.mkPiRing 𝕜 ι z) = ‖z‖
have rw₃ : ‖z‖ = ‖z‖
Tactic: rw [ContinuousMultilinearMap.mkPiRing, norm_smulRight, norm_mkPiAlgebra, one_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 : ContinuousMultilinearMap 𝕜 E 𝕜
x y : G
⊢ f.smulRight (M₁ := E) (x + y) =
    HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) x) (f.smulRight (M₁ := E) y)
have H : ∀ (x_1 : (i : ι) → E i),
  Eq.{wG + 1} (α := G) ((f.smulRight (M₁ := E) (x + y) : (a : (i : ι) → E i) → G) x_1 : G)
    ((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) x) (f.smulRight (M₁ := E) y) :
          (a : (i : ι) → E i) → 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 ι
f : ContinuousMultilinearMap 𝕜 E 𝕜
c : 𝕜
x : G
⊢ f.smulRight (M₁ := E) (c • x) =
    HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (f.smulRight (M₁ := E) x)
have 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)
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 ι
f g : ContinuousMultilinearMap 𝕜 E 𝕜
⊢ { 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 }
have h : ∀ (x : G) (x_1 : (i : ι) → E i),
  Eq.{wG + 1} (α := G)
    (((({ toFun := fun (z : G) ↦ (f + g).smulRight (M₁ := E) z, map_add' := sorry, map_smul' := sorry } :
                (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' := sorry, map_smul' := sorry :
                    G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G }
                  { toFun := fun (z : G) ↦ g.smulRight (M₁ := E) z, map_add' := sorry, map_smul' := sorry :
                    G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G } :
                (a : G) → ContinuousMultilinearMap 𝕜 E G)
              x :
            ContinuousMultilinearMap 𝕜 E G) :
          (a : (i : ι) → E i) → 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 : ContinuousMultilinearMap 𝕜 E 𝕜
⊢ { 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 }
have h : ∀ (x : G) (x_1 : (i : ι) → E i),
  Eq.{wG + 1} (α := G)
    (((({ toFun := fun (z : G) ↦ (c • f).smulRight (M₁ := E) z, map_add' := sorry, map_smul' := sorry } :
                (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' := sorry, map_smul' := sorry :
                    G →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E G } :
                (a : G) → ContinuousMultilinearMap 𝕜 E G)
              x :
            ContinuousMultilinearMap 𝕜 E G) :
          (a : (i : ι) → E i) → 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 ι
z z' : G
⊢ ContinuousMultilinearMap.mkPiRing 𝕜 ι (z + z') =
    HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) (ContinuousMultilinearMap.mkPiRing 𝕜 ι z)
      (ContinuousMultilinearMap.mkPiRing 𝕜 ι z')
have 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)
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 : 𝕜
z : G
⊢ ContinuousMultilinearMap.mkPiRing 𝕜 ι (c • z) =
    HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (ContinuousMultilinearMap.mkPiRing 𝕜 ι z)
have 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)
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 ι
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
⊢ 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‖) ⋯
have H₁ : ∀ (x_1 : (i : ι) → E i),
  Eq.{wG' + 1} (α := G')
    ((mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') (x + y)) (C * ‖x + y‖) sorry : (a : (i : ι) → E i) → G')
        x_1 :
      G')
    ((mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') x) (C * ‖x‖) sorry +
            mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') y) (C * ‖y‖) 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 : 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
⊢ 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‖) ⋯)
have H₁ : ∀ (x_1 : (i : ι) → E i),
  Eq.{wG' + 1} (α := G')
    ((mkContinuous (E := E) ((f : (a : G) → MultilinearMap 𝕜 E G') (c • x)) (C * ‖c • x‖) sorry : (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‖) 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 : 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
⊢ max (C * ‖x‖) 0 = max C 0 * ‖x‖
have rw : max (C * ‖x‖) 0 = max (C * ‖x‖) (0 * ‖x‖)
Tactic: rw [max_mul_of_nonneg _ _ (norm_nonneg x), 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 →ₗ[𝕜] 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‖)
⊢ max (C * ‖x‖) 0 = max C 0 * ‖x‖
have rw₁ : max (C * ‖x‖) 0 = max (C * ‖x‖) 0
Tactic: rw [max_mul_of_nonneg _ _ (norm_nonneg x), 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 ι
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
⊢ 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‖) ⋯
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 (x + y)))
            (C * ∏ i_1 : ι, ‖update (β := E) m i (x + y) i_1‖) sorry :
          (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‖) sorry +
            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‖) sorry :
          (a : (i : ι') → E' i) → G)
        x_1 :
      G)
Tactic: ext1