awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
⊢ Eq.{u_2 + 1} (α := Set X) (⋃₀ {K : Set X | IsCompact K}) univ

Tactic:
exact eq_univ_iff_forall.mpr (fun x ↦ mem_sUnion_of_mem (mem_singleton x) isCompact_singleton)

Premises used: Iff.mpr, Set.mem_singleton, Set.eq_univ_iff_forall, Set.mem_sUnion_of_mem
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
⊢ ∀ (K : Set X), Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} K → IsCompact K

Tactic:
fun _ ↦ id

Premises used: Set.Mem, setOf, id, IsCompact
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
⊢ ∀ (K : Set X), Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} K → IsCompact K

Tactic:
exact fun _ ↦ id

Premises used: id
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
⊢ ∀ (K : Set X),
    Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} K →
      EquicontinuousOn (ι := (↑S : Type (max u_2 u_3))) (α := α)
        (comp (β :=
          { x : (a : X) → α //
            Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x })
          (Subtype.val (p := fun (x : (a : X) → α) ↦
            Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x))
          (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
            (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3))))
        K

Tactic:
fun K _ ↦ hS2.equicontinuousOn K

Premises used: Equicontinuous.equicontinuousOn
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
⊢ ∀ (K : Set X),
    Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} K →
      EquicontinuousOn (ι := (↑S : Type (max u_2 u_3))) (α := α)
        (comp (β :=
          { x : (a : X) → α //
            Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x })
          (Subtype.val (p := fun (x : (a : X) → α) ↦
            Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x))
          (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
            (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3))))
        K

Tactic:
exact fun K _ ↦ hS2.equicontinuousOn K

Premises used: Equicontinuous.equicontinuousOn
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
arg : s ○ t
| IsOpen[instTopologicalSpaceProd] (s ○ t)

Tactic:
arg 1
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
h :
  ∀ (fst : α) (snd : γ),
    (fst, snd) ∈ s ○ t ↔
      Membership.mem (γ := Set (α × γ))
        (⋃ (b : β), (fun (p : α × γ) ↦ (p.1, b)) ⁻¹' s ∩ (fun (p : α × γ) ↦ (b, p.2)) ⁻¹' t) (fst, snd)
⊢ s ○ t = ⋃ (b : β), (fun (p : α × γ) ↦ (p.1, b)) ⁻¹' s ∩ (fun (p : α × γ) ↦ (b, p.2)) ⁻¹' t

Tactic:
ext ⟨_, _⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
fst : α
snd : γ
⊢ (fst, snd) ∈ s ○ t ↔
    Membership.mem (γ := Set (α × γ))
      (⋃ (b : β), (fun (p : α × γ) ↦ (p.1, b)) ⁻¹' s ∩ (fun (p : α × γ) ↦ (b, p.2)) ⁻¹' t) (fst, snd)

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
arg arg₁ : s ○ t
| IsOpen[instTopologicalSpaceProd] (s ○ t)

Tactic:
arg 1; equals ⋃ b, (fun p => (p.1, b)) ⁻¹' s ∩ (fun p => (b, p.2)) ⁻¹' t => ext ⟨_, _⟩; simp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
conv :
  IsOpen[instTopologicalSpaceProd] (⋃ (b : β), (fun (p : α × γ) ↦ (p.1, b)) ⁻¹' s ∩ (fun (p : α × γ) ↦ (b, p.2)) ⁻¹' t)
⊢ IsOpen[instTopologicalSpaceProd] (s ○ t)

Tactic:
conv =>
    arg 1; equals ⋃ b, (fun p => (p.1, b)) ⁻¹' s ∩ (fun p => (b, p.2)) ⁻¹' t => ext ⟨_, _⟩; simp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
a : β
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : α × γ) ↦ (p.1, a)

