awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Sort u_5
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
f : ι → Set E
h : ∀ (i : ι), Balanced 𝕜 (f i)
⊢ Balanced.{u_1, u_3} 𝕜 (E := E) (⋂ (i : ι), f i)

Tactic:
fun _a ha => (smul_set_iInter_subset _ _).trans <| iInter_mono fun _ => h _ _ ha

Premises used: Set.smul_set_iInter_subset, HasSubset.Subset.trans, Set.iInter_mono, Balanced
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Sort u_5
κ : ι → Sort u_6
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
f : (i : ι) → κ i → Set E
h : ∀ (i : ι) (j : κ i), Balanced 𝕜 (f i j)
⊢ Balanced.{u_1, u_3} 𝕜 (E := E) (⋂ (i : ι), ⋂ (j : κ i), f i j)

Tactic:
balanced_iInter fun _ => balanced_iInter <| h _

Premises used: balanced_iInter
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : SMul 𝕜 F
s : Set F
hs : Balanced 𝕜 s
f : MulActionHom.{u_1, u_1, u_3, u_4} (M := 𝕜) id E F
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
h : x ∈ HSMul.hSMul (β := Set E) a ((⇑f : (a : E) → F) ⁻¹' s)
y : E
hy₁ : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) y
hy₂ : (fun (x : E) ↦ a • x) y = x
rw : HSMul.hSMul (β := F) a ((f : (a : E) → F) y : F) ∈ s
⊢ Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) x

Tactic:
rw [mem_preimage, ← hy₂, map_smul]

Premises used: Set.mem_preimage, map_smul
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : SMul 𝕜 F
s : Set F
hs : Balanced 𝕜 s
f : MulActionHom.{u_1, u_1, u_3, u_4} (M := 𝕜) id E F
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
h : x ∈ HSMul.hSMul (β := Set E) a ((⇑f : (a : E) → F) ⁻¹' s)
y : E
hy₁ : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) y
hy₂ : (fun (x : E) ↦ a • x) y = x
⊢ HSMul.hSMul (β := F) a ((f : (a : E) → F) y : F) ∈ s

Tactic:
hs a ha (smul_mem_smul_set hy₁)

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : SMul 𝕜 F
s : Set F
hs : Balanced 𝕜 s
f : MulActionHom.{u_1, u_1, u_3, u_4} (M := 𝕜) id E F
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
h : x ∈ HSMul.hSMul (β := Set E) a ((⇑f : (a : E) → F) ⁻¹' s)
y : E
hy₁ : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) y
hy₂ : (fun (x : E) ↦ a • x) y = x
⊢ HSMul.hSMul (β := F) a ((f : (a : E) → F) y : F) ∈ s

Tactic:
exact hs a ha (smul_mem_smul_set hy₁)

Premises used: Set.smul_mem_smul_set
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
inst_2 : SMul 𝕝 E
inst_3 : SMulCommClass 𝕜 𝕝 E
a : 𝕝
hs : Balanced 𝕜 s
⊢ Balanced 𝕜 (a • s)

Tactic:
fun _b hb =>
  (smul_comm _ _ _).subset.trans <| smul_set_mono <| hs _ hb

Premises used: HasSubset.Subset.trans, Set.smul_set_mono, Eq.subset, SMulCommClass.smul_comm, Balanced
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
⊢ Balanced 𝕜 s → Balanced 𝕜 (-s)

Tactic:
forall₂_imp fun _ _ h => (smul_set_neg _ _).subset.trans <| neg_subset_neg.2 h

Premises used: Iff.mpr, Set.smul_set_neg, forall₂_imp, Set.neg_subset_neg, HasSubset.Subset.trans, Eq.subset, Balanced
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
⊢ Balanced 𝕜 (-s) ↔ Balanced 𝕜 s

Tactic:
⟨fun h ↦ neg_neg s ▸ h.neg, fun h ↦ h.neg⟩

Premises used: Eq.rec, neg_neg, Iff.intro, Balanced.neg
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : -x ∈ s
⊢ norm.{u_1} (E := 𝕜) (-1) ≤ 1

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : -x ∈ s
⊢ x ∈ s

