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 ι
inst_6 : IsEmpty ι
x_1 : G
x : (i : ι) → E i
⊢ Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x_1 : (a : (i : ι) → E i) → G) x : G) ≤ ‖x_1‖ * ∏ i : ι, ‖x i‖
have a : Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x_1 : (a : (i : ι) → E i) → G) x : G) ≤ ‖x_1‖ * 1
Tactic: rw [Fintype.prod_empty, mul_one, constOfIsEmpty_apply]
-- 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 ι
inst_6 : IsEmpty ι
x_1 : G
x : (i : ι) → E i
a : Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x_1 : (a : (i : ι) → E i) → G) x : G) ≤ ‖x_1‖ * 1
⊢ Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x_1 : (a : (i : ι) → E i) → G) x : G) ≤ ‖x_1‖ * ∏ i : ι, ‖x i‖
have a₁ : Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x_1 : (a : (i : ι) → E i) → G) x : G) ≤ ‖x_1‖
Tactic: rw [Fintype.prod_empty, mul_one, constOfIsEmpty_apply]
-- 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 ι
inst_6 : IsEmpty ι
x_1 : G
x : (i : ι) → E i
a : Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x_1 : (a : (i : ι) → E i) → G) x : G) ≤ ‖x_1‖ * 1
a₁ : Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x_1 : (a : (i : ι) → E i) → G) x : G) ≤ ‖x_1‖
⊢ Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x_1 : (a : (i : ι) → E i) → G) x : G) ≤ ‖x_1‖ * ∏ i : ι, ‖x i‖
have a₂ : ‖x_1‖ ≤ ‖x_1‖
Tactic: rw [Fintype.prod_empty, mul_one, constOfIsEmpty_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : SeminormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
k n : ℕ
f : ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
⊢ ‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k)
have hC : 0 ≤ ‖f‖ * ‖z‖ ^ (n - k)
Tactic: apply MultilinearMap.mkContinuous_norm_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : Nonempty ι
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) ≤ 1
have refine : ∀ (m : (i : ι) → A),
  norm.{u_1} (E := A)
      (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
            (a : (i : ι) → A) → A)
          m :
        A) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖m i‖)
Tactic: refine opNorm_le_bound zero_le_one fun m => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : Nonempty ι
m : (i : ι) → A
⊢ norm.{u_1} (E := A)
      (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
            (a : (i : ι) → A) → A)
          m :
        A) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖m i‖)
have simp : norm.{u_1} (E := A) (∏ i : ι, m i) ≤ ∏ i : ι, ‖m i‖
Tactic: simp only [ContinuousMultilinearMap.mkPiAlgebra_apply, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) =
    norm.{u_1} (E := A) 1
have a : norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) ≤
  norm.{u_1} (E := A) 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
a :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) ≤
    norm.{u_1} (E := A) 1
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) =
    norm.{u_1} (E := A) 1
have a₁ : norm.{u_1} (E := A) 1 ≤
  norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) ≤
    norm.{u_1} (E := A) 1
have a : 0 ≤ norm.{u_1} (E := A) 1
Tactic: apply opNorm_le_bound
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
a : 0 ≤ norm.{u_1} (E := A) 1
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) ≤
    norm.{u_1} (E := A) 1
have a₁ : ∀ (m : (i : ι) → A),
  norm.{u_1} (E := A)
      (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
            (a : (i : ι) → A) → A)
          m :
        A) ≤
    norm.{u_1} (E := A) 1 * ∏ i : ι, ‖m i‖
Tactic: apply opNorm_le_bound
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
⊢ norm.{u_1} (E := A) 1 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A)
have h : norm.{u_1} (E := A) 1 =
  norm.{u_1} (E := A)
      (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
            (a : (i : ι) → A) → A)
          fun (x : ι) ↦ 1 :
        A) /
    ∏ i : ι, norm.{u_1} (E := A) 1
Tactic: convert! ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : NormOneClass A
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1
have inl : IsEmpty ι → norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : NormOneClass A
inl :
  IsEmpty ι →
    norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1
