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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
refine_1 :
  ∃ (r : ℝ),
    Membership.mem (γ := Filter (ContinuousMultilinearMap 𝕜 E G)) (𝓝 0)
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)
⊢ 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_2 : ∀ (x : Set ((i : ι) → E i) × ℝ) (s : Set ((i : ι) → E i)) (r : ℝ),
  Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2 →
    ∀ (hs : Bornology.IsVonNBounded 𝕜 (s, r).1) (hr : 0 < (s, r).2),
      ∃ r_1 > 0,
        Subset (α := Set (ContinuousMultilinearMap 𝕜 E G))
          (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
          {f : ContinuousMultilinearMap 𝕜 E G |
            Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}
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⟩ ↦ ?_
-- 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‖
⊢ ∃ (r : ℝ),
    Membership.mem (γ := Filter (ContinuousMultilinearMap 𝕜 E G)) (𝓝 0)
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)
have refine_1 : ∀ (c : 𝕜) (hc : 1 < ‖c‖),
  ∃ (r : ℝ),
    Membership.mem (γ := Filter (ContinuousMultilinearMap 𝕜 E G)) (𝓝 0)
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)
Tactic: rcases NormedField.exists_lt_norm 𝕜 1 with ⟨c, hc⟩
-- 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ (r : ℝ),
    Membership.mem (γ := Filter (ContinuousMultilinearMap 𝕜 E G)) (𝓝 0)
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)
have hc₀ : 0 < ‖c‖
Tactic: have hc₀ : 0 < ‖c‖ := one_pos.trans hc
-- 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‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
⊢ ∃ (r : ℝ),
    Membership.mem (γ := Filter (ContinuousMultilinearMap 𝕜 E G)) (𝓝 0)
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)
have refine_1 : ∃ (r : ℝ) (a : Set ((i : ι) → E i)) (b : Set G),
  (Bornology.IsVonNBounded 𝕜 a ∧ Membership.mem (γ := Filter G) (𝓝 0) b) ∧
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G))
      {f : ContinuousMultilinearMap 𝕜 E G | Set.MapsTo (⇑f : (a : (i : ι) → E i) → G) a b}
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)
Tactic: simp only [hasBasis_nhds_zero.mem_iff, Prod.exists]
-- 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‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
⊢ ∃ (r : ℝ) (a : Set ((i : ι) → E i)) (b : Set G),
    (Bornology.IsVonNBounded 𝕜 a ∧ Membership.mem (γ := Filter G) (𝓝 0) b) ∧
      Subset (α := Set (ContinuousMultilinearMap 𝕜 E G))
        {f : ContinuousMultilinearMap 𝕜 E G | Set.MapsTo (⇑f : (a : (i : ι) → E i) → G) a b}
        (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)
have h : (Bornology.IsVonNBounded 𝕜 (E := (i : ι) → E i) (closedBall 0 ‖c‖) ∧
    Membership.mem (γ := Filter G) (𝓝 0) (closedBall 0 1)) ∧
  Subset (α := Set (ContinuousMultilinearMap 𝕜 E G))
    {f : ContinuousMultilinearMap 𝕜 E G |
      Set.MapsTo (α := (i : ι) → E i) (β := G) (⇑f : (a : (i : ι) → E i) → G) (closedBall 0 ‖c‖) (closedBall 0 1)}
    (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 1)
Tactic: use 1, closedBall 0 ‖c‖, closedBall 0 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
⊢ (Bornology.IsVonNBounded 𝕜 (E := (i : ι) → E i) (closedBall 0 ‖c‖) ∧
      Membership.mem (γ := Filter G) (𝓝 0) (closedBall 0 1)) ∧
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G))
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (α := (i : ι) → E i) (β := G) (⇑f : (a : (i : ι) → E i) → G) (closedBall 0 ‖c‖) (closedBall 0 1)}
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 1)
have h : ∀ (f : ContinuousMultilinearMap 𝕜 E G),
  (∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1) → ‖f‖ ≤ 1
