awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ ∀ (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:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ 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 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A)

Tactic:
ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) fun _ => (1 : A)

Premises used: ContinuousMultilinearMap.mkPiAlgebraFin, ContinuousMultilinearMap.ratio_le_opNorm, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
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
⊢ norm.{u_1} (E := A) 1 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A)

Tactic:
convert! ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) fun _ => (1 : A)

Premises used: ContinuousMultilinearMap.mkPiAlgebraFin, ContinuousMultilinearMap.ratio_le_opNorm, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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 := 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:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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)
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)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A) ≤
    max 1 (norm.{u_1} (E := A) 1)

Tactic:
cases n
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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) ≤
    max 1 (norm.{u_1} (E := A) 1)

Tactic:
norm_mkPiAlgebraFin_zero.le.trans (le_max_right _ _)

Premises used: le_max_right, ContinuousMultilinearMap.norm_mkPiAlgebraFin_zero, Eq.le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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) ≤
    max 1 (norm.{u_1} (E := A) 1)

Tactic:
exact norm_mkPiAlgebraFin_zero.le.trans (le_max_right _ _)

Premises used: le_max_right, ContinuousMultilinearMap.norm_mkPiAlgebraFin_zero, Eq.le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
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:
(norm_mkPiAlgebraFin_le_of_pos (Nat.zero_lt_succ _)).trans (le_max_left _ _)

Premises used: Nat.zero_lt_succ, ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
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:
exact (norm_mkPiAlgebraFin_le_of_pos (Nat.zero_lt_succ _)).trans (le_max_left _ _)

Premises used: Nat.zero_lt_succ, ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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
succ :
  ∀ (n : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ A) A)
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n + 1) A) =
      1
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A) = 1

Tactic:
cases n
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : NormOneClass A
zero : norm.{u_1} (E := A) 1 = 1
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) = 1

Tactic:
rw [norm_mkPiAlgebraFin_zero]

Premises used: ContinuousMultilinearMap.norm_mkPiAlgebraFin_zero
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : NormOneClass A
⊢ norm.{u_1} (E := A) 1 = 1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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

Tactic:
le_antisymm norm_mkPiAlgebraFin_succ_le ?_

Premises used: le_antisymm, ContinuousMultilinearMap.norm_mkPiAlgebraFin_succ_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : NormOneClass A
n : ℕ
succ :
  1 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n + 1) A)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n + 1) A) =
    1

Tactic:
refine le_antisymm norm_mkPiAlgebraFin_succ_le ?_

Premises used: le_antisymm, ContinuousMultilinearMap.norm_mkPiAlgebraFin_succ_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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)

Tactic:
le_of_eq_of_le ?_ <|
      ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (Nat.succ _) A) fun _ => 1

Premises used: ContinuousMultilinearMap.mkPiAlgebraFin, ContinuousMultilinearMap.ratio_le_opNorm, le_of_eq_of_le, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : NormOneClass A
n : ℕ
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
⊢ 1 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n + 1) A)

Tactic:
refine le_of_eq_of_le ?_ <|
      ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (Nat.succ _) A) fun _ => 1

Premises used: ContinuousMultilinearMap.mkPiAlgebraFin, ContinuousMultilinearMap.ratio_le_opNorm, le_of_eq_of_le, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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 := 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:
simp
-- 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
⊢ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) = ‖f‖₊ * ‖z‖₊

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
refine_1 : nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) ≤ ‖f‖₊ * ‖z‖₊
refine_2 : ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)
⊢ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) = ‖f‖₊ * ‖z‖₊

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
⊢ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) ≤ ‖f‖₊ * ‖z‖₊

Tactic:
opNNNorm_le_iff.2 fun m => (nnnorm_smul_le _ _).trans ?_

Premises used: Iff.mpr, LinearMap.id, nnnorm_smul_le, ContinuousMultilinearMap.toMultilinearMap, ContinuousMultilinearMap.opNNNorm_le_iff, LE.le.trans, DFunLike.coe
-- 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
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‖₊
⊢ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) ≤ ‖f‖₊ * ‖z‖₊

Tactic:
refine opNNNorm_le_iff.2 fun m => (nnnorm_smul_le _ _).trans ?_

Premises used: Iff.mpr, ContinuousMultilinearMap.opNNNorm_le_iff
-- 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
m : (i : ι) → E i
refine_1 :
  nnnorm.{u} (E := 𝕜)
        ((LinearMap.id : (a : 𝕜) → 𝕜) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → 𝕜) m : 𝕜) : 𝕜) *
      ‖z‖₊ ≤
    (‖f‖₊ * ∏ i : ι, ‖m i‖₊) * ‖z‖₊
⊢ nnnorm.{u} (E := 𝕜)
        ((LinearMap.id : (a : 𝕜) → 𝕜) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → 𝕜) m : 𝕜) : 𝕜) *
      ‖z‖₊ ≤
    ‖f‖₊ * ‖z‖₊ * ∏ i : ι, ‖m i‖₊