have inr : Nonempty ι → norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : NormOneClass A
h : Nonempty ι
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1
have inr : 1 ≤ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A)
Tactic: refine le_antisymm norm_mkPiAlgebra_le ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : NormOneClass A
h : Nonempty ι
⊢ 1 ≤ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A)
have h : 1 =
  norm.{u_1} (E := A)
      (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
            (a : (i : ι) → A) → A)
          fun (x : ι) ↦ 1 :
        A) /
    ∏ i : ι, norm.{u_1} (E := A) 1
Tactic: convert! ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A) ≤
    1
have refine : ∀ (m : (i : Fin n.succ) → A),
  norm (E := A) ((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A : (a : (i : Fin n.succ) → A) → A) m : A) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : Fin n.succ, ‖m i‖)
Tactic: refine opNorm_le_bound zero_le_one fun m => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
⊢ norm (E := A) ((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A : (a : (i : Fin n.succ) → A) → A) m : A) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : Fin n.succ, ‖m i‖)
have simp : ‖(List.map m (List.finRange n.succ)).prod‖ ≤ List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))
Tactic: simp only [ContinuousMultilinearMap.mkPiAlgebraFin_apply, one_mul, List.ofFn_eq_map,
    Fin.prod_univ_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
⊢ ‖(List.map m (List.finRange n.succ)).prod‖ ≤
    List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))
have refine_1 : List.map m (List.finRange n.succ) ≠ []
Tactic: refine (List.norm_prod_le' ?_).trans_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
refine_1 : List.map m (List.finRange n.succ) ≠ []
⊢ ‖(List.map m (List.finRange n.succ)).prod‖ ≤
    List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))
have refine_2 : (List.map norm (List.map m (List.finRange n.succ))).prod =
  List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))
Tactic: refine (List.norm_prod_le' ?_).trans_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
⊢ List.map m (List.finRange n.succ) ≠ []
have refine_1 : ¬n.succ = 0
Tactic: rw [Ne, List.map_eq_nil_iff, List.finRange_eq_nil_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
⊢ (List.map norm (List.map m (List.finRange n.succ))).prod =
    List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))
have refine_2 : (List.map (norm ∘ m) (List.finRange n.succ)).prod =
  List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))
Tactic: rw [List.map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
refine_2 :
  (List.map (norm ∘ m) (List.finRange n.succ)).prod =
    List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))
⊢ (List.map norm (List.map m (List.finRange n.succ))).prod =
    List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))
have refine_2₁ : Eq (α := ℝ) (List.prod (List.map (fun (x : Fin n.succ) ↦ ‖m x‖) (List.finRange n.succ)))
  (List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ)))
Tactic: rw [List.map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
hn : 0 < n
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A) ≤ 1
have obtain : ∀ (n : ℕ) (hn : 0 < n.succ),
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A) ≤
    1
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) =
    norm.{u_1} (E := A) 1
have refine_1 : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) ≤
  norm.{u_1} (E := A) 1
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
refine_1 :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) ≤
    norm.{u_1} (E := A) 1
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) =
    norm.{u_1} (E := A) 1
have refine_2 : norm.{u_1} (E := A) 1 ≤
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) ≤
    norm.{u_1} (E := A) 1
have refine_1 : ∀ (m : (i : Fin 0) → A),
  norm (E := A) ((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A : (a : (i : Fin 0) → A) → A) m : A) ≤
    norm.{u_1} (E := A) 1 * ∏ i : Fin 0, ‖m i‖
Tactic: refine opNorm_le_bound (norm_nonneg (1 : A)) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ norm.{u_1} (E := A) 1 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A)
have h : norm.{u_1} (E := A) 1 =
  norm (E := A) ((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A : (a : (i : Fin 0) → A) → A) fun (x : Fin 0) ↦ 1 : A) /
    ∏ i : Fin 0, norm.{u_1} (E := A) 1