Tactic:
fun_prop
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
a : β
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : α × γ) ↦ (a, p.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
⊢ IsOpen[instTopologicalSpaceProd] (⋃ (b : β), (fun (p : α × γ) ↦ (p.1, b)) ⁻¹' s ∩ (fun (p : α × γ) ↦ (b, p.2)) ⁻¹' t)

Tactic:
exact isOpen_iUnion fun a ↦ hs.preimage (by fun_prop) |>.inter <| ht.preimage (by fun_prop)

Premises used: isOpen_iUnion, IsOpen.inter, IsOpen.preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
⊢ IsOpen[instTopologicalSpaceProd] s.inv

Tactic:
hs.preimage continuous_swap

Premises used: SetRel.inv, continuous_swap, IsOpen.preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
simp_rw : IsOpen[inst_1] (⋃ i ∈ t, {x : β | (i, x) ∈ s})
⊢ IsOpen[inst_1] (s.image t)

Tactic:
simp_rw [SetRel.image, ← exists_prop, Set.setOf_exists]

Premises used: Set.setOf_exists, exists_prop, SetRel.image
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
⊢ IsOpen[inst_1] (⋃ i ∈ t, {x : β | (i, x) ∈ s})

Tactic:
isOpen_biUnion fun _ _ => hs.preimage <| .prodMk_right _

Premises used: Continuous.prodMk_right, isOpen_biUnion, IsOpen.preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
⊢ IsOpen[inst_1] (⋃ i ∈ t, {x : β | (i, x) ∈ s})

Tactic:
exact isOpen_biUnion fun _ _ => hs.preimage <| .prodMk_right _

Premises used: Continuous.prodMk_right, isOpen_biUnion, IsOpen.preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set β
⊢ IsOpen[inst] (s.preimage t)

Tactic:
hs.relInv.relImage

Premises used: IsOpen.relInv, Set.Mem, SetRel.inv, setOf, Set.preimage, IsOpen.relImage, SetRel.preimage, Prod.swap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
⊢ IsClosed[instTopologicalSpaceProd] s.inv

Tactic:
hs.preimage continuous_swap

Premises used: SetRel.inv, continuous_swap, IsClosed.preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set α
ht : t.Finite
simp_rw : IsClosed[inst_1] (⋃ i ∈ t, {x : β | (i, x) ∈ s})
⊢ IsClosed[inst_1] (s.image t)

Tactic:
simp_rw [SetRel.image, ← exists_prop, Set.setOf_exists]

Premises used: Set.setOf_exists, exists_prop, SetRel.image
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set α
ht : t.Finite
⊢ IsClosed[inst_1] (⋃ i ∈ t, {x : β | (i, x) ∈ s})

Tactic:
ht.isClosed_biUnion fun _ _ => hs.preimage <| .prodMk_right _

Premises used: Continuous.prodMk_right, IsClosed.preimage, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set α
ht : t.Finite
⊢ IsClosed[inst_1] (⋃ i ∈ t, {x : β | (i, x) ∈ s})

Tactic:
exact ht.isClosed_biUnion fun _ _ => hs.preimage <| .prodMk_right _

Premises used: Continuous.prodMk_right, IsClosed.preimage, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set β
ht : t.Finite
⊢ IsClosed[inst] (s.preimage t)

Tactic:
hs.relInv.relImage_of_finite ht

Premises used: IsClosed.relInv, Set.Mem, SetRel.inv, setOf, Set.preimage, SetRel.preimage, Prod.swap, IsClosed.relImage_of_finite
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
n : ℕ
suffices : ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s

Tactic:
suffices ∀ᶠ t in (𝓤 α).smallSets, t ⊆ s ∧ (t ○ ·)^[n] t ⊆ s from (eventually_and.1 this).2
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[0] t ⊆ s

Tactic:
simpa
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
n : ℕ
ihn :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
succ :
  ∀ (t : Set (α × α)) (htU : t ∈ 𝓤 α) (hts : t ○ t ⊆ s),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n + 1] t ⊆ s
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n + 1] t ⊆ s

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

Premises used: comp_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
n : ℕ
ihn :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n + 1] t ⊆ s

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

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
n : ℕ
ihn :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
succ :
  ∀ (U : SetRel α α) (hU : U ⊆ t ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ t),
    U ⊆ s ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n + 1] U ⊆ s
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n + 1] t ⊆ s

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

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
n : ℕ
ihn :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ t
succ : U ⊆ s ∧ U ○ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ s
⊢ U ⊆ s ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n + 1] U ⊆ s

