awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
⊢ Absorbs 𝕜 U s
have rcases : ∀ (x : Set E × Set E)
  (hx :
    (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
      Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2)
  (h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U), Absorbs 𝕜 U s
Tactic: rcases h.basis_left h' U hU with ⟨x, hx, h''⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
⊢ Absorbs 𝕜 U s
have rcases : ∀ (t : Set E) (ht : t.Finite) (hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2), Absorbs 𝕜 U s
Tactic: rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ Absorbs 𝕜 U s
have refine : Absorbs 𝕜 U (⋃ y ∈ t, y +ᵥ x.2)
Tactic: refine Absorbs.mono_right ?_ hs
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ Absorbs 𝕜 U (⋃ y ∈ t, y +ᵥ x.2)
have rw : ∀ i ∈ t, Absorbs 𝕜 U (i +ᵥ x.2)
Tactic: rw [ht.absorbs_biUnion]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ ∀ i ∈ t, Absorbs 𝕜 U (i +ᵥ x.2)
have hx_fstsnd : x.1 + x.2 ⊆ U
Tactic: have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦
      h'' <| mk_mem_prod hz1 hz2
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
hx_fstsnd : x.1 + x.2 ⊆ U
⊢ ∀ i ∈ t, Absorbs 𝕜 U (i +ᵥ x.2)
have refine : ∀ y ∈ t, Absorbs 𝕜 (x.1 + x.2) (y +ᵥ x.2)
Tactic: refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
h : ¬∃ (x : 𝕜), 1 < ‖x‖
⊢ Bornology.IsVonNBounded 𝕜 s
have this : BoundedSpace 𝕜
Tactic: haveI : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
⊢ Bornology.IsVonNBounded 𝕜 s
have if : ∀ (h : ∃ (x : 𝕜), 1 < ‖x‖), Bornology.IsVonNBounded 𝕜 s
Tactic: if h : ∃ x : 𝕜, 1 < ‖x‖ then
    letI : NontriviallyNormedField 𝕜 := ⟨h⟩
    rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs
    intro U hU
    have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 0) (𝓝 0) :=
      continuous_add.tendsto' _ _ (zero_add _)
    have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
    simp_rw [← nhds_prod_eq, id] at h'
    rcases h.basis_left h' U hU with ⟨x, hx, h''⟩
    rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩
    refine Absorbs.mono_right ?_ hs
    rw [ht.absorbs_biUnion]
    have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦
      h'' <| mk_mem_prod hz1 hz2
    refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd
    exact (absorbent_nhds_zero hx.1.1).vadd_absorbs hx.2.2.absorbs_self
  else
    haveI : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
    exact Bornology.IsVonNBounded.of_boundedSpace
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
if : ∀ (h : ∃ (x : 𝕜), 1 < ‖x‖), Bornology.IsVonNBounded 𝕜 s
⊢ Bornology.IsVonNBounded 𝕜 s
have if₁ : ∀ (h : ¬∃ (x : 𝕜), 1 < ‖x‖), Bornology.IsVonNBounded 𝕜 s
Tactic: if h : ∃ x : 𝕜, 1 < ‖x‖ then
    letI : NontriviallyNormedField 𝕜 := ⟨h⟩
    rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs
    intro U hU
    have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 0) (𝓝 0) :=
      continuous_add.tendsto' _ _ (zero_add _)
    have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
    simp_rw [← nhds_prod_eq, id] at h'
    rcases h.basis_left h' U hU with ⟨x, hx, h''⟩
    rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩
    refine Absorbs.mono_right ?_ hs
    rw [ht.absorbs_biUnion]
    have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦
      h'' <| mk_mem_prod hz1 hz2
    refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd
    exact (absorbent_nhds_zero hx.1.1).vadd_absorbs hx.2.2.absorbs_self
  else
    haveI : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
    exact Bornology.IsVonNBounded.of_boundedSpace
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
⊢ Absorbs 𝕜 V s
have refine : AntilipschitzWith.{u_1, u_2} (β := 𝕜') (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ fun (x : 𝕜) ↦ HSMul.hSMul (β := 𝕜') x 1
Tactic: refine (h hV).restrict_scalars <| AntilipschitzWith.tendsto_cobounded (K := ‖(1 : 𝕜')‖₊⁻¹) ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
⊢ AntilipschitzWith.{u_1, u_2} (β := 𝕜') (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ fun (x : 𝕜) ↦ HSMul.hSMul (β := 𝕜') x 1
have refine : ∀ (x y : 𝕜), nndist x y ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
Tactic: refine AntilipschitzWith.of_le_mul_nndist fun x y ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
x y : 𝕜
⊢ nndist x y ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
have rw : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
    mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
x y : 𝕜
rw : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
⊢ nndist x y ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
have rw₁ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * ‖HSMul.hSMul (β := 𝕜') x 1 - HSMul.hSMul (β := 𝕜') y 1‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
    mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
x y : 𝕜
rw : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
rw₁ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * ‖HSMul.hSMul (β := 𝕜') x 1 - HSMul.hSMul (β := 𝕜') y 1‖₊
⊢ nndist x y ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
have rw₂ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * ‖HSMul.hSMul (β := 𝕜') (x - y) 1‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
    mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
x y : 𝕜
rw : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
rw₁ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * ‖HSMul.hSMul (β := 𝕜') x 1 - HSMul.hSMul (β := 𝕜') y 1‖₊
rw₂ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * ‖HSMul.hSMul (β := 𝕜') (x - y) 1‖₊
⊢ nndist x y ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
have rw₃ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * (‖x - y‖₊ * nnnorm.{u_2} (E := 𝕜') 1)
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
    mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
x y : 𝕜
rw : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
rw₁ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * ‖HSMul.hSMul (β := 𝕜') x 1 - HSMul.hSMul (β := 𝕜') y 1‖₊
rw₂ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * ‖HSMul.hSMul (β := 𝕜') (x - y) 1‖₊
rw₃ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * (‖x - y‖₊ * nnnorm.{u_2} (E := 𝕜') 1)
⊢ nndist x y ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
have rw₄ : ‖x - y‖₊ ≤ ‖x - y‖₊ * nnnorm.{u_2} (E := 𝕜') 1 / nnnorm.{u_2} (E := 𝕜') 1
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
    mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
x y : 𝕜
rw : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
rw₁ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * ‖HSMul.hSMul (β := 𝕜') x 1 - HSMul.hSMul (β := 𝕜') y 1‖₊
rw₂ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * ‖HSMul.hSMul (β := 𝕜') (x - y) 1‖₊
rw₃ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * (‖x - y‖₊ * nnnorm.{u_2} (E := 𝕜') 1)
rw₄ : ‖x - y‖₊ ≤ ‖x - y‖₊ * nnnorm.{u_2} (E := 𝕜') 1 / nnnorm.{u_2} (E := 𝕜') 1
⊢ nndist x y ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
have rw₅ : ‖x - y‖₊ ≤ ‖x - y‖₊
Tactic: rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
    mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
⊢ Bornology.IsVonNBounded 𝕜 s
have rcases : ∀ (r : ℝ) (hr : s ⊆ Metric.ball 0 r), Bornology.IsVonNBounded 𝕜 s
Tactic: rcases h.subset_ball 0 with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Metric.ball 0 r
⊢ Bornology.IsVonNBounded 𝕜 s
have rw : ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Metric.ball 0 i) s
Tactic: rw [Metric.nhds_basis_ball.isVonNBounded_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Metric.ball 0 r
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Metric.ball 0 i) s
have rw : ∀ (hr : s ⊆ Seminorm.ball (normSeminorm 𝕜 E) 0 r) (i : ℝ), 0 < i → Absorbs 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 i) s
Tactic: rw [← ball_normSeminorm 𝕜 E] at hr ⊢
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
have refine : ∀ (h : Bornology.IsVonNBounded 𝕜 s), Bornology.IsBounded s
Tactic: refine ⟨fun h ↦ ?_, isVonNBounded_of_isBounded _⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
⊢ Bornology.IsBounded s
have rcases : ∀ (ρ : ℝ) (hρ : ρ > 0) (hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ HSMul.hSMul (β := Set E) c (Metric.ball 0 1)),
  Bornology.IsBounded s
Tactic: rcases (h (Metric.ball_mem_nhds 0 zero_lt_one)).exists_pos with ⟨ρ, hρ, hρball⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ HSMul.hSMul (β := Set E) c (Metric.ball 0 1)
⊢ Bornology.IsBounded s
have rcases : ∀ (a : 𝕜) (ha : ρ < ‖a‖), Bornology.IsBounded s
Tactic: rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ HSMul.hSMul (β := Set E) c (Metric.ball 0 1)
a : 𝕜
ha : ρ < ‖a‖
⊢ Bornology.IsBounded s
have hρball₁ : s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
Tactic: specialize hρball a ha.le
Cleared hypotheses: hρball
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
⊢ Bornology.IsBounded s
have hρball₁ : s ⊆ Metric.ball 0 (‖a‖ * 1)
Tactic: rw [← ball_normSeminorm 𝕜 E, Seminorm.smul_ball_zero (norm_pos_iff.1 <| hρ.trans ha),
    ball_normSeminorm] at hρball
Cleared hypotheses: hρball
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r
have rw : Bornology.IsBounded s ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r
Tactic: rw [NormedSpace.isVonNBounded_iff, isBounded_iff_forall_norm_le]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
rw : Bornology.IsBounded s ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r
have rw₁ : (∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C) ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r
Tactic: rw [NormedSpace.isVonNBounded_iff, isBounded_iff_forall_norm_le]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
α : Type u_6
f : α → E
s : Set α
⊢ Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖f x‖ ≤ r
have simp_rw : (∃ (r : ℝ), ∀ x ∈ f '' s, ‖x‖ ≤ r) ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖f x‖ ≤ r
Tactic: simp_rw [isVonNBounded_iff', Set.forall_mem_image]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology
have rw : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
Tactic: rw [Bornology.ext_iff_isBounded]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s
have rw : Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
Tactic: rw [Bornology.isBounded_iff_isVonNBounded]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
have rw : Bornology.IsVonNBounded 𝕜 s ↔ ∃ (a : 𝕜), s ⊆ HSMul.hSMul (β := Set E) a (Metric.ball 0 1)
Tactic: rw [← isVonNBounded_iff 𝕜]