awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
if : ∀ (h₁ : ∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
if₁ : ∀ (h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
if₂ : ∀ (h₁ : ∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
if₃ if₄ : ∀ (h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)

Tactic:
classical
  if h₁ : ∀ c : 𝕜, ‖c‖ ≤ 1 then
    exact absorbs_iff_norm.2 ⟨2, fun c hc ↦ by linarith [h₁ c]⟩
  else
    let _ : NontriviallyNormedField 𝕜 := ⟨by simpa using h₁⟩
    obtain ⟨I, t, ht₀, hft⟩ :
        ∃ (I : Finset ι) (t : ∀ i, Set (E i)), (∀ i, t i ∈ 𝓝 0) ∧ Set.pi I t ⊆ f ⁻¹' V := by
      have hfV : f ⁻¹' V ∈ 𝓝 0 := (map_continuous f).tendsto' _ _ f.map_zero hV
      rwa [nhds_pi, Filter.mem_pi, exists_finite_iff_finset] at hfV
    have : ∀ i, ∃ c : 𝕜, c ≠ 0 ∧ ∀ c' : 𝕜, ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i := fun i ↦ by
      rw [isVonNBounded_pi_iff] at hs
      have := (hs i).tendsto_smallSets_nhds.eventually (mem_lift' (ht₀ i))
      rcases NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff.1 this with ⟨r, hr₀, hr⟩
      rcases NormedField.exists_norm_lt 𝕜 hr₀ with ⟨c, hc₀, hc⟩
      refine ⟨c, norm_pos_iff.1 hc₀, fun c' hle x hx ↦ ?_⟩
      exact hr (hle.trans_lt hc) ⟨_, ⟨x, hx, rfl⟩, rfl⟩
    choose c hc₀ hc using this
    rw [absorbs_iff_eventually_nhds_zero (mem_of_mem_nhds hV),
      NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff]
    have hc₀' : ∏ i ∈ I, c i ≠ 0 := Finset.prod_ne_zero_iff.2 fun i _ ↦ hc₀ i
    refine ⟨‖∏ i ∈ I, c i‖, norm_pos_iff.2 hc₀', fun a ha ↦ mapsTo_image_iff.2 fun x hx ↦ ?_⟩
    let ⟨i₀⟩ := ‹Nonempty ι›
    set y := I.piecewise (fun i ↦ c i • x i) x
    calc
      f (update y i₀ ((a / ∏ i ∈ I, c i) • y i₀)) ∈ V := hft fun i hi => by
        rcases eq_or_ne i i₀ with rfl | hne
        · simp_rw [update_self, y, I.piecewise_eq_of_mem _ _ hi, smul_smul]
          refine hc _ _ ?_ _ hx
          calc
            ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ (‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖) * ‖c i‖ := by
              rw [norm_mul, norm_div]; gcongr; exact ha.out.le
            _ ≤ 1 * ‖c i‖ := by gcongr; apply div_self_le_one
            _ = ‖c i‖ := one_mul _
        · simp_rw [update_of_ne hne, y, I.piecewise_eq_of_mem _ _ hi]
          exact hc _ _ le_rfl _ hx
      _ = a • f x := by
        rw [f.map_update_smul, update_eq_self, f.map_piecewise_smul, div_eq_mul_inv, mul_smul,
          inv_smul_smul₀ hc₀']

Premises used: Iff.mpr, Finset, mem_of_mem_nhds, absorbs_iff_norm, Exists.intro, Filter.HasBasis.eventually_iff, absorbs_iff_eventually_nhds_zero, NormedAddGroup.nhds_zero_basis_norm_lt, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : ContinuousSMul 𝕜 F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
h : IsEmpty ι
⊢ IsVonNBounded.{u_2, u_3} 𝕜 (E := F) ((⇑f : (a : (i : ι) → E i) → F) '' s)

Tactic:
(isBounded_iff_isVonNBounded _).1 <|
      @Set.Finite.isBounded _ (vonNBornology 𝕜 F) _ (s.toFinite.image _)

Premises used: Set.Finite.image, Bornology.isBounded_iff_isVonNBounded, Set.Finite.isBounded, Set.toFinite, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : ContinuousSMul 𝕜 F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
h : IsEmpty ι
⊢ IsVonNBounded.{u_2, u_3} 𝕜 (E := F) ((⇑f : (a : (i : ι) → E i) → F) '' s)

Tactic:
exact (isBounded_iff_isVonNBounded _).1 <|
      @Set.Finite.isBounded _ (vonNBornology 𝕜 F) _ (s.toFinite.image _)

Premises used: Set.Finite.image, Bornology.isBounded_iff_isVonNBounded, Set.Finite.isBounded, Set.toFinite, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : ContinuousSMul 𝕜 F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
h : Nonempty ι
⊢ IsVonNBounded.{u_2, u_3} 𝕜 (E := F) ((⇑f : (a : (i : ι) → E i) → F) '' s)

Tactic:
hs.image_multilinear' f

Premises used: Bornology.IsVonNBounded.image_multilinear'
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : ContinuousSMul 𝕜 F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
h : Nonempty ι
⊢ IsVonNBounded.{u_2, u_3} 𝕜 (E := F) ((⇑f : (a : (i : ι) → E i) → F) '' s)

Tactic:
exact hs.image_multilinear' f

Premises used: Bornology.IsVonNBounded.image_multilinear'
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : ContinuousSMul 𝕜 F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
⊢ IsEmpty ι ∨ Nonempty ι

Tactic:
cases isEmpty_or_nonempty ι with
  | inl h =>
    exact (isBounded_iff_isVonNBounded _).1 <|
      @Set.Finite.isBounded _ (vonNBornology 𝕜 F) _ (s.toFinite.image _)
  | inr h => exact hs.image_multilinear' f

Premises used: isEmpty_or_nonempty, Bornology.isBounded_iff_isVonNBounded, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : DecidableEq ι
inst_7 : TopologicalSpace F
f : ContinuousMultilinearMap 𝕜 E F
⊢ Membership.mem (γ := Set (((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F))
    {f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
      Continuous[Pi.topologicalSpace, inst_7]
          ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f) ∧
        (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
            (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                  (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                f (update (β := E) m i (x + y)) =
              HAdd.hAdd (α := F) (β := F)
                ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                      (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                    f (update (β := E) m i x) :
                  F)
                ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                      (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                    f (update (β := E) m i y) :
                  F)) ∧
          ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
            (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                  (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                f (update (β := E) m i (c • x)) =
              HSMul.hSMul (β := F) c
                ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                      (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                    f (update (β := E) m i x) :
                  F)}
    (f.toUniformOnFun (E := E))

Tactic:
⟨f.cont, f.map_update_add, f.map_update_smul⟩

Premises used: Set.Mem, setOf, ContinuousMultilinearMap.map_update_add, ContinuousMultilinearMap.cont, And.intro, ContinuousMultilinearMap.map_update_smul
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : DecidableEq ι
inst_7 : TopologicalSpace F
f : ContinuousMultilinearMap 𝕜 E F
⊢ Membership.mem (γ := Set (((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F))
    {f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
      Continuous[Pi.topologicalSpace, inst_7]
          ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f) ∧
        (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
            (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                  (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                f (update (β := E) m i (x + y)) =
              HAdd.hAdd (α := F) (β := F)
                ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                      (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                    f (update (β := E) m i x) :
                  F)
                ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                      (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                    f (update (β := E) m i y) :
                  F)) ∧
          ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
            (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                  (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                f (update (β := E) m i (c • x)) =
              HSMul.hSMul (β := F) c
                ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                      (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                    f (update (β := E) m i x) :
                  F)}
    (f.toUniformOnFun (E := E))

Tactic:
exact ⟨f.cont, f.map_update_add, f.map_update_smul⟩
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : DecidableEq ι
inst_7 : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F
hcont :
  Continuous[Pi.topologicalSpace, inst_7]
    ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
      f)
hadd :
  ∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (x + y)) =
      HAdd.hAdd (α := F) (β := F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i y) :
          F)
hsmul :
  ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (c • x)) =
      HSMul.hSMul (β := F) c
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)
inst_8 : DecidableEq ι
⊢ ∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (x + y)) =
      HAdd.hAdd (α := F) (β := F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i y) :
          F)

Tactic:
hadd
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : DecidableEq ι
inst_7 : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F
hcont :
  Continuous[Pi.topologicalSpace, inst_7]
    ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
      f)
hadd :
  ∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (x + y)) =
      HAdd.hAdd (α := F) (β := F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i y) :
          F)
hsmul :
  ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (c • x)) =
      HSMul.hSMul (β := F) c
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)
inst_8 : DecidableEq ι
⊢ ∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
    f (update (β := E) m i (x + y)) = f (update (β := E) m i x) + f (update (β := E) m i y)

Tactic:
convert! hadd
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : DecidableEq ι
inst_7 : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F
hcont :
  Continuous[Pi.topologicalSpace, inst_7]
    ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
      f)
hadd :
  ∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (x + y)) =
      HAdd.hAdd (α := F) (β := F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i y) :
          F)