Tactic:
rw [mul_right_comm]

Premises used: mul_right_comm
-- 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
m : (i : ι) → E i
refine_1 :
  nnnorm.{u} (E := 𝕜)
      ((LinearMap.id : (a : 𝕜) → 𝕜) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → 𝕜) m : 𝕜) : 𝕜) ≤
    ‖f‖₊ * ∏ i : ι, ‖m i‖₊
⊢ nnnorm.{u} (E := 𝕜)
        ((LinearMap.id : (a : 𝕜) → 𝕜) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → 𝕜) m : 𝕜) : 𝕜) *
      ‖z‖₊ ≤
    (‖f‖₊ * ∏ i : ι, ‖m i‖₊) * ‖z‖₊

Tactic:
gcongr
-- 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
m : (i : ι) → E i
⊢ nnnorm.{u} (E := 𝕜)
      ((LinearMap.id : (a : 𝕜) → 𝕜) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → 𝕜) m : 𝕜) : 𝕜) ≤
    ‖f‖₊ * ∏ i : ι, ‖m i‖₊

Tactic:
le_opNNNorm _ _

Premises used: ContinuousMultilinearMap.le_opNNNorm
-- 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
m : (i : ι) → E i
⊢ nnnorm.{u} (E := 𝕜)
      ((LinearMap.id : (a : 𝕜) → 𝕜) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → 𝕜) m : 𝕜) : 𝕜) ≤
    ‖f‖₊ * ∏ i : ι, ‖m i‖₊

Tactic:
exact le_opNNNorm _ _

Premises used: ContinuousMultilinearMap.le_opNNNorm
-- 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
refine_2 : ∀ (hz : ‖z‖₊ = 0), ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)
refine_2₁ : ∀ (hz : 0 < ‖z‖₊), ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)
⊢ ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)

Tactic:
obtain hz | hz := eq_zero_or_pos ‖z‖₊

Premises used: NNNorm.nnnorm, eq_zero_or_pos
-- 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
hz : ‖z‖₊ = 0
⊢ ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)

Tactic:
simp [hz]
-- 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
hz : 0 < ‖z‖₊
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‖₊
⊢ ‖f‖₊ * ‖z‖₊ ≤ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z)

Tactic:
rw [← le_div_iff₀ hz, opNNNorm_le_iff]

Premises used: ContinuousMultilinearMap.opNNNorm_le_iff, le_div_iff₀
-- 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
hz : 0 < ‖z‖₊
m : (i : ι) → E i
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‖₊
⊢ 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 [div_mul_eq_mul_div, le_div_iff₀ hz]

Premises used: div_mul_eq_mul_div, le_div_iff₀
-- 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
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‖₊

Tactic:
le_trans ?_ ((f.smulRight z).le_opNNNorm m)

Premises used: ContinuousMultilinearMap.smulRight, ContinuousMultilinearMap.le_opNNNorm, le_trans
-- 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
hz : 0 < ‖z‖₊
m : (i : ι) → E i
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)
⊢ nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) * ‖z‖₊ ≤
    nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) * ∏ i : ι, ‖m i‖₊

Tactic:
refine le_trans ?_ ((f.smulRight z).le_opNNNorm m)

Premises used: ContinuousMultilinearMap.smulRight, ContinuousMultilinearMap.le_opNNNorm, le_trans
-- 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
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‖₊
refine_2₁ refine_2₂ :
  nnnorm.{u} (E := 𝕜) ((f : (a : (i : ι) → E i) → 𝕜) m : 𝕜) * ‖z‖₊ ≤
    nnnorm.{u} (E := 𝕜) ((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)

Tactic:
rw [smulRight_apply, nnnorm_smul]

Premises used: nnnorm_smul, ContinuousMultilinearMap.smulRight_apply
-- 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
⊢ norm (E := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) z) = ‖f‖ * ‖z‖

Tactic:
congr_arg NNReal.toReal (nnnorm_smulRight f z)

Premises used: congr_arg, ContinuousMultilinearMap.nnnorm_smulRight, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
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‖
rw₃ rw₄ : ‖z‖ = ‖z‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ 𝕜) G) (ContinuousMultilinearMap.mkPiRing 𝕜 ι z) = ‖z‖

Tactic:
rw [ContinuousMultilinearMap.mkPiRing, norm_smulRight, norm_mkPiAlgebra, one_mul]

Premises used: ContinuousMultilinearMap.norm_mkPiAlgebra, ContinuousMultilinearMap.mkPiRing, ContinuousMultilinearMap.norm_smulRight, one_mul
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E 𝕜
x y : G
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)
⊢ f.smulRight (M₁ := E) (x + y) =
    HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E G) (f.smulRight (M₁ := E) x) (f.smulRight (M₁ := E) y)

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 𝕜
x y : G
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:
simp