-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem basisSets_smul_left (x : 𝕜) (U : Set E) (hU : U ∈ p.basisSets) :
    ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun y : E => x • y) ⁻¹' U

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

Tactic:
rw [(s.sup p).smul_ball_preimage 0 r x h, smul_zero]

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

Proof state:
case h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
⊢ (s.sup p).ball 0 (r / ‖x‖) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧
    (s.sup p).ball 0 (r / ‖x‖) ⊆ (s.sup p).ball 0 (r / ‖x‖)

Tactic:
exact ⟨p.basisSets_mem s (div_pos hr (norm_pos_iff.mpr h)), Subset.rfl⟩

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬x ≠ 0
⊢ ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' (s.sup p).ball 0 r

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

Result:
case neg
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬x ≠ 0
⊢ (s.sup p).ball 0 r ⊆ (fun y => x • y) ⁻¹' (s.sup p).ball 0 r

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 ι
x : 𝕜
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' U

Tactic:
rw [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 ι
x : 𝕜
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' (s.sup p).ball 0 r

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 ι
x : 𝕜
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' (s.sup p).ball 0 r

Tactic:
by_cases h : x ≠ 0

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

case neg
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬x ≠ 0
⊢ ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' (s.sup p).ball 0 r

Proof state:
case neg
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬x ≠ 0
⊢ (s.sup p).ball 0 r ⊆ (fun y => x • y) ⁻¹' (s.sup p).ball 0 r

Tactic:
simp only [not_ne_iff.mp h, Set.subset_def, mem_ball_zero, hr, mem_univ, map_zero, imp_true_iff,
  preimage_const_of_mem, zero_smul]

Result:
no goals

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 ι
x : 𝕜
U : Set E
hU : U ∈ p.basisSets
⊢ ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' 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 ι
x : 𝕜
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' U

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

Tactic:
use (s.sup p).ball 0 (r / ‖x‖)

Result:
case h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
⊢ (s.sup p).ball 0 (r / ‖x‖) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧
    (s.sup p).ball 0 (r / ‖x‖) ⊆ (s.sup p).ball 0 (r / ‖x‖)