awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
c : 𝕜
x : F
x_1 : ι → E
⊢ Eq.{wG + 1} (α := G)
    ((mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) (c • x)) (C * ‖c • x‖) ⋯ : (a : ι → E) → G) x_1 : G)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            (mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x) (C * ‖x‖) ⋯) :
          (a : ι → E) → G)
        x_1 :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
x : F
rw : max (C * ‖x‖) 0 = max (C * ‖x‖) (0 * ‖x‖)
rw₁ rw₂ : max (C * ‖x‖) 0 = max (C * ‖x‖) 0
⊢ max (C * ‖x‖) 0 = max C 0 * ‖x‖

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

Premises used: max_mul_of_nonneg, MulZeroClass.zero_mul, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
x : F
⊢ ‖mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x) (C * ‖x‖) ⋯‖ ≤ max C 0 * ‖x‖

Tactic:
exact (mkContinuous_norm_le' _ _).trans_eq <| by
        rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]

Premises used: LE.le.trans_eq, AlternatingMap.mkContinuous_norm_le'
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ ‖mkContinuousLinear f C H‖ ≤ max C 0

Tactic:
LinearMap.mkContinuous_norm_le _ (le_max_right _ _) _

Premises used: le_max_right, LinearMap.mkContinuous_norm_le, AlternatingMap.mkContinuousLinear
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
hC : 0 ≤ C
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ ‖mkContinuousLinear f C H‖ ≤ C

Tactic:
(mkContinuousLinear_norm_le_max f C H).trans_eq (max_eq_left hC)

Premises used: LE.le.trans_eq, max_eq_left, AlternatingMap.mkContinuousLinear_norm_le_max
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
inst_9 : DecidableEq ι
m : (i : ι) → E
i : ι
x y : E
H₁ :
  ∀ (x_1 : ι' → F),
    Eq.{wG + 1} (α := G)
      ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i (x + y)))
              (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i (x + y) i_1‖) ⋯ :
            (a : ι' → F) → G)
          x_1 :
        G)
      ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i x))
                (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i x i_1‖) ⋯ +
              mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i y))
                (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i y i_1‖) ⋯ :
            (a : ι' → F) → G)
          x_1 :
        G)
⊢ mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i (x + y)))
      (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i (x + y) i_1‖) ⋯ =
    mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i x))
        (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i x i_1‖) ⋯ +
      mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i y))
        (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i y i_1‖) ⋯

Tactic:
ext1
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
inst_9 : DecidableEq ι
m : (i : ι) → E
i : ι
x y : E
x_1 : ι' → F
⊢ Eq.{wG + 1} (α := G)
    ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i (x + y)))
            (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i (x + y) i_1‖) ⋯ :
          (a : ι' → F) → G)
        x_1 :
      G)
    ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i x))
              (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i x i_1‖) ⋯ +
            mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i y))
              (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i y i_1‖) ⋯ :
          (a : ι' → F) → G)
        x_1 :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
inst_9 : DecidableEq ι
m : (i : ι) → E
i : ι
c : 𝕜
x : E
H₁ :
  ∀ (x_1 : ι' → F),
    Eq.{wG + 1} (α := G)
      ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i (c • x)))
              (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i (c • x) i_1‖) ⋯ :
            (a : ι' → F) → G)
          x_1 :
        G)
      ((c •
              mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i x))
                (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i x i_1‖) ⋯ :
            (a : ι' → F) → G)
          x_1 :
        G)
⊢ mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i (c • x)))
      (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i (c • x) i_1‖) ⋯ =
    c •
      mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i x))
        (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i x i_1‖) ⋯

Tactic:
ext1
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
inst_9 : DecidableEq ι
m : (i : ι) → E
i : ι
c : 𝕜
x : E
x_1 : ι' → F
⊢ Eq.{wG + 1} (α := G)
    ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i (c • x)))
            (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i (c • x) i_1‖) ⋯ :
          (a : ι' → F) → G)
        x_1 :
      G)
    ((c •
            mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) (Function.update (β := fun (x : ι) ↦ E) m i x))
              (C * ∏ i_1 : ι, ‖Function.update (β := fun (x : ι) ↦ E) m i x i_1‖) ⋯ :
          (a : ι' → F) → G)
        x_1 :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
v : ι → E
i j : ι
hv : v i = v j
hij : i ≠ j
H₁ :
  ∀ (v' : ι' → F),
    Eq.{wG + 1} (α := G)
      ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) v) (C * ∏ i : ι, ‖v i‖) ⋯ : (a : ι' → F) → G) v' : G)
      ((0 : (a : ι' → F) → G) v' : G)
⊢ mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) v) (C * ∏ i : ι, ‖v i‖) ⋯ = 0

