-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem IsVonNBounded.image {σ : 𝕜₁ →+* 𝕜₂} [RingHomSurjective σ] [RingHomIsometric σ] {s : Set E}
    (hs : IsVonNBounded 𝕜₁ s) (f : E →SL[σ] F) : IsVonNBounded 𝕜₂ (f '' s)

Proof state:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
f : E →SL[σ] F
σ_iso : Isometry ⇑σ
this : map (⇑σ) (𝓝 0) = 𝓝 0
hf₀ : Tendsto (⇑f) (𝓝 0) (𝓝 0)
hs : Tendsto (fun x => x • s) (𝓝 0) (𝓝 0).smallSets
⊢ Tendsto ((fun x => x • ⇑f '' s) ∘ ⇑σ) (𝓝 0) (𝓝 0).smallSets

Tactic:
simpa only [comp_def, image_smul_setₛₗ _ _ σ f] using hf₀.image_smallSets.comp hs

Result:
no goals

Proof state:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ_iso : Isometry ⇑σ
this : map (⇑σ) (𝓝 0) = 𝓝 0
⊢ IsVonNBounded 𝕜₂ (⇑f '' s)

Tactic:
have hf₀ : Tendsto f (𝓝 0) (𝓝 0) := f.continuous.tendsto' 0 0 (map_zero f)

Result:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ_iso : Isometry ⇑σ
this : map (⇑σ) (𝓝 0) = 𝓝 0
hf₀ : Tendsto (⇑f) (𝓝 0) (𝓝 0)
⊢ IsVonNBounded 𝕜₂ (⇑f '' s)

Proof state:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ_iso : Isometry ⇑σ
this : map (⇑σ) (𝓝 0) = 𝓝 0
hf₀ : Tendsto (⇑f) (𝓝 0) (𝓝 0)
⊢ IsVonNBounded 𝕜₂ (⇑f '' s)

Tactic:
simp only [isVonNBounded_iff_tendsto_smallSets_nhds, ← this, tendsto_map'_iff] at hs ⊢

Result:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
f : E →SL[σ] F
σ_iso : Isometry ⇑σ
this : map (⇑σ) (𝓝 0) = 𝓝 0
hf₀ : Tendsto (⇑f) (𝓝 0) (𝓝 0)
hs : Tendsto (fun x => x • s) (𝓝 0) (𝓝 0).smallSets
⊢ Tendsto ((fun x => x • ⇑f '' s) ∘ ⇑σ) (𝓝 0) (𝓝 0).smallSets

Proof state:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ_iso : Isometry ⇑σ
⊢ map (⇑σ) (𝓝 0) = 𝓝 0

Tactic:
rw [σ_iso.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]

Result:
no goals

Proof state:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ_iso : Isometry ⇑σ
⊢ IsVonNBounded 𝕜₂ (⇑f '' s)

Tactic:
have : map σ (𝓝 0) = 𝓝 0 := by
  rw [σ_iso.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]

Result:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ_iso : Isometry ⇑σ
this : map (⇑σ) (𝓝 0) = 𝓝 0
⊢ IsVonNBounded 𝕜₂ (⇑f '' s)

Proof state:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
⊢ IsVonNBounded 𝕜₂ (⇑f '' s)

Tactic:
have σ_iso : Isometry σ := AddMonoidHomClass.isometry_of_norm σ fun x => RingHomIsometric.is_iso

Result:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ_iso : Isometry ⇑σ
⊢ IsVonNBounded 𝕜₂ (⇑f '' s)