Tactic:
simpa using h.smul_mem (a := -1) (by simp) hx

Premises used: Balanced.smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : x ∈ s
⊢ norm.{u_1} (E := 𝕜) (-1) ≤ 1

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : x ∈ s
⊢ -x ∈ s

Tactic:
simpa using h.smul_mem (a := -1) (by simp) hx

Premises used: Balanced.smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormOneClass 𝕜
h : Balanced 𝕜 s
⊢ -s = s

Tactic:
Set.ext fun _ ↦ h.neg_mem_iff

Premises used: Set.ext, Balanced.neg_mem_iff
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s + t)

Tactic:
fun _a ha =>
  (smul_add _ _ _).subset.trans <| add_subset_add (hs _ ha) <| ht _ ha

Premises used: HasSubset.Subset.trans, Eq.subset, Set.add_subset_add, Balanced, smul_add
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
simp_rw : Balanced 𝕜 (s + -t)
⊢ Balanced 𝕜 (s - t)

Tactic:
simp_rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s + -t)

Tactic:
hs.add ht.neg

Premises used: Balanced.add, Balanced.neg
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s + -t)

Tactic:
exact hs.add ht.neg

Premises used: Balanced.add, Balanced.neg
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
⊢ Balanced.{u_1, u_3} 𝕜 (E := E) 0

Tactic:
fun _a _ha => (smul_zero _).subset

Premises used: smul_zero, Eq.subset, Balanced
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
rw :
  (∀ᶠ (c : 𝕜) in Bornology.cobounded 𝕜, MapsTo (fun (x : E) ↦ c⁻¹ • x) t s) ↔
    ∀ᶠ (c : 𝕜) in (Bornology.cobounded 𝕜)⁻¹, MapsTo (fun (x : E) ↦ c • x) t s
⊢ Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, MapsTo (fun (x : E) ↦ c • x) t s

Tactic:
rw [absorbs_iff_eventually_cobounded_mapsTo, ← Filter.inv_cobounded₀]

Premises used: Filter.inv_cobounded₀, absorbs_iff_eventually_cobounded_mapsTo
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
⊢ (∀ᶠ (c : 𝕜) in Bornology.cobounded 𝕜, MapsTo (fun (x : E) ↦ c⁻¹ • x) t s) ↔
    ∀ᶠ (c : 𝕜) in (Bornology.cobounded 𝕜)⁻¹, MapsTo (fun (x : E) ↦ c • x) t s

Tactic:
rfl
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
⊢ Absorbs 𝕜 s {x} ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, c • x ∈ s

Tactic:
simp only [absorbs_iff_eventually_nhdsNE_zero, mapsTo_singleton]

