case this
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
n : ℕ
this : ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s

case this
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
exact (eventually_and.1 this).2
case this.zero
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[Nat.zero]) t ⊆ s

case this.succ
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn :
  ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[Nat.succ n]) t ⊆ s
case this
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
induction' n with n ihn generalizing s
case this.succ.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn :
  ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[Nat.succ n]) t ⊆ s
case this.succ
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn :
  ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[Nat.succ n]) t ⊆ s
rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩
case this.succ.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn :
  ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : Set (α × α)
hU : U ⊆ t ∧ ((fun x x_1 => x ○ x_1) U^[n]) U ⊆ t
⊢ U ⊆ s ∧ ((fun x x_1 => x ○ x_1) U^[Nat.succ n]) U ⊆ s
case this.succ.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn :
  ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[Nat.succ n]) t ⊆ s
refine' (ihn htU).mono fun U hU => _
case this.succ.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn :
  ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : Set (α × α)
hU : U ⊆ t ∧ ((fun x x_1 => x ○ x_1) U^[n]) U ⊆ t
⊢ U ⊆ s ∧ (fun x x_1 => x ○ x_1) U (((fun x x_1 => x ○ x_1) U^[n]) U) ⊆ s
case this.succ.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn :
  ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : Set (α × α)
hU : U ⊆ t ∧ ((fun x x_1 => x ○ x_1) U^[n]) U ⊆ t
⊢ U ⊆ s ∧ ((fun x x_1 => x ○ x_1) U^[Nat.succ n]) U ⊆ s
rw [Function.iterate_succ_apply']
no goals
case this.succ.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
n : ℕ
ihn :
  ∀ {s : Set (α × α)}, s ∈ 𝓤 α → ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[n]) t ⊆ s
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : Set (α × α)
hU : U ⊆ t ∧ ((fun x x_1 => x ○ x_1) U^[n]) U ⊆ t
⊢ U ⊆ s ∧ (fun x x_1 => x ○ x_1) U (((fun x x_1 => x ○ x_1) U^[n]) U) ⊆ s
exact
  ⟨hU.1.trans <| (subset_comp_self <| refl_le_uniformity htU).trans hts,
    (compRel_mono hU.1 hU.2).trans hts⟩
no goals
case this.zero
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.45668
inst✝ : UniformSpace α
s✝ : Set (α × α)
hs✝ : s✝ ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : Set (α × α)) in smallSets (𝓤 α), t ⊆ s ∧ ((fun x x_1 => x ○ x_1) t^[Nat.zero]) t ⊆ s
simpa