awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
g : α → β
hf : TendstoLocallyUniformly F f p
hg : ∀ (x : α), f x = g x
⊢ TendstoLocallyUniformly F g p

Tactic:
hf.congr_inseparable_right fun x => .of_eq (hg x)

Premises used: TendstoLocallyUniformly.congr_inseparable_right, Inseparable.of_eq
-- Module: Mathlib.Topology.UniformSpace.Matrix
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
inst_1 : AddGroup 𝕜
inst_2 : IsUniformAddGroup 𝕜
⊢ IsUniformAddGroup (Matrix m n 𝕜)

Tactic:
inferInstanceAs <| IsUniformAddGroup (m → n → 𝕜)

Premises used: _private.0.Matrix.instIsUniformAddGroup._proof_1
-- Module: Mathlib.Topology.UniformSpace.Matrix
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
erw :
  Eq (α := Filter (Matrix m n 𝕜 × Matrix m n 𝕜))
    (⨅ (i : m),
      Filter.comap (β := (n → 𝕜) × (n → 𝕜)) (fun (a : ((i : m) → n → 𝕜) × ((i : m) → n → 𝕜)) ↦ (a.1 i, a.2 i))
        (𝓤 (n → 𝕜)))
    (⨅ (i : m), ⨅ (j : n), Filter.comap (fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜))
⊢ Eq (α := Filter (Matrix m n 𝕜 × Matrix m n 𝕜)) (𝓤 (Matrix m n 𝕜))
    (⨅ (i : m), ⨅ (j : n), Filter.comap (fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜))

Tactic:
erw [Pi.uniformity]

Premises used: Pi.uniformity
-- Module: Mathlib.Topology.UniformSpace.Matrix
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
simp_rw :
  Eq (α := Filter (Matrix m n 𝕜 × Matrix m n 𝕜))
    (⨅ (i : m),
      ⨅ (i_1 : n),
        Filter.comap
          ((fun (a : ((i : n) → 𝕜) × ((i : n) → 𝕜)) ↦ (a.1 i_1, a.2 i_1)) ∘
            fun (a : ((i : m) → n → 𝕜) × ((i : m) → n → 𝕜)) ↦ (a.1 i, a.2 i))
          (𝓤 𝕜))
    (⨅ (i : m), ⨅ (j : n), Filter.comap (fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜))
⊢ Eq (α := Filter (Matrix m n 𝕜 × Matrix m n 𝕜))
    (⨅ (i : m),
      Filter.comap (β := (n → 𝕜) × (n → 𝕜)) (fun (a : ((i : m) → n → 𝕜) × ((i : m) → n → 𝕜)) ↦ (a.1 i, a.2 i))
        (𝓤 (n → 𝕜)))
    (⨅ (i : m), ⨅ (j : n), Filter.comap (fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜))

Tactic:
simp_rw [Pi.uniformity, Filter.comap_iInf, Filter.comap_comap]

Premises used: Filter.comap_iInf, Filter.comap_comap, Pi.uniformity
-- Module: Mathlib.Topology.UniformSpace.Matrix
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
⊢ Eq (α := Filter (Matrix m n 𝕜 × Matrix m n 𝕜))
    (⨅ (i : m),
      ⨅ (i_1 : n),
        Filter.comap
          ((fun (a : ((i : n) → 𝕜) × ((i : n) → 𝕜)) ↦ (a.1 i_1, a.2 i_1)) ∘
            fun (a : ((i : m) → n → 𝕜) × ((i : m) → n → 𝕜)) ↦ (a.1 i, a.2 i))
          (𝓤 𝕜))
    (⨅ (i : m), ⨅ (j : n), Filter.comap (fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜))

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Matrix
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
β : Type u_4
inst_1 : UniformSpace β
f : β → Matrix m n 𝕜
simp :
  (∀ (i : m) (i_1 : n),
      Filter.Tendsto
        ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2)) (𝓤 β)
        (𝓤 𝕜)) ↔
    ∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
⊢ UniformContinuous f ↔ ∀ (i : m) (j : n), UniformContinuous.{u_4, u_3} (β := 𝕜) fun (x : β) ↦ f x i j

Tactic:
simp only [UniformContinuous, Matrix.uniformity, Filter.tendsto_iInf, Filter.tendsto_comap_iff]

