awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (hypothesis)
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 : MultilinearMap 𝕜 E G
C : ℝ
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
D : ℝ := max C 1
⊢ Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
have D_pos : 0 ≤ D
Tactic: have D_pos : 0 ≤ D := le_trans zero_le_one (le_max_right _ _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (hypothesis)
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 : MultilinearMap 𝕜 E G
C : ℝ
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
D : ℝ := max C 1
D_pos : 0 ≤ D
⊢ Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
have H₁ : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ D * ∏ i : ι, ‖m i‖
Tactic: replace H (m) : ‖f m‖ ≤ D * ∏ i, ‖m i‖ :=
    (H m).trans (mul_le_mul_of_nonneg_right (le_max_left _ _) <| by positivity)
Cleared hypotheses: H
-- 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 : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ D * ∏ i : ι, ‖m i‖
⊢ Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
have refine : ∀ (m : (i : ι) → E i), ContinuousAt (Y := G) (⇑f : (a : (i : ι) → E i) → G) m
Tactic: refine continuous_iff_continuousAt.2 fun 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 : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ D * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
⊢ ContinuousAt (Y := G) (⇑f : (a : (i : ι) → E i) → G) m
have continuousAt_of_locally_lipschitz : ∀ (m' : (i : ι) → E i) (h' : dist m' m < 1),
  dist.{wG} (α := G) ((f : (a : (i : ι) → E i) → G) m' : G) ((f : (a : (i : ι) → E i) → G) m : G) ≤
    D * (↑(Fintype.card ι) : ℝ) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * dist m' m
Tactic: refine
    continuousAt_of_locally_lipschitz zero_lt_one
      (D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1)) fun m' h' => ?_
-- 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 : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ D * ∏ i : ι, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
⊢ dist.{wG} (α := G) ((f : (a : (i : ι) → E i) → G) m' : G) ((f : (a : (i : ι) → E i) → G) m : G) ≤
    D * (↑(Fintype.card ι) : ℝ) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * dist m' m
have rw : ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m' : G) ((f : (a : (i : ι) → E i) → G) m : G)‖ ≤
  D * (↑(Fintype.card ι) : ℝ) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖
Tactic: rw [dist_eq_norm, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (hypothesis)
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 : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ D * ∏ i : ι, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
⊢ ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m' : G) ((f : (a : (i : ι) → E i) → G) m : G)‖ ≤
    D * (↑(Fintype.card ι) : ℝ) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖
have this : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1
Tactic: have : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1 := by
    simp [zero_le_one, norm_le_of_mem_closedBall (le_of_lt h')]
-- 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 : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ D * ∏ i : ι, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
this : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1
⊢ D * (↑(Fintype.card ι) : ℝ) * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ ≤
    D * (↑(Fintype.card ι) : ℝ) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖
have ha : 0 ≤ ‖m' - m‖
Tactic: gcongr
-- 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 : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ D * ∏ i : ι, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
this : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1
ha : 0 ≤ ‖m' - m‖
⊢ D * (↑(Fintype.card ι) : ℝ) * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ ≤
    D * (↑(Fintype.card ι) : ℝ) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖
have hbc : 0 ≤ D * (↑(Fintype.card ι) : ℝ)
Tactic: gcongr
-- 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 : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ D * ∏ i : ι, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
this : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1
ha : 0 ≤ ‖m' - m‖
hbc : 0 ≤ D * (↑(Fintype.card ι) : ℝ)
⊢ D * (↑(Fintype.card ι) : ℝ) * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ ≤
    D * (↑(Fintype.card ι) : ℝ) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖
have hbc₁ : 0 ≤ max ‖m'‖ ‖m‖
Tactic: gcongr
-- 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 : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ D * ∏ i : ι, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
this : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1
⊢ ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m' : G) ((f : (a : (i : ι) → E i) → G) m : G)‖ ≤
    D * (↑(Fintype.card ι) : ℝ) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖
have m'₁ : D * (↑(Fintype.card ι) : ℝ) * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ ≤
  D * (↑(Fintype.card ι) : ℝ) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖
Tactic: calc
    ‖f m' - f m‖ ≤ D * Fintype.card ι * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ :=
      f.norm_image_sub_le_of_bound D_pos H m' m
    _ ≤ D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖ := by gcongr
-- 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 : MultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (x : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : (i : Fin n) → G), norm.{wG'} (E := G') ((f : (a : (i : Fin n) → G) → G') m : G') ≤ C * ∏ i : Fin n, ‖m i‖
v : Fin k → G
⊢ norm.{wG'} (E := G') ((f.restr s hk z : (a : (i : Fin k) → G) → G') v : G') ≤ C * ‖z‖ ^ (n - k) * ∏ i : Fin k, ‖v i‖
have rw : norm.{wG'} (E := G') ((f.restr s hk z : (a : (i : Fin k) → G) → G') v : G') ≤ C * ((∏ i : Fin k, ‖v i‖) * ‖z‖ ^ (n - k))
Tactic: rw [mul_right_comm, mul_assoc]
-- 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 : MultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (x : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : (i : Fin n) → G), norm.{wG'} (E := G') ((f : (a : (i : Fin n) → G) → G') m : G') ≤ C * ∏ i : Fin n, ‖m i‖
v : Fin k → G
⊢ norm.{wG'} (E := G') ((f.restr s hk z : (a : (i : Fin k) → G) → G') v : G') ≤
    C * ((∏ i : Fin k, ‖v i‖) * ‖z‖ ^ (n - k))
have h : (∏ i : Fin k, ‖v i‖) * ‖z‖ ^ (n - k) =
  ∏ i : Fin n,
    norm.{wG} (E := G)
      (if h : i ∈ s then
        v ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) i h))
      else z)
Tactic: convert! H _ using 2
-- 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 : MultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (x : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : (i : Fin n) → G), norm.{wG'} (E := G') ((f : (a : (i : Fin n) → G) → G') m : G') ≤ C * ∏ i : Fin n, ‖m i‖
v : Fin k → G
⊢ (∏ i : Fin k, ‖v i‖) * ‖z‖ ^ (n - k) =
    ∏ i : Fin n,
      norm.{wG} (E := G)
        (if h : i ∈ s then
          v ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) i h))
        else z)
have h : (∏ i : ↥s, ‖v ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) i)‖) * ‖z‖ ^ (n - k) =
  (∏ a : ↥s,
      ‖v
          ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k)
            (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) (↑a : Fin n) sorry))‖) *
    ‖z‖ ^ (n - k)
Tactic: simp only [apply_dite norm, Fintype.prod_dite, prod_const ‖z‖, Finset.card_univ,
    Fintype.card_of_subtype sᶜ fun _ => mem_compl, card_compl, Fintype.card_fin, hk, ←
    (s.orderIsoOfFin hk).symm.bijective.prod_comp fun x => ‖v x‖]
-- 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 G
⊢ IsLeast
    {c : ℝ |
      0 ≤ c ∧ ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ c * ∏ i : ι, ‖m i‖}
    ‖f‖
have refine : IsClosed (X := ℝ)
  {c : ℝ |
    0 ≤ c ∧ ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ c * ∏ i : ι, ‖m i‖}
Tactic: refine IsClosed.isLeast_csInf ?_ bounds_nonempty bounds_bddBelow
-- 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 G
⊢ IsClosed (X := ℝ)
    {c : ℝ |
      0 ≤ c ∧ ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ c * ∏ i : ι, ‖m i‖}
have simp : IsClosed (X := ℝ)
  ({a : ℝ | 0 ≤ a} ∩
    ⋂ (i : (i : ι) → E i),
      {x : ℝ | Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) i : G) ≤ x * ∏ i_1 : ι, ‖i i_1‖})