Tactic:
rw [Function.iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
n : ℕ
ihn :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ t
⊢ SetRel.IsRefl t

Tactic:
have := isRefl_of_mem_uniformity htU
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
n : ℕ
ihn :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ t
this : SetRel.IsRefl t
⊢ U ⊆ s ∧ U ○ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ s

Tactic:
⟨hU.1.trans <| SetRel.left_subset_comp.trans hts,
     (SetRel.comp_subset_comp hU.1 hU.2).trans hts⟩

Premises used: SetRel.comp_subset_comp, SetRel.left_subset_comp, HasSubset.Subset.trans, And.right, And.left, And.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
n : ℕ
ihn :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ t
this : SetRel.IsRefl t
⊢ U ⊆ s ∧ U ○ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ s

Tactic:
exact ⟨hU.1.trans <| SetRel.left_subset_comp.trans hts,
     (SetRel.comp_subset_comp hU.1 hU.2).trans hts⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
n : ℕ
zero :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[0] t ⊆ s
succ :
  ∀ (n : ℕ)
    (ihn :
      ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
        ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s)
    {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n + 1] t ⊆ s
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ 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']
    have := isRefl_of_mem_uniformity htU
    exact ⟨hU.1.trans <| SetRel.left_subset_comp.trans hts,
     (SetRel.comp_subset_comp hU.1 hU.2).trans hts⟩

Premises used: Function.iterate_succ_apply', comp_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ○ t ⊆ s

Tactic:
eventually_uniformity_iterate_comp_subset hs 1

Premises used: Nat.iterate, SetRel.comp, eventually_uniformity_iterate_comp_subset, OfNat.ofNat
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : SetRel α α
hV : IsOpen[instTopologicalSpaceProd] V
⊢ IsOpen[inst.toTopologicalSpace] (ball x V)

Tactic:
hV.preimage <| .prodMk_right _

Premises used: Continuous.prodMk_right, UniformSpace.ball, IsOpen.preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : SetRel α α
hV : IsClosed[instTopologicalSpaceProd] V
⊢ IsClosed[inst.toTopologicalSpace] (ball x V)

Tactic:
hV.preimage <| .prodMk_right _

Premises used: Continuous.prodMk_right, UniformSpace.ball, IsClosed.preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x y : α
rw :
  (𝓝 x ×ˢ 𝓝 y).HasBasis (fun (s : Set (α × α)) ↦ s ∈ 𝓤 α ∧ SetRel.IsSymm s) fun (s : Set (α × α)) ↦ ball x s ×ˢ ball y s
⊢ (𝓝 (x, y)).HasBasis (fun (s : Set (α × α)) ↦ s ∈ 𝓤 α ∧ SetRel.IsSymm s) fun (s : Set (α × α)) ↦ ball x s ×ˢ ball y s

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x y : α
apply :
  ∀ {i j : SetRel α α},
    i ∈ 𝓤 α ∧ i.IsSymm →
      j ∈ 𝓤 α ∧ j.IsSymm → ∃ (k : SetRel α α), (k ∈ 𝓤 α ∧ k.IsSymm) ∧ ball x k ⊆ ball x i ∧ ball y k ⊆ ball y j
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (fun (s : Set (α × α)) ↦ s ∈ 𝓤 α ∧ SetRel.IsSymm s) fun (s : Set (α × α)) ↦ ball x s ×ˢ ball y s

Tactic:
apply (hasBasis_nhds x).prod_same_index (hasBasis_nhds y)

Premises used: UniformSpace.hasBasis_nhds, Filter.HasBasis.prod_same_index
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x y : α
U V : SetRel α α
U_in : U ∈ 𝓤 α
U_symm : U.IsSymm
V_in : V ∈ 𝓤 α
V_symm : V.IsSymm
⊢ ∃ (k : SetRel α α), (k ∈ 𝓤 α ∧ k.IsSymm) ∧ ball x k ⊆ ball x U ∧ ball y k ⊆ ball y V

Tactic:
⟨U ∩ V, ⟨(𝓤 α).inter_sets U_in V_in, inferInstance⟩, ball_inter_left x U V,
    ball_inter_right y U V⟩

Premises used: UniformSpace.ball_inter_right, uniformity, inferInstance, Filter.inter_sets, Inter.inter, UniformSpace.ball_inter_left, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x y : α
U V : SetRel α α
U_in : U ∈ 𝓤 α
U_symm : U.IsSymm
V_in : V ∈ 𝓤 α
V_symm : V.IsSymm
⊢ ∃ (k : SetRel α α), (k ∈ 𝓤 α ∧ k.IsSymm) ∧ ball x k ⊆ ball x U ∧ ball y k ⊆ ball y V

Tactic:
exact ⟨U ∩ V, ⟨(𝓤 α).inter_sets U_in V_in, inferInstance⟩, ball_inter_left x U V,
    ball_inter_right y U V⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
a b : α
hg₁ :
  ∀ (s : Set (α × α)),
    Monotone (β := Set (α × α)) fun (t : Set (α × α)) ↦
      SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}