Premises used: UniformContinuous, Filter.tendsto_comap_iff, Filter.tendsto_iInf, Matrix.uniformity
-- Module: Mathlib.Topology.UniformSpace.Matrix
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
β : Type u_4
inst_1 : UniformSpace β
f : β → Matrix m n 𝕜
mp :
  (∀ (i : m) (i_1 : n),
      Filter.Tendsto
        ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2)) (𝓤 β)
        (𝓤 𝕜)) →
    ∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
mpr :
  (∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)) →
    ∀ (i : m) (i_1 : n),
      Filter.Tendsto
        ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2)) (𝓤 β)
        (𝓤 𝕜)
⊢ (∀ (i : m) (i_1 : n),
      Filter.Tendsto
        ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2)) (𝓤 β)
        (𝓤 𝕜)) ↔
    ∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)

Tactic:
apply Iff.intro

Premises used: Iff.intro
-- Module: Mathlib.Topology.UniformSpace.Matrix
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
β : Type u_4
inst_1 : UniformSpace β
f : β → Matrix m n 𝕜
a :
  ∀ (i : m) (i_1 : n),
    Filter.Tendsto ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2))
      (𝓤 β) (𝓤 𝕜)
⊢ ∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)

Tactic:
apply a
-- Module: Mathlib.Topology.UniformSpace.Matrix
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
β : Type u_4
inst_1 : UniformSpace β
f : β → Matrix m n 𝕜
a : ∀ (i : m) (j : n), Filter.Tendsto (fun (x : β × β) ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)
⊢ ∀ (i : m) (i_1 : n),
    Filter.Tendsto ((fun (a : Matrix m n 𝕜 × Matrix m n 𝕜) ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun (x : β × β) ↦ (f x.1, f x.2))
      (𝓤 β) (𝓤 𝕜)

Tactic:
apply a
-- Module: Mathlib.Topology.UniformSpace.Matrix
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
inst_1 : CompleteSpace 𝕜
⊢ CompleteSpace (Matrix m n 𝕜)

Tactic:
inferInstanceAs <| CompleteSpace (m → n → 𝕜)

Premises used: _private.0.Matrix.instCompleteSpace._proof_1
-- Module: Mathlib.Topology.UniformSpace.Matrix
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : UniformSpace 𝕜
inst_1 : T0Space 𝕜
⊢ T0Space (Matrix m n 𝕜)

Tactic:
inferInstanceAs (T0Space (m → n → 𝕜))

Premises used: _private.0.Matrix.instT0Space._proof_1
-- Module: Mathlib.Topology.UniformSpace.OfFun
Goal:
X : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
hr : r > 0
⊢ Subset.{u_1} (α := Set (X × X)) SetRel.id {x : X × X | d x.1 x.2 < r}

Tactic:
simp [Set.subset_def, *]

Premises used: Set.subset_def
-- Module: Mathlib.Topology.UniformSpace.OfFun
Goal:
X : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
h : r > 0
x : X × X
hx : Membership.mem (γ := Set (X × X)) {x : X × X | d x.1 x.2 < r} x
rwa : d x.swap.1 x.swap.2 < r
rwa₁ rwa₂ rwa₃ rwa₄ : d x.swap.2 x.swap.1 < r
⊢ Membership.mem (γ := Set (X × X)) {x : X × X | d x.1 x.2 < r} x.swap

Tactic:
rwa [mem_setOf, symm]

Premises used: Set.mem_setOf
-- Module: Mathlib.Topology.UniformSpace.OfFun
Goal:
X : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
h₀ : ∃ (x : M), 0 < x
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
⊢ (𝓤 X).HasBasis (fun (x : M) ↦ 0 < x) fun (ε : M) ↦ {x : X × X | d x.1 x.2 < ε}

Tactic:
hasBasis_biInf_principal'
    (fun ε₁ h₁ ε₂ h₂ => ⟨min ε₁ ε₂, lt_min h₁ h₂, fun _x hx => lt_of_lt_of_le hx (min_le_left _ _),
      fun _x hx => lt_of_lt_of_le hx (min_le_right _ _)⟩) h₀

Premises used: iInf, uniformity, lt_min, min_le_left, Filter.hasBasis_biInf_principal', And.intro, min_le_right, Exists.intro, Min.min, lt_of_lt_of_le
-- Module: Mathlib.Topology.UniformSpace.Path
Goal:
X : Type u_1
inst : UniformSpace X
x y : X
γ : Path x y
⊢ UniformContinuous (α := (↑I : Type)) (β := X) (⇑γ : (a : (↑I : Type)) → X)

Tactic:
CompactSpace.uniformContinuous_of_continuous <| map_continuous _

Premises used: CompactSpace.uniformContinuous_of_continuous, ContinuousMapClass.map_continuous
-- Module: Mathlib.Topology.UniformSpace.Path
Goal:
X : Type u_1
inst : UniformSpace X
x y : X
γ : Path x y
⊢ UniformContinuous (α := ℝ) (β := X) (⇑γ.extend : (a : ℝ) → X)

Tactic:
γ.uniformContinuous.comp <| LipschitzWith.projIcc _ |>.uniformContinuous

Premises used: LipschitzWith.projIcc, Path.uniformContinuous, LipschitzWith.uniformContinuous, UniformContinuous.comp, Set.IccExtend
-- Module: Mathlib.Topology.UniformSpace.Path
Goal:
X : Type u_1
inst : UniformSpace X
x y : X
⊢ UniformContinuous.{u_1, u_1} (α := Path x y) extend

Tactic:
ContinuousMap.projIccCM.uniformContinuous_comp_left.comp isUniformEmbedding_coe.uniformContinuous

Premises used: ContinuousMap.uniformContinuous_comp_left, ContinuousMap.comp, ContinuousMap.projIccCM, Set.projIcc, IsUniformEmbedding.toIsUniformInducing, Path.isUniformEmbedding_coe, UniformContinuous.comp, Path.extend, Set.IccExtend, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Path
Goal:
X : Type u_1
inst : UniformSpace X
x y : X
ι : Sort u_2
p : ι → Prop
U : ι → Set (X × X)
hU : (𝓤 X).HasBasis p U
⊢ Filter.HasBasis.{u_1, u_2} (α := Path x y × Path x y) (𝓤 (Path x y)) p fun (i : ι) ↦
    {γ : Path x y × Path x y |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) (U i) (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}

Tactic:
hU.compactConvergenceUniformity_of_compact.comap _

Premises used: Set.Mem, uniformity, setOf, Filter.HasBasis.comap, Set.preimage, Filter.HasBasis.compactConvergenceUniformity_of_compact, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Path
Goal:
X : Type u_1
inst : UniformSpace X
x y : X
⊢ Filter.HasBasis (α := Path x y × Path x y) (𝓤 (Path x y)) (fun (x : Set (X × X)) ↦ x ∈ 𝓤 X) fun (x_1 : Set (X × X)) ↦
    {γ : Path x y × Path x y |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) x_1 (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}

Tactic:
(𝓤 X).basis_sets.uniformityPath

Premises used: Set.Mem, uniformity, setOf, Filter.basis_sets, Filter.HasBasis.uniformityPath
-- Module: Mathlib.Topology.UniformSpace.Path
Goal:
X : Type u_1
inst : UniformSpace X
x y : X
⊢ UniformContinuous.{u_1, u_1} (α := Path x y) symm

Tactic:
hasBasis_uniformity.uniformContinuous_iff hasBasis_uniformity |>.mpr fun U hU ↦
    ⟨U, hU, fun _ _ h x ↦ h (σ x)⟩

Premises used: Iff.mpr, Path.hasBasis_uniformity, And.intro, Filter.HasBasis.uniformContinuous_iff, Exists.intro, unitInterval.symm
-- Module: Mathlib.Topology.UniformSpace.Path
Goal:
X : Type u_1
inst : UniformSpace X
x y z : X
U : Set (X × X)
hU : U ∈ 𝓤 X
x_1 x_2 : Path x y × Path y z
t : (↑I : Type)
fst : Path x y
snd : Path y z
fst_1 : Path x y
snd_1 : Path y z
h :
  Membership.mem (γ := SetRel (Path x y × Path y z) (Path x y × Path y z))
    (entourageProd
      {γ : Path x y × Path x y |
        ∀ (t : (↑I : Type)),
          Membership.mem (α := X × X) (U, U).1
            (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
      {γ : Path y z × Path y z |
        ∀ (t : (↑I : Type)),
          Membership.mem (α := X × X) (U, U).2
            (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)})
    ((fst, snd), fst_1, snd_1)
h₁ :
  Membership.mem (γ := SetRel (Path x y) (Path x y))
    {γ : Path x y × Path x y |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) (U, U).1
          (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
    (fst, fst_1)
h₂ :
  Membership.mem (γ := SetRel (Path y z) (Path y z))
    {γ : Path y z × Path y z |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) (U, U).2
          (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
    (snd, snd_1)
pos :
  ∀ (ht : (↑t : ℝ) ≤ 2⁻¹),
    Membership.mem (α := X × X) U
      ((((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).1 : (a : (↑I : Type)) → X) t,
          ((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).2 : (a : (↑I : Type)) → X) t) :
        X × X)
neg :
  ∀ (ht : ¬(↑t : ℝ) ≤ 2⁻¹),
    Membership.mem (α := X × X) U
      ((((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).1 : (a : (↑I : Type)) → X) t,
          ((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).2 : (a : (↑I : Type)) → X) t) :
        X × X)
⊢ Membership.mem (α := X × X) U
    ((((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).1 : (a : (↑I : Type)) → X) t,
        ((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).2 : (a : (↑I : Type)) → X) t) :
      X × X)

Tactic:
by_cases ht : (t : ℝ) ≤ 2⁻¹

Premises used: Subtype.val
-- Module: Mathlib.Topology.UniformSpace.Path
Goal:
X : Type u_1
inst : UniformSpace X
x y z : X
U : Set (X × X)
hU : U ∈ 𝓤 X
x_1 x_2 : Path x y × Path y z
t : (↑I : Type)
fst : Path x y
snd : Path y z
fst_1 : Path x y
snd_1 : Path y z
h :
  Membership.mem (γ := SetRel (Path x y × Path y z) (Path x y × Path y z))
    (entourageProd
      {γ : Path x y × Path x y |
        ∀ (t : (↑I : Type)),
          Membership.mem (α := X × X) (U, U).1
            (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
      {γ : Path y z × Path y z |
        ∀ (t : (↑I : Type)),
          Membership.mem (α := X × X) (U, U).2
            (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)})
    ((fst, snd), fst_1, snd_1)
h₁ :
  Membership.mem (γ := SetRel (Path x y) (Path x y))
    {γ : Path x y × Path x y |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) (U, U).1
          (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
    (fst, fst_1)
h₂ :
  Membership.mem (γ := SetRel (Path y z) (Path y z))
    {γ : Path y z × Path y z |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) (U, U).2
          (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
    (snd, snd_1)
ht : (↑t : ℝ) ≤ 2⁻¹
⊢ Membership.mem (α := X × X) U
    ((((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).1 : (a : (↑I : Type)) → X) t,
        ((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).2 : (a : (↑I : Type)) → X) t) :
      X × X)

Tactic:
simp [Path.trans_apply, ht, h₁ _, h₂ _]

Premises used: Path.trans_apply
-- Module: Mathlib.Topology.UniformSpace.Path
Goal:
X : Type u_1
inst : UniformSpace X
x y z : X
U : Set (X × X)
hU : U ∈ 𝓤 X
x_1 x_2 : Path x y × Path y z
t : (↑I : Type)
fst : Path x y
snd : Path y z
fst_1 : Path x y
snd_1 : Path y z
h :
  Membership.mem (γ := SetRel (Path x y × Path y z) (Path x y × Path y z))
    (entourageProd
      {γ : Path x y × Path x y |
        ∀ (t : (↑I : Type)),
          Membership.mem (α := X × X) (U, U).1
            (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
      {γ : Path y z × Path y z |
        ∀ (t : (↑I : Type)),
          Membership.mem (α := X × X) (U, U).2
            (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)})
    ((fst, snd), fst_1, snd_1)
h₁ :
  Membership.mem (γ := SetRel (Path x y) (Path x y))
    {γ : Path x y × Path x y |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) (U, U).1
          (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
    (fst, fst_1)
h₂ :
  Membership.mem (γ := SetRel (Path y z) (Path y z))
    {γ : Path y z × Path y z |
      ∀ (t : (↑I : Type)),
        Membership.mem (α := X × X) (U, U).2
          (((γ.1 : (a : (↑I : Type)) → X) t, (γ.2 : (a : (↑I : Type)) → X) t) : X × X)}
    (snd, snd_1)
ht : ¬(↑t : ℝ) ≤ 2⁻¹
⊢ Membership.mem (α := X × X) U
    ((((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).1 : (a : (↑I : Type)) → X) t,
        ((Function.uncurry trans (fst, snd), Function.uncurry trans (fst_1, snd_1)).2 : (a : (↑I : Type)) → X) t) :
      X × X)

Tactic:
simp [Path.trans_apply, ht, h₁ _, h₂ _]

Premises used: Path.trans_apply
-- Module: Mathlib.Topology.UniformSpace.Path
Goal:
X : Type u_1
inst : UniformSpace X
x y z : X
inst_1 : CompleteSpace X
⊢ IsComplete (α := C((↑I : Type), X)) (Set.range (ι := Path x y) _root_.toContinuousMap)

Tactic:
simpa [Set.EqOn, range_coe]
    using ContinuousMap.isComplete_setOf_eqOn (Function.update (fun _ : I ↦ y) 0 x) {0, 1}

Premises used: Function.update, Insert.insert, Set.EqOn, Path.range_coe, ContinuousMap.isComplete_setOf_eqOn, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
h : Eq (α := Filter (((i : ι) → α i) × ((i : ι) → α i))) (𝓤 ((i : ι) → α i)) (𝓤 ((i : ι) → α i))
⊢ uniformSpace α = ⨅ (i : ι), UniformSpace.comap (eval (β := α) i) (U i)

Tactic:
ext : 1
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
⊢ Eq (α := Filter (((i : ι) → α i) × ((i : ι) → α i))) (𝓤 ((i : ι) → α i)) (𝓤 ((i : ι) → α i))

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
⊢ Eq (α := Filter (((i : ι) → α i) × ((i : ι) → α i))) (𝓤 ((i : ι) → α i))
    (⨅ (i : ι), Filter.comap (β := α i × α i) (fun (a : ((i : ι) → α i) × ((i : ι) → α i)) ↦ (a.1 i, a.2 i)) (𝓤 (α i)))

Tactic:
iInf_uniformity

Premises used: iInf, uniformity, setOf, iInf_uniformity, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : Countable ι
inst_2 : ∀ (i : ι), IsCountablyGenerated.{u} (α := α i × α i) (𝓤 (α i))
rw :
  IsCountablyGenerated (α := ((i : ι) → α i) × ((i : ι) → α i))
    (⨅ (i : ι), Filter.comap (β := α i × α i) (fun (a : ((i : ι) → α i) × ((i : ι) → α i)) ↦ (a.1 i, a.2 i)) (𝓤 (α i)))
⊢ IsCountablyGenerated (α := ((i : ι) → α i) × ((i : ι) → α i)) (𝓤 ((i : ι) → α i))

Tactic:
rw [Pi.uniformity]

Premises used: Pi.uniformity
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : UniformSpace β
inst_1 : Countable ι
inst_2 : ∀ (i : ι), IsCountablyGenerated.{u} (α := α i × α i) (𝓤 (α i))
⊢ IsCountablyGenerated (α := ((i : ι) → α i) × ((i : ι) → α i))
    (⨅ (i : ι), Filter.comap (β := α i × α i) (fun (a : ((i : ι) → α i) × ((i : ι) → α i)) ↦ (a.1 i, a.2 i)) (𝓤 (α i)))

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
β : Type u_4
inst : UniformSpace β
f : β → (i : ι) → α i
⊢ UniformContinuous f ↔ ∀ (i : ι), UniformContinuous.{u_4, u} (β := α i) fun (x : β) ↦ f x i

Tactic:
simp only [UniformContinuous, Pi.uniformity, tendsto_iInf, tendsto_comap_iff, Function.comp_def]

Premises used: UniformContinuous, Filter.tendsto_comap_iff, Function.comp_def, Filter.tendsto_iInf, Pi.uniformity
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
i : ι
⊢ UniformContinuous (β := α i) fun (a : (i : ι) → α i) ↦ a i

Tactic:
uniformContinuous_pi.1 uniformContinuous_id i

Premises used: uniformContinuous_id, uniformContinuous_pi, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
φ : ι' → ι
⊢ UniformContinuous (β := (j : ι') → α (φ j)) fun (f : (i : ι) → α i) (j : ι') ↦ f (φ j)

Tactic:
uniformContinuous_pi.mpr fun j ↦ uniformContinuous_proj α (φ j)

Premises used: Iff.mpr, Pi.uniformContinuous_proj, uniformContinuous_pi
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
inst : UniformSpace β
φ : ι' → ι
⊢ UniformContinuous (β := ι' → β) fun (x : ι → β) ↦ x ∘ φ

Tactic:
Pi.uniformContinuous_precomp' _ φ

Premises used: Pi.uniformContinuous_precomp'
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
β : ι → Type u_4
inst : (i : ι) → UniformSpace (β i)
g : (i : ι) → α i → β i
hg : ∀ (i : ι), UniformContinuous (g i)
⊢ UniformContinuous (β := (i : ι) → β i) fun (f : (i : ι) → α i) (i : ι) ↦ g i (f i)

Tactic:
uniformContinuous_pi.mpr fun i ↦ (hg i).comp <| uniformContinuous_proj α i

Premises used: Iff.mpr, Pi.uniformContinuous_proj, UniformContinuous.comp, uniformContinuous_pi
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
β : Type u_3
inst : UniformSpace β
α : Type u_4
inst_1 : UniformSpace α
g : α → β
hg : UniformContinuous g
⊢ UniformContinuous (β := ι → β) fun (x : ι → α) ↦ g ∘ x

Tactic:
Pi.uniformContinuous_postcomp' _ fun _ ↦ hg

Premises used: Pi.uniformContinuous_postcomp'
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
φ : ι' → ι
⊢ Eq (α := UniformSpace ((x : ι) → α x))
    (UniformSpace.comap (β := (i : ι') → α (φ i)) (fun (g : (x : ι) → α x) (i' : ι') ↦ g (φ i'))
      (uniformSpace fun (i' : ι') ↦ α (φ i')))
    (⨅ (i' : ι'), UniformSpace.comap (eval (β := α) (φ i')) (U (φ i')))

Tactic:
simp [Pi.uniformSpace_eq, UniformSpace.comap_iInf, ← UniformSpace.comap_comap, comp_def]

Premises used: Pi.uniformSpace_eq, UniformSpace.comap_comap, Function.comp_def, UniformSpace.comap_iInf
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
ι' : Type u_2
β : Type u_3
inst : UniformSpace β
φ : ι' → ι
⊢ Eq (α := UniformSpace (ι → β))
    (UniformSpace.comap (β := ι' → β) (fun (x : ι → β) ↦ x ∘ φ) (uniformSpace fun (x : ι') ↦ β))
    (⨅ (i' : ι'), UniformSpace.comap (eval (β := fun (x : ι) ↦ β) (φ i')) inst)

Tactic:
uniformSpace_comap_precomp' (fun _ ↦ β) φ

Premises used: Pi.uniformSpace_comap_precomp'
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
S : Set ι
⊢ UniformContinuous (α := (a : ι) → α a) (S.restrict (π := α))

Tactic:
Pi.uniformContinuous_precomp' _ ((↑) : S → ι)

Premises used: Pi.uniformContinuous_precomp', Set.restrict, Subtype.val
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
S : Set ι
⊢ Eq (α := UniformSpace ((a : ι) → α a))
    (UniformSpace.comap (S.restrict (π := α)) (uniformSpace fun (i : (↑S : Type u_1)) ↦ α (↑i : ι)))
    (⨅ i ∈ S, UniformSpace.comap (eval (β := α) i) (U i))

Tactic:
simp +unfoldPartialApp
    [← iInf_subtype'', ← uniformSpace_comap_precomp' _ ((↑) : S → ι), Set.restrict]

Premises used: Pi.uniformSpace_comap_precomp', iInf_subtype'', Set.restrict, Subtype.val
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : Nonempty ι
l : Filter ((i : ι) → α i)
simp_rw : Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
simp_rw₁ : (∀ (i : ι), Cauchy l) ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)

Tactic:
simp_rw +instances [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace, cauchy_comap_uniformSpace]

Premises used: Pi.uniformSpace_eq, cauchy_comap_uniformSpace, cauchy_iInf_uniformSpace
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
l : Filter ((i : ι) → α i)
inst : l.NeBot
simp_rw : Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
simp_rw₁ : (∀ (i : ι), Cauchy l) ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval (β := α) i) l)

Tactic:
simp_rw +instances [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace', cauchy_comap_uniformSpace]

Premises used: Pi.uniformSpace_eq, cauchy_iInf_uniformSpace', cauchy_comap_uniformSpace
-- Module: Mathlib.Topology.UniformSpace.Pi
Goal:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst : Nonempty ι
l : (i : ι) → Filter (α i)
hl : ∀ (i : ι), Cauchy (l i)
⊢ ∀ (i : ι), (l i).NeBot

Tactic:
have := fun i ↦ (hl i).1