-- Mathlib/Topology/UniformSpace/Basic.lean
theorem eventually_uniformity_iterate_comp_subset {s : Set (α × α)} (hs : s ∈ 𝓤 α) (n : ℕ) :
    ∀ᶠ t in (𝓤 α).smallSets, (t ○ ·)^[n] t ⊆ s

Proof state:
case succ
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n✝] t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n✝ + 1] t ⊆ s

Tactic:
rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩

Result:
case succ.intro.intro
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n✝] t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
⊢ ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n✝ + 1] t ⊆ s

Proof state:
case succ.intro.intro
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n✝] t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
⊢ ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n✝ + 1] t ⊆ s

Tactic:
refine (ihn htU).mono fun U hU => ?_

Result:
case succ.intro.intro
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n✝] t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : Set (α × α)
hU : U ⊆ t ∧ (fun x => U ○ x)^[n✝] U ⊆ t
⊢ U ⊆ s ∧ (fun x => U ○ x)^[n✝ + 1] U ⊆ s

Proof state:
case succ.intro.intro
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n✝] t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : Set (α × α)
hU : U ⊆ t ∧ (fun x => U ○ x)^[n✝] U ⊆ t
⊢ U ⊆ s ∧ U ○ (fun x => U ○ x)^[n✝] U ⊆ s

Tactic:
exact
  ⟨hU.1.trans <| (subset_comp_self <| refl_le_uniformity htU).trans hts,
    (compRel_mono hU.1 hU.2).trans hts⟩

Result:
no goals

Proof state:
case succ.intro.intro
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n✝] t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : Set (α × α)
hU : U ⊆ t ∧ (fun x => U ○ x)^[n✝] U ⊆ t
⊢ U ⊆ s ∧ (fun x => U ○ x)^[n✝ + 1] U ⊆ s

Tactic:
rw [Function.iterate_succ_apply']

Result:
case succ.intro.intro
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n✝] t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : Set (α × α)
hU : U ⊆ t ∧ (fun x => U ○ x)^[n✝] U ⊆ t
⊢ U ⊆ s ∧ U ○ (fun x => U ○ x)^[n✝] U ⊆ s

Proof state:
case zero
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[0] t ⊆ s

Tactic:
simpa

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x => t ○ x)^[n] t ⊆ s

Tactic:
induction n generalizing s with
| zero => simpa
| succ _ ihn =>
  rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩
  refine (ihn htU).mono fun U hU => ?_
  rw [Function.iterate_succ_apply']
  exact
    ⟨hU.1.trans <| (subset_comp_self <| refl_le_uniformity htU).trans hts,
      (compRel_mono hU.1 hU.2).trans hts⟩

Result:
no goals