hg₂ :
  ∀ (t : Set (α × α)),
    Monotone (β := Set (α × α)) fun (s : Set (α × α)) ↦
      SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}
⊢ 𝓝 (a, b) =
    (𝓤 α).lift' fun (s : SetRel α α) ↦ SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ s}

Tactic:
rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift']

Premises used: nhds_nhds_eq_uniformity_uniformity_prod, Filter.lift_lift'_same_eq_lift', nhds_prod_eq
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
a b : α
⊢ ∀ (s : Set (α × α)),
    Monotone (β := Set (α × α)) fun (t : Set (α × α)) ↦
      SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}

Tactic:
fun s => monotone_const.set_prod monotone_preimage

Premises used: monotone_const, Monotone.set_prod, Set.monotone_preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
a b : α
⊢ ∀ (s : Set (α × α)),
    Monotone (β := Set (α × α)) fun (t : Set (α × α)) ↦
      SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}

Tactic:
exact fun s => monotone_const.set_prod monotone_preimage

Premises used: monotone_const, Monotone.set_prod, Set.monotone_preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
a b : α
⊢ ∀ (t : Set (α × α)),
    Monotone (β := Set (α × α)) fun (s : Set (α × α)) ↦
      SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}

Tactic:
fun t => Monotone.set_prod ?_ monotone_const

Premises used: monotone_const, Monotone.set_prod
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
a b : α
hg₂ : ∀ (t : Set (α × α)), Monotone (β := Set α) fun (s : Set (α × α)) ↦ {y : α | (y, a) ∈ s}
⊢ ∀ (t : Set (α × α)),
    Monotone (β := Set (α × α)) fun (s : Set (α × α)) ↦
      SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}

Tactic:
refine fun t => Monotone.set_prod ?_ monotone_const

Premises used: monotone_const, Monotone.set_prod
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
a b : α
t : Set (α × α)
⊢ Monotone (β := Set α) fun (s : Set (α × α)) ↦ {y : α | (y, a) ∈ s}

Tactic:
monotone_preimage (f := fun y => (y, a))

Premises used: Set.Mem, setOf, Set.preimage, Set.monotone_preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
a b : α
t : Set (α × α)
⊢ Monotone (β := Set α) fun (s : Set (α × α)) ↦ {y : α | (y, a) ∈ s}

Tactic:
exact monotone_preimage (f := fun y => (y, a))

Premises used: Set.monotone_preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x_1 : α × α
x y : α
hp : (x, y) ∈ s
rw : ∃ t ∈ 𝓤 α, SProd.sprod (α := Set α) (β := Set α) {y : α | (y, x) ∈ t} {y_1 : α | (y, y_1) ∈ t} ⊆ cl_d
hh :
  Monotone (β := Set (α × α)) fun (s : SetRel α α) ↦
    SProd.sprod (α := Set α) (β := Set α) {y : α | (y, x) ∈ s} {y_1 : α | (y, y_1) ∈ s}
⊢ cl_d ∈ 𝓝 (x, y)

Tactic:
rw [nhds_eq_uniformity_prod, mem_lift'_sets]

Premises used: Filter.mem_lift'_sets, nhds_eq_uniformity_prod
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x_1 : α × α
x y : α
hp : (x, y) ∈ s
⊢ ∃ t ∈ 𝓤 α, SProd.sprod (α := Set α) (β := Set α) {y : α | (y, x) ∈ t} {y_1 : α | (y, y_1) ∈ t} ⊆ cl_d

Tactic:
⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩

Premises used: _private.0.nhdset_of_mem_uniformity.match_2, Membership.mem, Prod.mk, _private.0.nhdset_of_mem_uniformity.match_3, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x_1 : α × α
x y : α
hp : (x, y) ∈ s
⊢ ∃ t ∈ 𝓤 α, SProd.sprod (α := Set α) (β := Set α) {y : α | (y, x) ∈ t} {y_1 : α | (y, y_1) ∈ t} ⊆ cl_d

Tactic:
exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