Tactic: convert! ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) fun _ => (1 : A)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A) ≤
    max 1 (norm.{u_1} (E := A) 1)
have zero : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) ≤
  max 1 (norm.{u_1} (E := A) 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
zero :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) ≤
    max 1 (norm.{u_1} (E := A) 1)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A) ≤
    max 1 (norm.{u_1} (E := A) 1)
have succ : ∀ (n : ℕ),
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n + 1) A) ≤
    max 1 (norm.{u_1} (E := A) 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : NormOneClass A
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A) = 1
have zero : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) = 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : NormOneClass A
zero :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) = 1
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A) = 1
have succ : ∀ (n : ℕ),
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n + 1) A) =
    1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : NormOneClass A
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) = 1
have zero : norm.{u_1} (E := A) 1 = 1
Tactic: rw [norm_mkPiAlgebraFin_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : NormOneClass A
n : ℕ
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n + 1) A) =
    1
have succ : 1 ≤
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ A) A)
    (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n + 1) A)
Tactic: refine le_antisymm norm_mkPiAlgebraFin_succ_le ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : NormOneClass A
n : ℕ
⊢ 1 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n + 1) A)
have succ : 1 =
  norm (E := A)
      ((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A : (a : (i : Fin n.succ) → A) → A) fun (x : Fin n.succ) ↦ 1 :
        A) /
    ∏ i : Fin n.succ, norm.{u_1} (E := A) 1
Tactic: refine le_of_eq_of_le ?_ <|
      ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (Nat.succ _) A) fun _ => 1
-- 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
⊢ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) = ‖f‖₊ * ‖z‖₊
have refine_1 : nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) ≤ ‖f‖₊ * ‖z‖₊
Tactic: refine le_antisymm ?_ ?_
-- 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_1 : nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) ≤ ‖f‖₊ * ‖z‖₊
⊢ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) = ‖f‖₊ * ‖z‖₊
have refine_2 : ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)
Tactic: refine le_antisymm ?_ ?_
-- 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
⊢ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) ≤ ‖f‖₊ * ‖z‖₊
have refine_1 : ∀ (m : (i : ι) → E i),
  nnnorm.{u} (E := 𝕜)
        ((LinearMap.id : (a : 𝕜) → 𝕜) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → 𝕜) m : 𝕜) : 𝕜) *
      ‖z‖₊ ≤
    ‖f‖₊ * ‖z‖₊ * ∏ i : ι, ‖m i‖₊
Tactic: refine opNNNorm_le_iff.2 fun m => (nnnorm_smul_le _ _).trans ?_
-- 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
m : (i : ι) → E i
⊢ nnnorm.{u} (E := 𝕜)
        ((LinearMap.id : (a : 𝕜) → 𝕜) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → 𝕜) m : 𝕜) : 𝕜) *
      ‖z‖₊ ≤
    ‖f‖₊ * ‖z‖₊ * ∏ i : ι, ‖m i‖₊
have refine_1 : nnnorm.{u} (E := 𝕜)
      ((LinearMap.id : (a : 𝕜) → 𝕜) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → 𝕜) m : 𝕜) : 𝕜) *
    ‖z‖₊ ≤
  (‖f‖₊ * ∏ i : ι, ‖m i‖₊) * ‖z‖₊
Tactic: rw [mul_right_comm]
-- 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
m : (i : ι) → E i
⊢ nnnorm.{u} (E := 𝕜)
        ((LinearMap.id : (a : 𝕜) → 𝕜) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → 𝕜) m : 𝕜) : 𝕜) *
      ‖z‖₊ ≤
    (‖f‖₊ * ∏ i : ι, ‖m i‖₊) * ‖z‖₊
have refine_1 : nnnorm.{u} (E := 𝕜)
    ((LinearMap.id : (a : 𝕜) → 𝕜) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → 𝕜) m : 𝕜) : 𝕜) ≤
  ‖f‖₊ * ∏ i : ι, ‖m i‖₊
Tactic: gcongr