awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
⊢ ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (α := CauchyFilter X) ((CauchyFilter.gen ∘ id) i)

Tactic:
exact fun _ ⟨_, hU, _⟩ ↦ by simp; infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
x : SetRel X X
h : x ∈ 𝓤 X ∧ x.IsSymm ∧ x.IsTrans
left : x ∈ 𝓤 X
left_1 : x.IsSymm
hU : x.IsTrans
simp : SetRel.IsTrans (α := CauchyFilter X) (CauchyFilter.gen x)
⊢ SetRel.IsTrans (α := CauchyFilter X) ((CauchyFilter.gen ∘ id) x)

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
x : SetRel X X
h : x ∈ 𝓤 X ∧ x.IsSymm ∧ x.IsTrans
left : x ∈ 𝓤 X
left_1 : x.IsSymm
hU : x.IsTrans
⊢ SetRel.IsTrans (α := CauchyFilter X) (CauchyFilter.gen x)

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
⊢ ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (α := CauchyFilter X) ((CauchyFilter.gen ∘ id) i)

Tactic:
exact fun _ ⟨_, _, hU⟩ ↦ by simp; infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
inst : UniformSpace X
⊢ IsUltraUniformity.{u_1} (CauchyFilter X) ↔ IsUltraUniformity X

Tactic:
⟨fun _ ↦ CauchyFilter.isUniformInducing_pureCauchy.isUltraUniformity,
   fun _ ↦ inferInstance⟩