hsmul :
  ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (c • x)) =
      HSMul.hSMul (β := F) c
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)
inst_8 : DecidableEq ι
⊢ ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (c • x)) =
      HSMul.hSMul (β := F) c
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)

Tactic:
hsmul
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : DecidableEq ι
inst_7 : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F
hcont :
  Continuous[Pi.topologicalSpace, inst_7]
    ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
      f)
hadd :
  ∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (x + y)) =
      HAdd.hAdd (α := F) (β := F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i y) :
          F)
hsmul :
  ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (c • x)) =
      HSMul.hSMul (β := F) c
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)
inst_8 : DecidableEq ι
⊢ ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i), f (update (β := E) m i (c • x)) = c • f (update (β := E) m i x)

Tactic:
convert! hsmul
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : DecidableEq ι
inst_7 : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F
hcont :
  Continuous[Pi.topologicalSpace, inst_7]
    ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
      f)
hadd :
  ∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (x + y)) =
      HAdd.hAdd (α := F) (β := F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i y) :
          F)
hsmul :
  ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
    (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        f (update (β := E) m i (c • x)) =
      HSMul.hSMul (β := F) c
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f (update (β := E) m i x) :
          F)
⊢ Membership.mem (γ := Set (((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F))
    (range (ι := ContinuousMultilinearMap 𝕜 E F) (toUniformOnFun (E := E))) f

Tactic:
exact ⟨⟨⟨f, by intro; convert! hadd, by intro; convert! hsmul⟩, hcont⟩, rfl⟩
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : ContinuousMultilinearMap 𝕜 E F
⊢ Eq (α := ((i : ι) → E i) → F)
    ((UniformOnFun.toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
        (f.toUniformOnFun (E := E)) :
      ((i : ι) → E i) → F)
    ((⇑f : (a : (i : ι) → E i) → F) : (a : (i : ι) → E i) → F)

Tactic:
rfl

Premises used: ContinuousMultilinearMap.toUniformOnFun, rfl