Tactic:
ext v'
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
v : ι → E
i j : ι
hv : v i = v j
hij : i ≠ j
v' : ι' → F
⊢ Eq (α := F [⋀^ι']→ₗ[𝕜] G) ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) v : F [⋀^ι']→ₗ[𝕜] G) (0 : F [⋀^ι']→ₗ[𝕜] G)

Tactic:
simpa using f.map_eq_zero_of_eq' v i j hv hij

Premises used: AlternatingMap.map_eq_zero_of_eq'
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
v : ι → E
i j : ι
hv : v i = v j
hij : i ≠ j
v' : ι' → F
⊢ Eq (α := F [⋀^ι']→ₗ[𝕜] G) ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) v : F [⋀^ι']→ₗ[𝕜] G) (0 : F [⋀^ι']→ₗ[𝕜] G)

Tactic:
have : f v = 0 := by simpa using f.map_eq_zero_of_eq' v i j hv hij
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
v : ι → E
i j : ι
hv : v i = v j
hij : i ≠ j
v' : ι' → F
this : Eq (α := F [⋀^ι']→ₗ[𝕜] G) ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) v : F [⋀^ι']→ₗ[𝕜] G) (0 : F [⋀^ι']→ₗ[𝕜] G)
⊢ Eq.{wG + 1} (α := G)
    ((mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) v) (C * ∏ i : ι, ‖v i‖) ⋯ : (a : ι' → F) → G) v' : G)
    ((0 : (a : ι' → F) → G) v' : G)

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : ι → E
⊢ ‖mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m) (C * ∏ i : ι, ‖m i‖) ⋯‖ ≤ max C 0 * ∏ i : ι, ‖m i‖

Tactic:
((f m).mkContinuous_norm_le' _).trans_eq ?_

Premises used: LE.le.trans_eq, DFunLike.coe, AlternatingMap.mkContinuous_norm_le'
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : ι → E
refine : max (C * ∏ i : ι, ‖m i‖) 0 = max C 0 * ∏ i : ι, ‖m i‖
⊢ ‖mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m) (C * ∏ i : ι, ‖m i‖) ⋯‖ ≤ max C 0 * ∏ i : ι, ‖m i‖

Tactic:
refine ((f m).mkContinuous_norm_le' _).trans_eq ?_

Premises used: LE.le.trans_eq, DFunLike.coe, AlternatingMap.mkContinuous_norm_le'
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : ι → E
hc : LE.le (α := ℝ) 0 (∏ i : ι, ‖m i‖)
⊢ max (C * ∏ i : ι, ‖m i‖) 0 = max C 0 * ∏ i : ι, ‖m i‖

Tactic:
rw [max_mul_of_nonneg, zero_mul]

Premises used: max_mul_of_nonneg, MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : ι → E
⊢ LE.le (α := ℝ) 0 (∏ i : ι, ‖m i‖)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
m : ι → E
⊢ Eq (α := (a : ι' → F) → G)
    (⇑((f.mkContinuousAlternating C H : (a : ι → E) → F [⋀^ι']→L[𝕜] G) m : F [⋀^ι']→L[𝕜] G) : (a : ι' → F) → G)
    (⇑((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ norm (E := E [⋀^ι]→L[𝕜] F [⋀^ι']→L[𝕜] G)
      (mkContinuous
        { toFun := fun (m : (i : ι) → E) ↦ mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m) (C * ∏ i : ι, ‖m i‖) ⋯,
          map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→L[𝕜] G }
        (max C 0) ⋯) ≤
    max C 0

Tactic:
mkContinuous_norm_le _ (le_max_right _ _) _

Premises used: le_max_right, AlternatingMap.mkContinuous_norm_le
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ norm (E := E [⋀^ι]→L[𝕜] F [⋀^ι']→L[𝕜] G)
      (mkContinuous
        { toFun := fun (m : (i : ι) → E) ↦ mkContinuous ((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m) (C * ∏ i : ι, ‖m i‖) ⋯,
          map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→L[𝕜] G }
        (max C 0) ⋯) ≤
    max C 0

Tactic:
exact mkContinuous_norm_le _ (le_max_right _ _) _

Premises used: le_max_right, AlternatingMap.mkContinuous_norm_le
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
ι' : Type u_1
inst_8 : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
hC : 0 ≤ C
H :
  ∀ (m₁ : ι → E) (m₂ : ι' → F),
    norm.{wG} (E := G) ((((f : (a : ι → E) → F [⋀^ι']→ₗ[𝕜] G) m₁ : F [⋀^ι']→ₗ[𝕜] G) : (a : ι' → F) → G) m₂ : G) ≤
      (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖
⊢ ‖f.mkContinuousAlternating C H‖ ≤ C

Tactic:
(mkContinuousAlternating_norm_le_max f H).trans_eq (max_eq_left hC)

Premises used: LE.le.trans_eq, max_eq_left, AlternatingMap.mkContinuousAlternating_norm_le_max
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
F : Type wF
ι : Type v
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : Subsingleton ι
inst_5 : Nontrivial F
i : ι
⊢ norm (E := F [⋀^ι]→L[𝕜] F)
      ((ofSubsingleton 𝕜 F F i : (a : F →L[𝕜] F) → F [⋀^ι]→L[𝕜] F) (ContinuousLinearMap.id 𝕜 F) : F [⋀^ι]→L[𝕜] F) =
    1

Tactic:
ContinuousMultilinearMap.norm_ofSubsingleton_id 𝕜 F i

Premises used: ContinuousMultilinearMap.norm_ofSubsingleton_id
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
F : Type wF
ι : Type v
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : Subsingleton ι
inst_5 : Nontrivial F
i : ι
⊢ nnnorm (E := F [⋀^ι]→L[𝕜] F)
      ((ofSubsingleton 𝕜 F F i : (a : F →L[𝕜] F) → F [⋀^ι]→L[𝕜] F) (ContinuousLinearMap.id 𝕜 F) : F [⋀^ι]→L[𝕜] F) =
    1

Tactic:
NNReal.eq <| norm_ofSubsingleton_id ..

Premises used: NNReal.eq, ContinuousAlternatingMap.norm_ofSubsingleton_id
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : F [⋀^ι]→ₗ[𝕜] E
ε : ι → ℝ
C : ℝ
c : ι → 𝕜
hε : ∀ (i : ι), 0 < ε i
hc : ∀ (i : ι), 1 < ‖c i‖
hf :
  ∀ (m : ι → F),
    (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
      (∀ (i : ι), ‖m i‖ < ε i) → norm.{wE} (E := E) ((f : (a : ι → F) → E) m : E) ≤ C * ∏ i : ι, ‖m i‖
m : ι → F
⊢ norm.{wE} (E := E) ((f : (a : ι → F) → E) m : E) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
f.1.bound_of_shell hε hc hf m

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.bound_of_shell
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Curry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
f : E [⋀^Fin (n + 1)]→L[𝕜] F
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (toContinuousMultilinearMap ((f.curryLeft : (a : E) → E [⋀^Fin n]→L[𝕜] F) x))
    ((f.curryLeft (Ei := fun (x : Fin (n + 1)) ↦ E) : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) x)

Tactic:
rfl

Premises used: MultilinearMap.mkContinuous, rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Curry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
f : E [⋀^Fin (n + 1)]→L[𝕜] F
x : E
⊢ Eq (α := E [⋀^Fin n]→ₗ[𝕜] F) (toAlternatingMap ((f.curryLeft : (a : E) → E [⋀^Fin n]→L[𝕜] F) x))
    ((f.toAlternatingMap.curryLeft : (a : E) → E [⋀^Fin n]→ₗ[𝕜] F) x)

Tactic:
rfl

Premises used: rfl