-- Mathlib/Topology/Algebra/Module/LocallyConvex.lean
theorem Disjoint.exists_open_convexes [LocallyConvexSpace 𝕜 E] {s t : Set E} (disj : Disjoint s t)
    (hs₁ : Convex 𝕜 s) (hs₂ : IsCompact s) (ht₁ : Convex 𝕜 t) (ht₂ : IsClosed t) :
    ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : (uniformity E).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
rcases disj.exists_uniform_thickening_of_basis this hs₂ ht₂ with ⟨V, ⟨hV0, hVopen, hVconvex⟩, hV⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : (uniformity E).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i
V : Set E
hV :
  Disjoint (⋃ x ∈ s, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V))
    (⋃ x ∈ t, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : (uniformity E).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i
V : Set E
hV :
  Disjoint (⋃ x ∈ s, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V))
    (⋃ x ∈ t, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
refine ⟨s + V, t + V, hVopen.add_left, hVopen.add_left, hs₁.add hVconvex, ht₁.add hVconvex,
  subset_add_left _ hV0, subset_add_left _ hV0, ?_⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : (uniformity E).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i
V : Set E
hV :
  Disjoint (⋃ x ∈ s, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V))
    (⋃ x ∈ t, UniformSpace.ball x ((fun x => x.2 - x.1) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
⊢ Disjoint (s + V) (t + V)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this :
  (comap (fun x => x.2 - x.1) (𝓝 0)).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i =>
    (fun x => x.2 - x.1) ⁻¹' id i
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
rw [← uniformity_eq_comap_nhds_zero] at this

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : (uniformity E).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
have := (LocallyConvexSpace.convex_open_basis_zero 𝕜 E).comap fun x : E × E => x.2 - x.1

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this :
  (comap (fun x => x.2 - x.1) (𝓝 0)).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i =>
    (fun x => x.2 - x.1) ⁻¹' id i
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : (uniformity E).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.2 - x.1) ⁻¹' id i
V : Set E
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
hV :
  Disjoint (⋃ x ∈ s, (fun x => -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V) (⋃ x ∈ t, (fun x => -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V)
⊢ Disjoint (⋃ a ∈ s, (fun x => -a + x) ⁻¹' V) (⋃ a ∈ t, (fun x => -a + x) ⁻¹' V)

Tactic:
exact hV

Result:
no goals