Tactic: simp only [Set.setOf_and, Set.setOf_forall]
-- 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 G
m : (i : ι) → E i
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
⊢ ‖f‖ * ∏ i : ι, ‖m i‖ ≤ C * ∏ i : ι, b i
have b0 : 0 ≤ C
Tactic: gcongr
-- 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 G
m : (i : ι) → E i
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
b0 : 0 ≤ C
⊢ ‖f‖ * ∏ i : ι, ‖m i‖ ≤ C * ∏ i : ι, b i
have h₂ : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → ‖m i‖ ≤ b i
Tactic: gcongr
-- 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 g : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ Norm.norm.{wG} (E := G) ((f + g : (a : (i : ι) → E i) → G) x : G) ≤ (‖f‖ + ‖g‖) * ∏ i : ι, ‖x i‖
have rw : Norm.norm.{wG} (E := G) ((f + g : (a : (i : ι) → E i) → G) x : G) ≤ ‖f‖ * ∏ i : ι, ‖x i‖ + ‖g‖ * ∏ i : ι, ‖x i‖
Tactic: rw [add_mul]
-- 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 ι
𝕜' : Type u_1
inst_6 : SeminormedRing 𝕜'
inst_7 : Module 𝕜' G
inst_8 : IsBoundedSMul 𝕜' G
inst_9 : SMulCommClass 𝕜 𝕜' G
c : 𝕜'
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ Norm.norm.{wG} (E := G) ((c • f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
have grw : ‖HSMul.hSMul (β := G) c ((f : (a : (i : ι) → E i) → G) m : G)‖ ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
Tactic: grw [smul_apply, norm_smul_le, mul_assoc, le_opNorm]
-- 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 ι
𝕜' : Type u_1
inst_6 : SeminormedRing 𝕜'
inst_7 : Module 𝕜' G
inst_8 : IsBoundedSMul 𝕜' G
inst_9 : SMulCommClass 𝕜 𝕜' G
c : 𝕜'
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
grw : ‖HSMul.hSMul (β := G) c ((f : (a : (i : ι) → E i) → G) m : G)‖ ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
⊢ Norm.norm.{wG} (E := G) ((c • f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
have grw₁ : ‖c‖ * Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
Tactic: grw [smul_apply, norm_smul_le, mul_assoc, le_opNorm]
-- 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 ι
𝕜' : Type u_1
inst_6 : SeminormedRing 𝕜'
inst_7 : Module 𝕜' G
inst_8 : IsBoundedSMul 𝕜' G
inst_9 : SMulCommClass 𝕜 𝕜' G
c : 𝕜'
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
grw : ‖HSMul.hSMul (β := G) c ((f : (a : (i : ι) → E i) → G) m : G)‖ ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
grw₁ : ‖c‖ * Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
⊢ Norm.norm.{wG} (E := G) ((c • f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
have grw₂ : ‖c‖ * Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * (‖f‖ * ∏ i : ι, ‖m i‖)
Tactic: grw [smul_apply, norm_smul_le, mul_assoc, le_opNorm]
-- 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 ι
𝕜' : Type u_1
inst_6 : SeminormedRing 𝕜'
inst_7 : Module 𝕜' G
inst_8 : IsBoundedSMul 𝕜' G
inst_9 : SMulCommClass 𝕜 𝕜' G
c : 𝕜'
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
grw : ‖HSMul.hSMul (β := G) c ((f : (a : (i : ι) → E i) → G) m : G)‖ ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
grw₁ : ‖c‖ * Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
grw₂ : ‖c‖ * Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * (‖f‖ * ∏ i : ι, ‖m i‖)
⊢ Norm.norm.{wG} (E := G) ((c • f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
have grw₃ : ‖c‖ * (‖f‖ * ∏ i : ι, ‖m i‖) ≤ ‖c‖ * (‖f‖ * ∏ i : ι, ‖m i‖)
Tactic: grw [smul_apply, norm_smul_le, mul_assoc, le_opNorm]
-- 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 G × ContinuousMultilinearMap 𝕜 E G
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
have rw : ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖
Tactic: rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- 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 G × ContinuousMultilinearMap 𝕜 E G
rw : ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
have rw₁ : ‖- -f.1 + -f.2‖ = ‖f.1 - f.2‖
Tactic: rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- 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 G × ContinuousMultilinearMap 𝕜 E G
rw : ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖
rw₁ : ‖- -f.1 + -f.2‖ = ‖f.1 - f.2‖
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
have rw₂ : ‖f.1 + -f.2‖ = ‖f.1 - f.2‖
Tactic: rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- 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 G × ContinuousMultilinearMap 𝕜 E G
rw : ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖
rw₁ : ‖- -f.1 + -f.2‖ = ‖f.1 - f.2‖
rw₂ : ‖f.1 + -f.2‖ = ‖f.1 - f.2‖
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
have rw₃ : ‖f.1 + -f.2‖ = ‖f.1 + -f.2‖
Tactic: rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (hypothesis)
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 ι
⊢ Eq (α := Filter (ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G))
    (𝓤 (ContinuousMultilinearMap 𝕜 E G))
    (⨅ (r : ℝ),
      ⨅ (_ : r > 0), 𝓟 {f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G | ‖-f.1 + f.2‖ < r})
have A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
Tactic: have A (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G) :
      ‖-f.1 + f.2‖ = ‖f.1 - f.2‖ := by rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
⊢ Eq (α := Filter (ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G))
    (𝓤 (ContinuousMultilinearMap 𝕜 E G))
    (⨅ (r : ℝ),
      ⨅ (_ : r > 0), 𝓟 {f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G | ‖-f.1 + f.2‖ < r})
have simp : Eq (α := Filter (ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G)) (𝓤 (ContinuousMultilinearMap 𝕜 E G))
  (⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G | ‖f.1 - f.2‖ < r})
Tactic: simp only [A]
-- 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
⊢ Eq (α := Filter (ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G))
    (𝓤 (ContinuousMultilinearMap 𝕜 E G))
    (⨅ (r : ℝ),
      ⨅ (_ : r > 0), 𝓟 {f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G | ‖f.1 - f.2‖ < r})
have refine_1 : ∃ (r : ℝ),
  Membership.mem (γ := Filter (ContinuousMultilinearMap 𝕜 E G)) (𝓝 0)
    (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)
Tactic: refine (ContinuousMultilinearMap.seminorm 𝕜 E G).uniformity_eq_of_hasBasis
    (ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis Metric.nhds_basis_closedBall)
    ?_ fun (s, r) ⟨hs, hr⟩ ↦ ?_