awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ (fun (x : E) ↦ a • x) '' interior A ⊆ interior A

Tactic:
((isOpenMap_smul₀ h).mapsTo_interior <| hA.smul_mem ha).image_subset

Premises used: isOpenMap_smul₀, IsOpenMap.mapsTo_interior, Set.MapsTo.image_subset, Balanced.smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ (fun (x : E) ↦ a • x) '' interior A ⊆ interior A

Tactic:
exact ((isOpenMap_smul₀ h).mapsTo_interior <| hA.smul_mem ha).image_subset

Premises used: isOpenMap_smul₀, IsOpenMap.mapsTo_interior, Set.MapsTo.image_subset, Balanced.smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ interior A
rw : Balanced 𝕜 (insert 0 (interior A))
⊢ Balanced 𝕜 (interior A)

Tactic:
rw [← insert_eq_self.2 h]

Premises used: Iff.mpr, Set.insert_eq_self
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ interior A
⊢ Balanced 𝕜 (insert 0 (interior A))

Tactic:
hA.zero_insert_interior

Premises used: Balanced.zero_insert_interior
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ interior A
⊢ Balanced 𝕜 (insert 0 (interior A))

Tactic:
exact hA.zero_insert_interior

Premises used: Balanced.zero_insert_interior
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
⊢ Balanced 𝕜 (closure[inst_3] A)

Tactic:
fun _a ha =>
  (image_closure_subset_closure_image <| continuous_const_smul _).trans <|
    closure_mono <| hA _ ha

Premises used: ContinuousConstSMul.continuous_const_smul, HasSubset.Subset.trans, closure_mono, image_closure_subset_closure_image, Balanced
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : Balanced 𝕜 s
this :
  Convex.{u_1, u_3} 𝕜 (E := E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
rw :
  ∀ (hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s)
    (this :
      Convex.{u_1, u_3} 𝕜 (E := E)
        {x : E |
          ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)})
    ⦃a : 𝕜⦄,
    ‖a‖ ≤ 1 →
      ∀ ⦃x : E⦄,
        Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x →
          Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)
⊢ Balanced.{u_1, u_3} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
rw [balanced_iff_smul_mem] at hs ⊢

Premises used: balanced_iff_smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this :
  Convex.{u_1, u_3} 𝕜 (E := E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
⊢ ∀ ⦃a : 𝕜⦄,
    ‖a‖ ≤ 1 →
      ∀ ⦃x : E⦄,
        Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x →
          Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)

Tactic:
fun a ha x hx => convexHull_min ?_ this hx a ha