Premises used: absorbs_iff_eventually_nhdsNE_zero, Set.mapsTo_singleton
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
rw : MapsTo (fun (x : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 x) t s
⊢ Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝 0, MapsTo (fun (x : E) ↦ c • x) t s

Tactic:
rw [← nhdsNE_sup_pure, Filter.eventually_sup, Filter.eventually_pure,
    ← absorbs_iff_eventually_nhdsNE_zero, and_iff_left]

Premises used: and_iff_left, absorbs_iff_eventually_nhdsNE_zero, Filter.eventually_pure, Filter.eventually_sup, nhdsNE_sup_pure
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
x : E
_ : x ∈ t → (fun (x : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 x) x ∈ s
⊢ x ∈ t → (fun (x : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 x) x ∈ s

Tactic:
_
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
x : E
h : x ∈ t
⊢ (fun (x : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 x) x ∈ s

Tactic:
simpa only [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h : Absorbs 𝕜 s t
h₀ : 0 ∈ s
⊢ ∀ᶠ (c : 𝕜) in 𝓝 0, MapsTo (fun (x : E) ↦ c • x) t s

Tactic:
(absorbs_iff_eventually_nhds_zero h₀).1 h

Premises used: Iff.mp, absorbs_iff_eventually_nhds_zero
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
inl : ∀ (h : ‖a‖ ≤ norm.{u_1} (E := 𝕜) 0), a • s ⊆ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 s
inr : ∀ (hb : b ≠ 0), a • s ⊆ b • s
⊢ a • s ⊆ b • s

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ norm.{u_1} (E := 𝕜) 0
⊢ a = 0

Tactic:
rw [norm_zero, norm_le_zero_iff] at h

Premises used: norm_zero, norm_le_zero_iff
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
hs : Balanced 𝕝 s
a : 𝕝
h : a = 0
⊢ a • s ⊆ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 s

Tactic:
simp only [h, ← image_smul, zero_smul, Subset.rfl]

Premises used: Set.image_smul, zero_smul, Set.Subset.rfl
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
rw : a • s = b • b⁻¹ • a • s
rw₁ rw₂ : a • s = a • s
⊢ a • s = b • (b⁻¹ • a) • s

Tactic:
rw [smul_assoc, smul_inv_smul₀ hb]

Premises used: smul_assoc, smul_inv_smul₀
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
rw : ‖a‖ / ‖b‖ ≤ 1
⊢ ‖b⁻¹ • a‖ ≤ 1

Tactic:
rw [norm_smul, norm_inv, ← div_eq_inv_mul]

Premises used: norm_smul, norm_inv, div_eq_inv_mul
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ ‖a‖ / ‖b‖ ≤ 1

Tactic:
div_le_one_of_le₀ h (norm_nonneg _)

Premises used: div_le_one_of_le₀, norm_nonneg
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ ‖a‖ / ‖b‖ ≤ 1

Tactic:
exact div_le_one_of_le₀ h (norm_nonneg _)

Premises used: div_le_one_of_le₀, norm_nonneg
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
a₁ : a • s = b • (b⁻¹ • a) • s
⊢ a • s ⊆ b • s

Tactic:
calc
      a • s = b • (b⁻¹ • a) • s := by rw [smul_assoc, smul_inv_smul₀ hb]
      _ ⊆ b • s := smul_set_mono <| hs _ <| by
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ h (norm_nonneg _)

Premises used: Set.smul_set_mono, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
inl : ∀ (ha : HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 x ∈ s) (hba : ‖b‖ ≤ norm.{u_1} (E := 𝕜) 0), b • x ∈ s
inr : ∀ (ha₀ : a ≠ 0), b • x ∈ s
⊢ b • x ∈ s

Tactic:
rcases eq_or_ne a 0 with rfl | ha₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 x ∈ s
hba : ‖b‖ ≤ norm.{u_1} (E := 𝕜) 0
⊢ b • x ∈ s

Tactic:
simp_all
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ (a⁻¹ • b) • a • x ∈ s

Tactic:
hs.smul_mem ?_ ha

Premises used: Balanced.smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
refine : ‖a⁻¹ • b‖ ≤ 1
⊢ (a⁻¹ • b) • a • x ∈ s

Tactic:
refine hs.smul_mem ?_ ha

Premises used: Balanced.smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
rw : ‖b‖ / ‖a‖ ≤ 1
⊢ ‖a⁻¹ • b‖ ≤ 1

Tactic:
rw [norm_smul, norm_inv, ← div_eq_inv_mul]

Premises used: norm_smul, norm_inv, div_eq_inv_mul
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ ‖b‖ / ‖a‖ ≤ 1

Tactic:
div_le_one_of_le₀ hba (norm_nonneg _)

Premises used: div_le_one_of_le₀, norm_nonneg
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ ‖b‖ / ‖a‖ ≤ 1

Tactic:
exact div_le_one_of_le₀ hba (norm_nonneg _)

Premises used: div_le_one_of_le₀, norm_nonneg
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
rw : a • (a⁻¹ • b) • x = b • x
rw₁ : a • a⁻¹ • b • x = b • x
rw₂ rw₃ : b • x = b • x
⊢ (a⁻¹ • b) • a • x = b • x

Tactic:
rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]

Premises used: smul_assoc, smul_inv_smul₀, SMulCommClass.smul_comm
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
a₁ : (a⁻¹ • b) • a • x ∈ s
a₂ : (a⁻¹ • b) • a • x = b • x
⊢ b • x ∈ s

Tactic:
calc
      (a⁻¹ • b) • a • x ∈ s := by
        refine hs.smul_mem ?_ ha
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ hba (norm_nonneg _)
      (a⁻¹ • b) • a • x = b • x := by rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]

Premises used: Inv.inv, HSMul.hSMul
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : 1 ≤ ‖a‖
⊢ norm.{u_1} (E := 𝕜) 1 ≤ ‖a‖

Tactic:
rw [← @norm_one 𝕜] at ha

Premises used: NormOneClass.norm_one
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : norm.{u_1} (E := 𝕜) 1 ≤ ‖a‖
⊢ s ⊆ a • s

Tactic:
simpa using hs.smul_mono ha

Premises used: Balanced.smul_mono
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
⊢ a • s = b • s

Tactic:
(hs.smul_mono h.le).antisymm (hs.smul_mono h.ge)

Premises used: Eq.ge, Eq.le, HasSubset.Subset.antisymm, Balanced.smul_mono
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : ‖a‖ = 1
⊢ a • s = s

Tactic:
(hs _ ha.le).antisymm <| hs.subset_smul ha.ge

Premises used: Eq.ge, Balanced.subset_smul, Eq.le, HasSubset.Subset.antisymm
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : Balanced 𝕜 s
⊢ Absorbs 𝕜 s s

Tactic:
.of_norm ⟨1, fun _ => hs.subset_smul⟩

Premises used: Balanced.subset_smul, Exists.intro, Absorbs.of_norm, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
⊢ a • x ∈ s ↔ b • x ∈ s

Tactic:
⟨(hs.smul_mem_mono · h.ge), (hs.smul_mem_mono · h.le)⟩

Premises used: Eq.ge, Eq.le, Balanced.smul_mem_mono, Iff.intro
-- 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 : Membership.mem (γ := Filter E) (𝓝 0) A
x : E
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Filter E) (𝓝 0) A
⊢ A ∈ 𝓝 (HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 x)

Tactic:
rwa [zero_smul]

Premises used: zero_smul
-- 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
inl :
  ∀ (ha : norm.{u_1} (E := 𝕜) 0 ≤ 1),
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 (insert 0 (interior A)) ⊆ insert 0 (interior A)
inr : ∀ (h : a ≠ 0), a • insert 0 (interior A) ⊆ insert 0 (interior A)
⊢ a • insert 0 (interior A) ⊆ insert 0 (interior A)

Tactic:
obtain rfl | h := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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
ha : norm.{u_1} (E := 𝕜) 0 ≤ 1
inl : 0 ⊆ insert 0 (interior A)
inl₁ : (insert 0 (interior A)).Nonempty
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 (insert 0 (interior A)) ⊆ insert 0 (interior A)

Tactic:
rw [zero_smul_set]

Premises used: Set.zero_smul_set
-- 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
ha : norm.{u_1} (E := 𝕜) 0 ≤ 1
⊢ 0 ⊆ insert 0 (interior A)

Tactic:
subset_union_left

Premises used: Set.insert, Set.Mem, setOf, Set.subset_union_left, Set.singleton
-- 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
ha : norm.{u_1} (E := 𝕜) 0 ≤ 1
⊢ (insert 0 (interior A)).Nonempty

Tactic:
⟨0, Or.inl rfl⟩

Premises used: Set.Nonempty, Exists.intro, Or.inl, OfNat.ofNat, rfl
-- 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
ha : norm.{u_1} (E := 𝕜) 0 ≤ 1
⊢ 0 ⊆ insert 0 (interior A)

Tactic:
exacts [subset_union_left, ⟨0, Or.inl rfl⟩]

Premises used: Set.subset_union_left
-- 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
inr : insert 0 ((fun (x : E) ↦ a • x) '' interior A) ⊆ insert 0 (interior A)
⊢ a • insert 0 (interior A) ⊆ insert 0 (interior A)

Tactic:
rw [← image_smul, image_insert_eq, smul_zero]

Premises used: Set.image_smul, smul_zero, Set.image_insert_eq
-- 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
inr : (fun (x : E) ↦ a • x) '' interior A ⊆ interior A
⊢ insert 0 ((fun (x : E) ↦ a • x) '' interior A) ⊆ insert 0 (interior A)

Tactic:
apply insert_subset_insert

Premises used: Set.insert_subset_insert