Premises used: CauchyFilter.isUniformInducing_pureCauchy, IsUniformInducing.isUltraUniformity, inferInstance, Iff.intro
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
⊢ HasBasis (α := SeparationQuotient X × SeparationQuotient X)
    (map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (𝓤 X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i

Tactic:
have := IsUltraUniformity.hasBasis.map
    (Prod.map SeparationQuotient.mk (SeparationQuotient.mk (X := X)))
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X)
    (map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (𝓤 X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i

Tactic:
rw [← SeparationQuotient.uniformity_eq] at this

Premises used: SeparationQuotient.uniformity_eq
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
h_symm :
  ∀ (i : SetRel X X),
    i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans →
      SetRel.IsSymm (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i)
h_trans :
  ∀ (i : SetRel X X),
    i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans →
      SetRel.IsTrans (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i)
⊢ IsUltraUniformity.{u_1} (SeparationQuotient X)

Tactic:
apply mk_of_hasBasis this

Premises used: IsUltraUniformity.mk_of_hasBasis
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
x : SetRel X X
h : x ∈ 𝓤 X ∧ x.IsSymm ∧ x.IsTrans
left : x ∈ 𝓤 X
hU : x.IsSymm
right : x.IsTrans
simp : SetRel.IsSymm (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' x)
⊢ SetRel.IsSymm (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id x)

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
x : SetRel X X
h : x ∈ 𝓤 X ∧ x.IsSymm ∧ x.IsTrans
left : x ∈ 𝓤 X
hU : x.IsSymm
right : x.IsTrans
⊢ SetRel.IsSymm (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' x)

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ ∀ (i : SetRel X X),
    i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans →
      SetRel.IsSymm (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i)

Tactic:
exact fun _ ⟨_, hU, _⟩ ↦ by simp; infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left : U.IsSymm
hU : U.IsTrans
h_trans :
  ∀ (a b c : SeparationQuotient X),
    Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
        (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (a, b) →
      Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
          (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (b, c) →
        Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
          (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (a, c)
⊢ SetRel.IsTrans (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U)

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left : U.IsSymm
hU : U.IsTrans
x y z : SeparationQuotient X
h_trans :
  ∀ (x_1 x_2 : X),
    (x_1, x_2) ∈ U →
      SeparationQuotient.mk x_1 = x →
        SeparationQuotient.mk x_2 = y →
          ∀ (x_3 x_4 : X),
            (x_3, x_4) ∈ U →
              SeparationQuotient.mk x_3 = y →
                SeparationQuotient.mk x_4 = z →
                  ∃ (a : X) (b : X), (a, b) ∈ U ∧ SeparationQuotient.mk a = x ∧ SeparationQuotient.mk b = z
⊢ Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
      (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (x, y) →
    Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
        (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (y, z) →
      Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
        (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (x, z)

Tactic:
simp only [id_eq, Set.mem_image, Prod.exists, Prod.map_apply, Prod.mk.injEq,
      forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_image, forall_exists_index, Prod.mk.injEq, Prod.map_apply, Prod.exists, id_eq
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : Eq (α := SeparationQuotient X) (SeparationQuotient.mk c) (SeparationQuotient.mk b)
⊢ ∀ s ∈ 𝓤 X, (b, c) ∈ s

Tactic:
rw [eq_comm, SeparationQuotient.mk_eq_mk, inseparable_iff_ker_uniformity,
          Filter.mem_ker] at hc

Premises used: SeparationQuotient.mk_eq_mk, inseparable_iff_ker_uniformity, Filter.mem_ker, eq_comm
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : ∀ s ∈ 𝓤 X, (b, c) ∈ s
⊢ (b, c) ∈ U

Tactic:
hc _ hU'
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : ∀ s ∈ 𝓤 X, (b, c) ∈ s
⊢ (b, c) ∈ U

Tactic:
exact hc _ hU'
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : Eq (α := SeparationQuotient X) (SeparationQuotient.mk c) (SeparationQuotient.mk b)
⊢ (b, c) ∈ U

Tactic:
have hbc : (b, c) ∈ U := by
      rw [eq_comm, SeparationQuotient.mk_eq_mk, inseparable_iff_ker_uniformity,
          Filter.mem_ker] at hc
      exact hc _ hU'
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : Eq (α := SeparationQuotient X) (SeparationQuotient.mk c) (SeparationQuotient.mk b)
hbc : (b, c) ∈ U
⊢ Eq (α := SeparationQuotient X) (SeparationQuotient.mk a) (SeparationQuotient.mk a)

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : Eq (α := SeparationQuotient X) (SeparationQuotient.mk c) (SeparationQuotient.mk b)
hbc : (b, c) ∈ U
⊢ Eq (α := SeparationQuotient X) (SeparationQuotient.mk d) (SeparationQuotient.mk d)

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : Eq (α := SeparationQuotient X) (SeparationQuotient.mk c) (SeparationQuotient.mk b)
hbc : (b, c) ∈ U
⊢ ∃ (a_1 : X) (b : X),
    (a_1, b) ∈ U ∧
      Eq (α := SeparationQuotient X) (SeparationQuotient.mk a_1) (SeparationQuotient.mk a) ∧
        Eq (α := SeparationQuotient X) (SeparationQuotient.mk b) (SeparationQuotient.mk d)

Tactic:
exact ⟨a, d, U.trans (U.trans hab hbc) hcd, by simp, by simp⟩
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
inst : UniformSpace X
⊢ IsUltraUniformity.{u_1} (SeparationQuotient X) ↔ IsUltraUniformity X

Tactic:
⟨fun _ ↦ SeparationQuotient.isUniformInducing_mk.isUltraUniformity,
   fun _ ↦ inferInstance⟩

Premises used: SeparationQuotient.isUniformInducing_mk, IsUniformInducing.isUltraUniformity, inferInstance, Iff.intro
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
inst : UniformSpace X
rw : IsUltraUniformity.{u_1} (SeparationQuotient (CauchyFilter X)) ↔ IsUltraUniformity.{u_1} (UniformSpace.Completion X)
⊢ IsUltraUniformity.{u_1} (UniformSpace.Completion X) ↔ IsUltraUniformity X

Tactic:
rw [iff_comm, ← cauchyFilter_iff, ← separationQuotient_iff]

Premises used: iff_comm, IsUltraUniformity.separationQuotient_iff, IsUltraUniformity.cauchyFilter_iff
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
inst : UniformSpace X
⊢ IsUltraUniformity.{u_1} (SeparationQuotient (CauchyFilter X)) ↔ IsUltraUniformity.{u_1} (UniformSpace.Completion X)

Tactic:
Iff.rfl

Premises used: Iff.rfl, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
inst : UniformSpace X
⊢ IsUltraUniformity.{u_1} (SeparationQuotient (CauchyFilter X)) ↔ IsUltraUniformity.{u_1} (UniformSpace.Completion X)

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
⊢ IsUltraUniformity.{u_1} (UniformSpace.Completion X)

Tactic:
completion_iff.2 inferInstance

Premises used: Iff.mpr, inferInstance, IsUltraUniformity.completion_iff
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ IsUltraUniformity X

Tactic:
.mk_of_hasBasis (h.hasBasis.comap (Prod.map f f)) ?_ ?_

Premises used: Prod.map, Filter.HasBasis.comap, IsUltraUniformity.mk_of_hasBasis, IsUltraUniformity.hasBasis
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
refine_1 : ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (Prod.map f f ⁻¹' id i)
refine_2 : ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (Prod.map f f ⁻¹' id i)
⊢ IsUltraUniformity X

Tactic:
refine .mk_of_hasBasis (h.hasBasis.comap (Prod.map f f)) ?_ ?_
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
i : SetRel Y Y
left : i ∈ uniformity Y
left_1 : i.IsSymm
right : i.IsTrans
⊢ SetRel.IsSymm (Prod.map f f ⁻¹' i)

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
i : SetRel Y Y
left : i ∈ uniformity Y
left_1 : i.IsSymm
right : i.IsTrans
⊢ SetRel.IsTrans (Prod.map f f ⁻¹' i)

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ IsUltraUniformity X

Tactic:
.mk_of_hasBasis (h.hasBasis.inf h'.hasBasis) ?_ ?_

Premises used: Filter.HasBasis.inf, IsUltraUniformity.mk_of_hasBasis, IsUltraUniformity.hasBasis
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
refine_1 :
  ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsSymm (id i.1 ∩ id i.2)
refine_2 :
  ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsTrans (id i.1 ∩ id i.2)
⊢ IsUltraUniformity X

Tactic:
refine .mk_of_hasBasis (h.hasBasis.inf h'.hasBasis) ?_ ?_
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
i : SetRel X X × SetRel X X
left : i.1 ∈ uniformity X
left_1 : i.1.IsSymm
right : i.1.IsTrans
left_2 : i.2 ∈ uniformity X
left_3 : i.2.IsSymm
right_1 : i.2.IsTrans
⊢ SetRel.IsSymm (i.1 ∩ i.2)

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
i : SetRel X X × SetRel X X
left : i.1 ∈ uniformity X
left_1 : i.1.IsSymm
right : i.1.IsTrans
left_2 : i.2 ∈ uniformity X
left_3 : i.2.IsSymm
right_1 : i.2.IsTrans
⊢ SetRel.IsTrans (i.1 ∩ i.2)

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
inst_3 : IsUltraUniformity Y
⊢ IsUltraUniformity (X × Y)

Tactic:
.inf (.comap ‹_› _) (.comap ‹_› _)

Premises used: IsUltraUniformity.inf, IsUltraUniformity.comap
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
ι : Type u_3
U : (i : ι) → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ (i : ι), U i
⊢ IsUltraUniformity X

Tactic:
.mk_of_hasBasis (iInf_uniformity ▸ Filter.HasBasis.iInf fun i ↦ (hU i).hasBasis) ?_ ?_

Premises used: IsUltraUniformity.mk_of_hasBasis
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
ι : Type u_3
U : (i : ι) → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ (i : ι), U i
refine_1 :
  ∀ (i : (I : Set ι) × ((i : (↑I : Type u_3)) → SetRel X X)),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1 ∈ uniformity X ∧
            (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsSymm ∧
              (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsTrans) →
      SetRel.IsSymm.{u_1} (α := X)
        (⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          id (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1))
refine_2 :
  ∀ (i : (I : Set ι) × ((i : (↑I : Type u_3)) → SetRel X X)),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1 ∈ uniformity X ∧
            (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsSymm ∧
              (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsTrans) →
      SetRel.IsTrans.{u_1} (α := X)
        (⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          id (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1))
⊢ IsUltraUniformity X

Tactic:
refine .mk_of_hasBasis (iInf_uniformity ▸ Filter.HasBasis.iInf fun i ↦ (hU i).hasBasis) ?_ ?_
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
ι : Type u_3
U : (i : ι) → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ (i : ι), U i
refine_1 :
  ∀ (i : (I : Set ι) × ((i : (↑I : Type u_3)) → SetRel X X)),
    i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite →
      (∀ (a : ι) (b : a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
          i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
              (Subtype.mk (p := fun (a : ι) ↦ a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) a
                b) ∈
            uniformity X) →
        (∀ (a : ι) (b : a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
            (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
                (Subtype.mk (p := fun (a : ι) ↦ a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) a
                  b)).IsSymm) →
          (∀ (a : ι) (b : a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
              (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
                  (Subtype.mk (p := fun (a : ι) ↦ a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X))
                    a b)).IsTrans) →
            SetRel.IsSymm.{u_1} (α := X)
              (⋂ (i_1 : ι),
                ⋂ (h : i_1 ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
                  i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
                    (Subtype.mk (p := fun (x : ι) ↦
                      x ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) i_1 h))
⊢ ∀ (i : (I : Set ι) × ((i : (↑I : Type u_3)) → SetRel X X)),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1 ∈ uniformity X ∧
            (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsSymm ∧
              (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsTrans) →
      SetRel.IsSymm.{u_1} (α := X)
        (⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          id (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1))

Tactic:
simp only [forall_and, Subtype.forall, id_eq, Set.iInter_coe_set, and_imp]

Premises used: and_imp, Subtype.forall, Set.iInter_coe_set, forall_and, id_eq