-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem basisSets_smul (U) (hU : U ∈ p.basisSets) :
    ∃ V ∈ 𝓝 (0 : 𝕜), ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ Metric.ball 0 √r • (s.sup p).ball 0 √r ⊆ U

Tactic:
refine Set.Subset.trans (ball_smul_ball (s.sup p) √r √r) ?_

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (√r * √r) ⊆ U

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (√r * √r) ⊆ U

Tactic:
rw [hU, Real.mul_self_sqrt (le_of_lt hr)]

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ W ∈ AddGroupFilterBasis.toFilterBasis.sets, Metric.ball 0 √r • W ⊆ U

Tactic:
refine ⟨(s.sup p).ball 0 √r, p.basisSets_mem s (Real.sqrt_pos.mpr hr), ?_⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ Metric.ball 0 √r • (s.sup p).ball 0 √r ⊆ U

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ 𝓝 0, ∃ W ∈ AddGroupFilterBasis.toFilterBasis.sets, V • W ⊆ U

Tactic:
refine ⟨Metric.ball 0 √r, Metric.ball_mem_nhds 0 (Real.sqrt_pos.mpr hr), ?_⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ W ∈ AddGroupFilterBasis.toFilterBasis.sets, Metric.ball 0 √r • W ⊆ U

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU : U ∈ p.basisSets
⊢ ∃ V ∈ 𝓝 0, ∃ W ∈ AddGroupFilterBasis.toFilterBasis.sets, V • W ⊆ U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ 𝓝 0, ∃ W ∈ AddGroupFilterBasis.toFilterBasis.sets, V • W ⊆ U