-- 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:
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)

Tactic:
simp_rw [← iUnion_add_left_image, image_add_left]

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 (⋃ a ∈ s, (fun x => -a + x) ⁻¹' V) (⋃ a ∈ t, (fun x => -a + x) ⁻¹' 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
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
haveI : UniformAddGroup E := uniformAddGroup_of_addCommGroup

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
⊢ ∃ 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
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
letI : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E

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
⊢ ∃ 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
⊢ Disjoint (⋃ a ∈ s, (fun x => -a + x) ⁻¹' V) (⋃ a ∈ t, (fun x => -a + x) ⁻¹' V)

Tactic:
simp_rw [UniformSpace.ball, ← preimage_comp, sub_eq_neg_add] at 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
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)