Tactic: suffices ∀ f : ContinuousMultilinearMap 𝕜 E G, (∀ x, ‖x‖ ≤ ‖c‖ → ‖f x‖ ≤ 1) → ‖f‖ ≤ 1 by
      simpa [NormedSpace.isVonNBounded_closedBall, closedBall_mem_nhds, Set.subset_def, Set.MapsTo]
-- 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‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
⊢ ‖f‖ ≤ 1
have h : ∀ (x : (i : ι) → E i) (hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖) (hx : ∀ (i : ι), ‖x i‖ < ‖c‖),
  Norm.norm.{wG} (E := G) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → G) x : G) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖x i‖)
Tactic: refine opNorm_le_bound (by positivity) <|
      f.1.bound_of_shell_of_continuous f.2 (fun _ ↦ hc₀) (fun _ ↦ hc) fun x hcx hx ↦ ?_
-- 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‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
⊢ LE.le (α := ℝ) (∏ i : ι, 1) (∏ i : ι, ‖x i‖)
have h1 : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → 1 ≤ ‖x i‖
Tactic: gcongr with i
-- 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‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
⊢ Norm.norm.{wG} (E := G) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → G) x : G) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖x i‖)
have hf₁ : Eq (α := ℝ) 1 (∏ i : ι, 1)
Tactic: calc
      ‖f x‖ ≤ 1 := hf _ <| (pi_norm_le_iff_of_nonneg (norm_nonneg c)).2 fun i ↦ (hx i).le
      _ = ∏ i : ι, 1 := by simp
      _ ≤ ∏ i, ‖x i‖ := by gcongr with i; simpa only [div_self hc₀.ne'] using hcx i
      _ = 1 * ∏ i, ‖x i‖ := (one_mul _).symm
-- 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‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
hf₁ : Eq (α := ℝ) 1 (∏ i : ι, 1)
⊢ Norm.norm.{wG} (E := G) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → G) x : G) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖x i‖)
have hf₂ : LE.le (α := ℝ) (∏ i : ι, 1) (∏ i : ι, ‖x i‖)
Tactic: calc
      ‖f x‖ ≤ 1 := hf _ <| (pi_norm_le_iff_of_nonneg (norm_nonneg c)).2 fun i ↦ (hx i).le
      _ = ∏ i : ι, 1 := by simp
      _ ≤ ∏ i, ‖x i‖ := by gcongr with i; simpa only [div_self hc₀.ne'] using hcx i
      _ = 1 * ∏ i, ‖x i‖ := (one_mul _).symm
-- 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‖
x : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
⊢ ∃ r_1 > 0,
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G)) (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}
have refine_2 : ∀ (ε : ℝ) (hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε),
  ∃ r_1 > 0,
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G)) (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}
Tactic: rcases (NormedSpace.isVonNBounded_iff' _).1 hs with ⟨ε, 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
⊢ ∃ r_1 > 0,
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G)) (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}
have refine_2 : ∀ (δ : ℝ) (hδ₀ : 0 < δ) (hδ : ε ^ Fintype.card ι * δ < (s, r).2),
  ∃ r_1 > 0,
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G)) (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}
Tactic: rcases exists_pos_mul_lt hr (ε ^ Fintype.card ι) with ⟨δ, hδ₀, 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
⊢ ∃ r_1 > 0,
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G)) (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}
have refine_2 : ∀ (f : ContinuousMultilinearMap 𝕜 E G)
  (hf :
    Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E G))
      (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 δ) f)
  (x : (i : ι) → E i) (hx : x ∈ (s, r).1),
  Membership.mem.{wG, wG} (α := G) (γ := Set G) (closedBall 0 (s, r).2) ((f : (a : (i : ι) → E i) → G) x : G)
