-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem basisSets_intersect (U V : Set E) (hU : U ∈ p.basisSets) (hV : V ∈ p.basisSets) :
    ∃ z ∈ p.basisSets, z ⊆ U ∩ V

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 ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV✝ : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ((s ∪ t).sup p).ball 0 (r₁ ⊓ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (r₁ ⊓ r₂) ⊆ U ∩ V

Tactic:
refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩

Result:
case h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV✝ : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ((s ∪ t).sup p).ball 0 (r₁ ⊓ r₂) ⊆ U ∩ V

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

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 ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

Tactic:
classical
  rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩
  rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩
  use ((s ∪ t).sup p).ball 0 (min r₁ r₂)
  refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩
  rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
    ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]
  exact
    Set.subset_inter
      (Set.iInter₂_mono' fun i hi =>
        ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
      (Set.iInter₂_mono' fun i hi =>
        ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV✝ : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

Tactic:
use ((s ∪ t).sup p).ball 0 (min r₁ r₂)

Result:
case h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV✝ : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ((s ∪ t).sup p).ball 0 (r₁ ⊓ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (r₁ ⊓ r₂) ⊆ U ∩ V

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 ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV✝ : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ⋂ i ∈ s ∪ t, (p i).ball 0 (r₁ ⊓ r₂) ⊆ (⋂ i ∈ s, (p i).ball 0 r₁) ∩ ⋂ i ∈ t, (p i).ball 0 r₂

Tactic:
exact
  Set.subset_inter
    (Set.iInter₂_mono' fun i hi =>
      ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
    (Set.iInter₂_mono' fun i hi =>
      ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)

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 ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

Tactic:
rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩

Result:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV✝ : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

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 ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV✝ : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ((s ∪ t).sup p).ball 0 (r₁ ⊓ r₂) ⊆ U ∩ V

Tactic:
rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
  ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]

Result:
case h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV✝ : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ⋂ i ∈ s ∪ t, (p i).ball 0 (r₁ ⊓ r₂) ⊆ (⋂ i ∈ s, (p i).ball 0 r₁) ∩ ⋂ i ∈ t, (p i).ball 0 r₂