-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_6, u_8} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
simp_rw :
  Tendsto (β := Set ((i : ι) → E i)) (fun (x : 𝕜) ↦ x • S) (𝓝 0) (smallSets (𝓝 0)) ↔
    ∀ (i : ι), Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ x • eval (β := E) i '' S) (𝓝 0) (smallSets (𝓝 0))
simp_rw₁ :
  Tendsto (β := Set ((i : ι) → E i)) (fun (x : 𝕜) ↦ x • S) (𝓝 0)
      (smallSets (Filter.pi (α := E) fun (i : ι) ↦ 𝓝 (0 i))) ↔
    ∀ (i : ι), Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ x • eval (β := E) i '' S) (𝓝 0) (smallSets (𝓝 0))
simp_rw₂ :
  Tendsto (β := Set ((i : ι) → E i)) (fun (x : 𝕜) ↦ x • S) (𝓝 0)
      (smallSets (⨅ (i : ι), comap (eval (β := E) i) (𝓝 (0 i)))) ↔
    ∀ (i : ι), Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ x • eval (β := E) i '' S) (𝓝 0) (smallSets (𝓝 0))
simp_rw₃ :
  Tendsto (β := Set ((i : ι) → E i)) (fun (x : 𝕜) ↦ x • S) (𝓝 0)
      (⨅ (i : ι), smallSets (comap (eval (β := E) i) (𝓝 (0 i)))) ↔
    ∀ (i : ι), Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ x • eval (β := E) i '' S) (𝓝 0) (smallSets (𝓝 0))
simp_rw₄ :
  Tendsto (β := Set ((i : ι) → E i)) (fun (x : 𝕜) ↦ x • S) (𝓝 0)
      (⨅ (i : ι), comap (image (eval (β := E) i)) (smallSets (𝓝 (0 i)))) ↔
    ∀ (i : ι), Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ x • eval (β := E) i '' S) (𝓝 0) (smallSets (𝓝 0))
simp_rw₅ :
  (∀ (i : ι),
      Tendsto (β := Set ((i : ι) → E i)) (fun (x : 𝕜) ↦ x • S) (𝓝 0)
        (comap (image (eval (β := E) i)) (smallSets (𝓝 (0 i))))) ↔
    ∀ (i : ι), Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ x • eval (β := E) i '' S) (𝓝 0) (smallSets (𝓝 0))
simp_rw₆ :
  (∀ (i : ι),
      Tendsto.{u_6, u_8} (α := 𝕜) (β := Set (E i)) (image (eval (β := E) i) ∘ fun (x : 𝕜) ↦ x • S) (𝓝 0)
        (smallSets (𝓝 (0 i)))) ↔
    ∀ (i : ι), Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ x • eval (β := E) i '' S) (𝓝 0) (smallSets (𝓝 0))
simp_rw₇ :
  (∀ (i : ι),
      Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ eval (β := E) i '' (x • S)) (𝓝 0) (smallSets (𝓝 (0 i)))) ↔
    ∀ (i : ι), Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ x • eval (β := E) i '' S) (𝓝 0) (smallSets (𝓝 0))
simp_rw₈ :
  (∀ (i : ι),
      Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ eval (β := E) i '' (fun (x_1 : (i : ι) → E i) ↦ x • x_1) '' S)
        (𝓝 0) (smallSets (𝓝 (0 i)))) ↔
    ∀ (i : ι),
      Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ (fun (x_1 : E i) ↦ x • x_1) '' eval (β := E) i '' S) (𝓝 0)
        (smallSets (𝓝 0))
simp_rw₉ :
  (∀ (i : ι),
      Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ (fun (x_1 : (i : ι) → E i) ↦ eval (β := E) i (x • x_1)) '' S)
        (𝓝 0) (smallSets (𝓝 (0 i)))) ↔
    ∀ (i : ι),
      Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ (fun (x_1 : (x : ι) → E x) ↦ x • eval (β := E) i x_1) '' S)
        (𝓝 0) (smallSets (𝓝 0))
simp_rw₁₀ :
  (∀ (i : ι),
      Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ (fun (a : (i : ι) → E i) ↦ (x • a) i) '' S) (𝓝 0)
        (smallSets (𝓝 (0 i)))) ↔
    ∀ (i : ι),
      Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ (fun (a : (x : ι) → E x) ↦ x • a i) '' S) (𝓝 0)
        (smallSets (𝓝 0))
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' S)
have simp_rw₁₁ : (∀ (i : ι),
    Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ (fun (a : (i : ι) → E i) ↦ x • a i) '' S) (𝓝 0)
      (smallSets (𝓝 (0 i)))) ↔
  ∀ (i : ι),
    Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ (fun (a : (x : ι) → E x) ↦ x • a i) '' S) (𝓝 0) (smallSets (𝓝 0))
Tactic: simp_rw [isVonNBounded_iff_tendsto_smallSets_nhds, nhds_pi, Filter.pi, smallSets_iInf,
    smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff, Function.comp_def,
    ← image_smul, image_image, eval, Pi.smul_apply, Pi.zero_apply]