Tactic: refine ⟨δ, hδ₀, fun f hf x hx ↦ ?_⟩
-- 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‖
x_1 : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
hf :
  Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E G))
    (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 δ) f
x : (i : ι) → E i
hx : x ∈ (s, r).1
⊢ Membership.mem.{wG, wG} (α := G) (γ := Set G) (closedBall 0 (s, r).2) ((f : (a : (i : ι) → E i) → G) x : G)
have refine_2 : ∀ (hf : (ContinuousMultilinearMap.seminorm 𝕜 E G : (a : ContinuousMultilinearMap 𝕜 E G) → ℝ) f < δ),
  Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ r
Tactic: simp only [Seminorm.mem_ball_zero, mem_closedBall_zero_iff] at hf ⊢
Cleared hypotheses: hf
-- 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hx : x ∈ (s, r).1
hf : (ContinuousMultilinearMap.seminorm 𝕜 E G : (a : ContinuousMultilinearMap 𝕜 E G) → ℝ) f < δ
⊢ Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ r
have hf₁ : ‖f‖ ≤ δ
Tactic: replace hf : ‖f‖ ≤ δ := hf.le
Cleared hypotheses: hf
-- 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hx : x ∈ (s, r).1
hf : ‖f‖ ≤ δ
⊢ Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ r
have hx₁ : ‖x‖ ≤ ε
Tactic: replace hx : ‖x‖ ≤ ε := hε x hx
Cleared hypotheses: hx
-- 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
⊢ ‖f‖ * ε ^ Fintype.card ι ≤ δ * ε ^ Fintype.card ι
have this : 0 ≤ ε
Tactic: have := (norm_nonneg x).trans hx
-- 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‖
x_1 : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
this : 0 ≤ ε
⊢ ‖f‖ * ε ^ Fintype.card ι ≤ δ * ε ^ Fintype.card ι
have ha : 0 ≤ ε ^ 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
⊢ Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ r
have ε₁ : ‖f‖ * ε ^ Fintype.card ι ≤ δ * ε ^ Fintype.card ι
Tactic: calc
      ‖f x‖ ≤ ‖f‖ * ε ^ Fintype.card ι := le_opNorm_mul_pow_card_of_le f hx
      _ ≤ δ * ε ^ Fintype.card ι := by have := (norm_nonneg x).trans hx; gcongr
      _ ≤ r := (mul_comm _ _).trans_le hδ.le
-- 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
⊢ (↑(nnnorm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G)) : ℝ) ≤ (↑(‖f‖₊ * ∏ i : ι, ‖m i‖₊) : ℝ)
have push_cast : Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖f‖ * ∏ x : ι, ‖m x‖
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : Fintype ι
inst_4 : Subsingleton ι
i : ι
⊢ Norm.norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) G)
      ((ofSubsingleton 𝕜 G G i : (a : G →L[𝕜] G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) G)
          (ContinuousLinearMap.id 𝕜 G) :
        ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) G) ≤
    1
have rw : Norm.norm (E := G →L[𝕜] G) (ContinuousLinearMap.id 𝕜 G) ≤ 1
Tactic: rw [norm_ofSubsingleton]
-- 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 : G
⊢ Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x) = ‖x‖
have a : Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x) ≤ ‖x‖
Tactic: apply 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 ι
inst_6 : IsEmpty ι
x : G
a : Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x) ≤ ‖x‖
⊢ Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x) = ‖x‖
have a₁ : ‖x‖ ≤ Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x)
Tactic: apply 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 ι
inst_6 : IsEmpty ι
x : G
⊢ Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x) ≤ ‖x‖
have a : ∀ (x_1 : (i : ι) → E i),
  Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x : (a : (i : ι) → E i) → G) x_1 : G) ≤ ‖x‖ * ∏ i : ι, ‖x_1 i‖
Tactic: refine opNorm_le_bound (norm_nonneg _) fun x => ?_