Premises used: convexHull_min
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this :
  Convex.{u_1, u_3} 𝕜 (E := E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
refine :
  ∀ (a : 𝕜) (ha : ‖a‖ ≤ 1) (x : E)
    (hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x),
    s ⊆
      {x : E |
        ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
⊢ ∀ ⦃a : 𝕜⦄,
    ‖a‖ ≤ 1 →
      ∀ ⦃x : E⦄,
        Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x →
          Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)

Tactic:
refine fun a ha x hx => convexHull_min ?_ this hx a ha

Premises used: convexHull_min
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this :
  Convex.{u_1, u_3} 𝕜 (E := E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
⊢ s ⊆
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}

Tactic:
fun y hy a ha => subset_convexHull 𝕜 s (hs ha hy)

Premises used: Set.Mem, subset_convexHull, setOf, Set.Subset
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this :
  Convex.{u_1, u_3} 𝕜 (E := E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
⊢ s ⊆
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}

Tactic:
exact fun y hy a ha => subset_convexHull 𝕜 s (hs ha hy)

Premises used: subset_convexHull
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : Balanced 𝕜 s
suffices :
  Convex.{u_1, u_3} 𝕜 (E := E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
⊢ Balanced.{u_1, u_3} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
suffices Convex 𝕜 { x | ∀ a : 𝕜, ‖a‖ ≤ 1 → a • x ∈ convexHull 𝕜 s } by
    rw [balanced_iff_smul_mem] at hs ⊢
    refine fun a ha x hx => convexHull_min ?_ this hx a ha
    exact fun y hy a ha => subset_convexHull 𝕜 s (hs ha hy)
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : Balanced 𝕜 s
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
    x
y : E
hy :
  Membership.mem (γ := Set E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
    y
u v : 𝕜
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
rw : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (u • a • x + v • a • y)
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • (u • x + v • y))

Tactic:
rw [smul_add, ← smul_comm u, ← smul_comm v]

Premises used: SMulCommClass.smul_comm, smul_add
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : Balanced 𝕜 s
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
    x
y : E
hy :
  Membership.mem (γ := Set E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
    y
u v : 𝕜
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (u • a • x + v • a • y)

Tactic:
convex_convexHull 𝕜 s (hx a ha) (hy a ha) hu hv huv

Premises used: Set.Mem, convex_convexHull
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : Balanced 𝕜 s
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
    x
y : E
hy :
  Membership.mem (γ := Set E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
    y
u v : 𝕜
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (u • a • x + v • a • y)

Tactic:
exact convex_convexHull 𝕜 s (hx a ha) (hy a ha) hu hv huv

Premises used: convex_convexHull
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
S : Type u_7
inst_3 : SetLike S E
inst_4 : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 (↑V : Set E)
rw : ∀ (x : E), x ∈ (↑V : Set E)
⊢ (↑V : Set E) = univ

Tactic:
rw [eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
S : Type u_7
inst_3 : SetLike S E
inst_4 : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 (↑V : Set E)
x : E
obtain : ∀ (c : 𝕜) (hc : c • x ∈ (↑V : Set E)) (hc' : Membership.mem (γ := Set 𝕜) {0}ᶜ c), x ∈ (↑V : Set E)
⊢ x ∈ (↑V : Set E)

Tactic:
obtain ⟨c, hc, hc'⟩ :=
    ((absorbent_iff_eventually_nhdsNE_zero.mp hV x).and eventually_mem_nhdsWithin).exists

Premises used: absorbent_iff_eventually_nhdsNE_zero, eventually_mem_nhdsWithin, Filter.Eventually.and, Filter.Eventually.exists, Iff.mp
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
S : Type u_7
inst_3 : SetLike S E
inst_4 : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 (↑V : Set E)
x : E
c : 𝕜
hc : c • x ∈ (↑V : Set E)
hc' : Membership.mem (γ := Set 𝕜) {0}ᶜ c
rw : c⁻¹ • c • x ∈ (↑V : Set E)
⊢ x ∈ (↑V : Set E)

Tactic:
rw [← inv_smul_smul₀ hc' x]

Premises used: inv_smul_smul₀
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
S : Type u_7
inst_3 : SetLike S E
inst_4 : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 (↑V : Set E)
x : E
c : 𝕜
hc : c • x ∈ (↑V : Set E)
hc' : Membership.mem (γ := Set 𝕜) {0}ᶜ c
⊢ c⁻¹ • c • x ∈ (↑V : Set E)

Tactic:
SMulMemClass.smul_mem c⁻¹ hc

Premises used: SMulMemClass.smul_mem, Set.Mem, Inv.inv
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
S : Type u_7
inst_3 : SetLike S E
inst_4 : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 (↑V : Set E)
x : E
c : 𝕜
hc : c • x ∈ (↑V : Set E)
hc' : Membership.mem (γ := Set 𝕜) {0}ᶜ c
⊢ c⁻¹ • c • x ∈ (↑V : Set E)

Tactic:
exact SMulMemClass.smul_mem c⁻¹ hc

Premises used: SMulMemClass.smul_mem, Inv.inv
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
V : Submodule 𝕜 E
hV : Absorbent 𝕜 (↑V : Set E)
⊢ V = ⊤

Tactic:
(StrictMono.apply_eq_top_iff (α := Submodule 𝕜 E) (β := Set E) (fun _ _ a_1 ↦ a_1)).mp
  hV.eq_univ_of_smulMemClass

Premises used: Absorbent.eq_univ_of_smulMemClass, Iff.mp, StrictMono.apply_eq_top_iff
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
F : Type u_8
𝕜₂ : Type u_9
inst_3 : Semiring 𝕜₂
σ : 𝕜₂ →+* 𝕜
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : RingHomSurjective σ
f : F →ₛₗ[σ] E
s : Set E
hs_abs : Absorbent 𝕜 s
⊢ s ⊆ (↑f.range : Set E) ↔ Function.Surjective.{u_8 + 1, u_3 + 1} (α := F) (β := E) (⇑f : (a : F) → E)

Tactic:
⟨fun hs_sub ↦ LinearMap.range_eq_top.mp ((hs_abs.mono hs_sub).submodule_eq_top), fun h a _ ↦ h a⟩

Premises used: LinearMap.range_eq_top, Absorbent.submodule_eq_top, Iff.intro, Iff.mp, Absorbent.mono
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
⊢ Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s

Tactic:
⟨fun h x => h.neg_mem_iff.2, fun h a ha => smul_set_subset_iff.2 fun x hx => ?_⟩

Premises used: Iff.mpr, Iff.intro, Balanced.neg_mem_iff, Set.smul_set_subset_iff
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
refine : ∀ (h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s) (a : ℝ) (ha : ‖a‖ ≤ 1) (x : E) (hx : x ∈ s), a • x ∈ s
⊢ Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s

Tactic:
refine ⟨fun h x => h.neg_mem_iff.2, fun h a ha => smul_set_subset_iff.2 fun x hx => ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ s
rw : ∀ (ha : -1 ≤ a ∧ a ≤ 1) (x : E) (hx : x ∈ s), a • x ∈ s
⊢ a • x ∈ s

Tactic:
rw [Real.norm_eq_abs, abs_le] at ha

Premises used: abs_le, Real.norm_eq_abs
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a = -((1 - a) / 2) + (a - -1) / 2

Tactic:
ring
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
rw : ((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s
⊢ a • x ∈ s

Tactic:
rw [show a = -((1 - a) / 2) + (a - -1) / 2 by ring, add_smul, neg_smul, ← smul_neg]

Premises used: neg_smul, smul_neg, add_smul
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ (1 - a) / 2 + (a - -1) / 2 = 1

Tactic:
ring
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ ((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s

Tactic:
exact hs (h hx) hx (div_nonneg (sub_nonneg_of_le ha.2) zero_le_two)
    (div_nonneg (sub_nonneg_of_le ha.1) zero_le_two) (by ring)

Premises used: sub_nonneg_of_le, And.right, And.left, zero_le_two, div_nonneg
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
⊢ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ∅

Tactic:
fun _ _ => Absorbs.empty

Premises used: Absorbs.empty, Bornology.IsVonNBounded
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
s : Set E
⊢ IsVonNBounded 𝕜 s ↔ ∀ (V : Set E), Membership.mem (γ := Filter E) (𝓝 0) V → Absorbs 𝕜 V s

Tactic:
Iff.rfl

Premises used: Bornology.IsVonNBounded, Iff.rfl
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
⊢ IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A

Tactic:
⟨fun hA i hi => hA (h.mem_of_mem hi), fun hA V hV => ?_⟩

Premises used: Iff.intro, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
refine :
  ∀ (hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A) (V : Set E) (hV : Membership.mem (γ := Filter E) (𝓝 0) V), Absorbs 𝕜 V A
⊢ IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A

Tactic:
refine ⟨fun hA i hi => hA (h.mem_of_mem hi), fun hA V hV => ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
rcases : ∀ (i : ι) (hi : q i) (hV : s i ⊆ V), Absorbs 𝕜 V A
⊢ Absorbs 𝕜 V A

Tactic:
rcases h.mem_iff.mp hV with ⟨i, hi, hV⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV_1 : Membership.mem (γ := Filter E) (𝓝 0) V
i : ι
hi : q i
hV : s i ⊆ V
⊢ Absorbs 𝕜 V A

Tactic:
(hA i hi).mono_left hV

Premises used: Absorbs.mono_left
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV_1 : Membership.mem (γ := Filter E) (𝓝 0) V
i : ι
hi : q i
hV : s i ⊆ V
⊢ Absorbs 𝕜 V A

Tactic:
exact (hA i hi).mono_left hV

Premises used: Absorbs.mono_left
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
s₁ s₂ : Set E
h : s₁ ⊆ s₂
hs₂ : IsVonNBounded 𝕜 s₂
⊢ IsVonNBounded 𝕜 s₁

Tactic:
fun _ hV => (hs₂ hV).mono_right h

Premises used: Bornology.IsVonNBounded, Absorbs.mono_right
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
s t : Set E
⊢ IsVonNBounded 𝕜 (s ∪ t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
simp only [IsVonNBounded, absorbs_union, forall_and]

Premises used: Bornology.IsVonNBounded, absorbs_union, forall_and
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
s₁ s₂ : Set E
hs₁ : IsVonNBounded 𝕜 s₁
hs₂ : IsVonNBounded 𝕜 s₂
⊢ IsVonNBounded 𝕜 (s₁ ∪ s₂)

Tactic:
isVonNBounded_union.2 ⟨hs₁, hs₂⟩

Premises used: Iff.mpr, Bornology.isVonNBounded_union, And.intro
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
inst_4 : BoundedSpace 𝕜
s : Set E
⊢ IsVonNBounded 𝕜 s

Tactic:
fun _ _ ↦
  .of_boundedSpace

Premises used: Bornology.IsVonNBounded, Absorbs.of_boundedSpace
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
inst_4 : Subsingleton E
s : Set E
⊢ IsVonNBounded 𝕜 s

Tactic:
fun U hU ↦ .of_forall fun c ↦ calc
    s ⊆ univ := subset_univ s
    _ = c • U := .symm <| Subsingleton.eq_univ_of_nonempty <| (Filter.nonempty_of_mem hU).image _

Premises used: Trans.trans, Bornology.IsVonNBounded, Set.subset_univ, Filter.Eventually.of_forall, Filter.nonempty_of_mem, Set.Nonempty.image, Absorbs, HSMul.hSMul, Subsingleton.eq_univ_of_nonempty, Eq.symm
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
ι : Sort u_6
inst_4 : Finite ι
s : ι → Set E
⊢ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ (i : ι), s i) ↔ ∀ (i : ι), IsVonNBounded 𝕜 (s i)

Tactic:
simp only [IsVonNBounded, absorbs_iUnion, @forall_comm ι]

Premises used: Bornology.IsVonNBounded, absorbs_iUnion, forall_comm
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
⊢ Finite.{u_6 + 1} (↑I : Type u_6)

Tactic:
have _ := hI.to_subtype
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
h : Finite.{u_6 + 1} (↑I : Type u_6)
rw : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ (x : (↑I : Type u_6)), s (↑x : ι)) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
rw₁ : (∀ (i : (↑I : Type u_6)), IsVonNBounded 𝕜 (s (↑i : ι))) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
rw₂ rw₃ :
  (∀ (a : ι) (b : a ∈ I), IsVonNBounded 𝕜 (s (↑(Subtype.mk (p := fun (a : ι) ↦ a ∈ I) a b) : ι))) ↔
    ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
⊢ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)

Tactic:
rw [biUnion_eq_iUnion, isVonNBounded_iUnion, Subtype.forall]

Premises used: Bornology.isVonNBounded_iUnion, Subtype.forall, Set.biUnion_eq_iUnion
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
S : Set (Set E)
hS : S.Finite
rw : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ i ∈ S, i) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s
rw₁ rw₂ : (∀ i ∈ S, IsVonNBounded 𝕜 i) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s
⊢ IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s

Tactic:
rw [sUnion_eq_biUnion, isVonNBounded_biUnion hS]

Premises used: Set.sUnion_eq_biUnion, Bornology.isVonNBounded_biUnion
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddZeroClass E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : DistribSMul 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
rcases : ∀ (V : Set E) (hVo : IsOpen[inst_2] V) (hV : 0 ∈ V) (hVU : V + V ⊆ U), Absorbs 𝕜 U (s + t)
⊢ Absorbs 𝕜 U (s + t)

Tactic:
rcases exists_open_nhds_zero_add_subset hU with ⟨V, hVo, hV, hVU⟩

Premises used: exists_open_nhds_zero_add_subset
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddZeroClass E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : DistribSMul 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set E
hVo : IsOpen[inst_2] V
hV : 0 ∈ V
hVU : V + V ⊆ U
⊢ Absorbs 𝕜 U (s + t)

Tactic:
((hs <| hVo.mem_nhds hV).add (ht <| hVo.mem_nhds hV)).mono_left hVU

Premises used: Absorbs.mono_left, Absorbs.add, IsOpen.mem_nhds