awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' S)
have 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))
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]
-- 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))
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' S)
have 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))
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]
-- 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))
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' S)
have 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))
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]
-- 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))
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' S)
have 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))
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]
-- 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))
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' S)
have 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))
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]
-- 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))
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' S)
have 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))
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]
-- 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))
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' S)
have 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))
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]
-- 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))
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' S)
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
⊢ Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)
have rw : Eq.{u_7 + 1} (α := Filter 𝕜₂) (𝓝[range.{u_7, u_6 + 1} (ι := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂)] (σ : (a : 𝕜₁) → 𝕜₂) 0 : Filter 𝕜₂)
  (𝓝 0 : Filter 𝕜₂)
Tactic: rw [σ.isometry.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
rw :
  Eq.{u_7 + 1} (α := Filter 𝕜₂)
    (𝓝[range.{u_7, u_6 + 1} (ι := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂)] (σ : (a : 𝕜₁) → 𝕜₂) 0 : Filter 𝕜₂) (𝓝 0 : Filter 𝕜₂)
⊢ Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)
have rw₁ : Eq.{u_7 + 1} (α := Filter 𝕜₂) (𝓝[univ] (σ : (a : 𝕜₁) → 𝕜₂) 0 : Filter 𝕜₂) (𝓝 0 : Filter 𝕜₂)
Tactic: rw [σ.isometry.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
rw :
  Eq.{u_7 + 1} (α := Filter 𝕜₂)
    (𝓝[range.{u_7, u_6 + 1} (ι := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂)] (σ : (a : 𝕜₁) → 𝕜₂) 0 : Filter 𝕜₂) (𝓝 0 : Filter 𝕜₂)
rw₁ : Eq.{u_7 + 1} (α := Filter 𝕜₂) (𝓝[univ] (σ : (a : 𝕜₁) → 𝕜₂) 0 : Filter 𝕜₂) (𝓝 0 : Filter 𝕜₂)
⊢ Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)
have rw₂ : Eq.{u_7 + 1} (α := Filter 𝕜₂) (𝓝 ((σ : (a : 𝕜₁) → 𝕜₂) 0) : Filter 𝕜₂) (𝓝 0 : Filter 𝕜₂)
Tactic: rw [σ.isometry.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
rw :
  Eq.{u_7 + 1} (α := Filter 𝕜₂)
    (𝓝[range.{u_7, u_6 + 1} (ι := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂)] (σ : (a : 𝕜₁) → 𝕜₂) 0 : Filter 𝕜₂) (𝓝 0 : Filter 𝕜₂)
rw₁ : Eq.{u_7 + 1} (α := Filter 𝕜₂) (𝓝[univ] (σ : (a : 𝕜₁) → 𝕜₂) 0 : Filter 𝕜₂) (𝓝 0 : Filter 𝕜₂)
rw₂ : Eq.{u_7 + 1} (α := Filter 𝕜₂) (𝓝 ((σ : (a : 𝕜₁) → 𝕜₂) 0) : Filter 𝕜₂) (𝓝 0 : Filter 𝕜₂)
⊢ Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)
have rw₃ : Eq.{u_7 + 1} (α := Filter 𝕜₂) (𝓝 0) (𝓝 0)
Tactic: rw [σ.isometry.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
⊢ IsVonNBounded.{u_7, u_4} 𝕜₂ (E := F) ((⇑f : (a : E) → F) '' s)
have this : Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)
Tactic: have : map σ (𝓝 0) = 𝓝 0 := by
    rw [σ.isometry.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
this : Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)
⊢ IsVonNBounded.{u_7, u_4} 𝕜₂ (E := F) ((⇑f : (a : E) → F) '' s)
have hf₀ : Tendsto.{u_3, u_4} (α := E) (β := F) (⇑f : (a : E) → F) (𝓝 0) (𝓝 0)
Tactic: have hf₀ : Tendsto f (𝓝 0) (𝓝 0) := f.continuous.tendsto' 0 0 (map_zero f)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
this : Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)
hf₀ : Tendsto.{u_3, u_4} (α := E) (β := F) (⇑f : (a : E) → F) (𝓝 0) (𝓝 0)
⊢ IsVonNBounded.{u_7, u_4} 𝕜₂ (E := F) ((⇑f : (a : E) → F) '' s)
have simp : ∀ (hs : Tendsto.{u_6, u_3} (β := Set E) (fun (x : 𝕜₁) ↦ x • s) (𝓝 0) (smallSets (𝓝 0))),
  Tendsto.{u_6, u_4} (α := 𝕜₁) (β := Set F)
    ((fun (x : 𝕜₂) ↦ HSMul.hSMul (β := Set F) x ((⇑f : (a : E) → F) '' s)) ∘ (⇑σ : (a : 𝕜₁) → 𝕜₂)) (𝓝 0)
    (smallSets (𝓝 0))
Tactic: simp only [isVonNBounded_iff_tendsto_smallSets_nhds, ← this, tendsto_map'_iff] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst_5 : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
⊢ IsVonNBounded 𝕜 S
have rw : ∀ (i : Set E), Membership.mem (γ := Filter E) (𝓝 0) i ∧ Balanced 𝕜 i → Absorbs 𝕜 (id i) S
Tactic: rw [(nhds_basis_balanced 𝕜 E).isVonNBounded_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst_5 : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
⊢ ∀ (i : Set E), Membership.mem (γ := Filter E) (𝓝 0) i ∧ Balanced 𝕜 i → Absorbs 𝕜 (id i) S
have by_contra! : ∀ (V : Set E) (hVS : ¬Absorbs 𝕜 (id V) S) (hV : Membership.mem (γ := Filter E) (𝓝 0) V) (hVb : Balanced 𝕜 V), False
Tactic: by_contra! ⟨V, ⟨hV, hVb⟩, hVS⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst_5 : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕜 (id V) S
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hVb : Balanced 𝕜 V
⊢ ∀ᶠ (n : ι) in l, ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
have h : ∀ (n : ι) (hn : ε n ≠ 0), ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
Tactic: filter_upwards [hε] with n hn