-- Mathlib/Topology/UniformSpace/Defs.lean
theorem comp_comp_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ○ t ⊆ s

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
⊢ ∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ○ t ⊆ s

Tactic:
use t, t_in, t_symm

Result:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
⊢ t ○ t ○ t ⊆ s

Proof state:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
⊢ t ○ t ○ t ⊆ s

Tactic:
have : t ⊆ t ○ t := subset_comp_self_of_mem_uniformity t_in

Result:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ t ○ t ○ t ⊆ s

Proof state:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
⊢ t ○ t ○ t ⊆ s

Tactic:
have hw := Subset.refl w

Result:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
hw : w ⊆ w
⊢ t ○ t ○ t ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
hw : w ⊆ w
⊢ w ○ (t ○ t) ⊆ w ○ w

Tactic:
mono

Result:
no goals

Proof state:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
hw : w ⊆ w
⊢ t ○ t ○ t ⊆ s

Tactic:
calc
  t ○ t ○ t ⊆ w ○ t := by mono
  _ ⊆ w ○ (t ○ t) := by mono
  _ ⊆ w ○ w := by mono
  _ ⊆ s := w_sub

Result:
no goals

Proof state:
case intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
⊢ ∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ○ t ⊆ s

Tactic:
rcases comp_symm_mem_uniformity_sets w_in with ⟨t, t_in, t_symm, t_sub⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
⊢ ∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ○ t ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
hw : w ⊆ w
⊢ t ○ t ○ t ⊆ w ○ t

Tactic:
mono

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
hw : w ⊆ w
⊢ w ○ t ⊆ w ○ (t ○ t)

Tactic:
mono

Result:
no goals

Proof state:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ t ○ t ○ t ⊆ s

Tactic:
have ht := Subset.refl t

Result:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SymmetricRel t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
ht : t ⊆ t
⊢ t ○ t ○ t ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ○ t ⊆ s

Tactic:
rcases comp_symm_mem_uniformity_sets hs with ⟨w, w_in, _, w_sub⟩

Result:
case intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left✝ : SymmetricRel w
w_sub : w ○ w ⊆ s
⊢ ∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ○ t ⊆ s