awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p3 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
i : ι
p4 : (L i, ℓ) ∈ t
p5_1 : ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p6_1 : ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
x : α
p5 : (F i x, L i) ∈ t
p6 : (f x, F i x) ∈ t
⊢ (f x, ℓ) ∈ s

Tactic:
hts ⟨F i x, p6, L i, p5, p4⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p3 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
i : ι
p4 : (L i, ℓ) ∈ t
p5 : ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p6 : ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (F i x, L i) ∈ t) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (f x, F i x) ∈ t) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (f x, ℓ) ∈ s) x} x}
            x}
      a
h₁ h₂ : ∀ (x : α) (p5 : (F i x, L i) ∈ t) (p6 : (f x, F i x) ∈ t), (f x, ℓ) ∈ s
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
filter_upwards [p5, p6] with x p5 p6 using hts ⟨F i x, p6, L i, p5, p4⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformly F f p
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
⊢ Tendsto f p' (𝓝 ℓ)

Tactic:
(h1.tendstoUniformlyOnFilter.mono_right le_top).tendsto_of_eventually_tendsto h2 h3

Premises used: TendstoUniformlyOnFilter.mono_right, TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto, TendstoUniformly.tendstoUniformlyOnFilter, le_top
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
rw :
  (∀ (s : Set (α × α)),
      Membership.mem (γ := Filter (α × α)) (comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β)) s ↔ s ∈ 𝓤 α) ↔
    ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
⊢ IsUniformInducing f ↔ UniformSpace.comap f inst_1 = inst

Tactic:
rw [isUniformInducing_iff, UniformSpace.ext_iff, Filter.ext_iff]

Premises used: Filter.ext_iff, isUniformInducing_iff, UniformSpace.ext_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
⊢ (∀ (s : Set (α × α)),
      Membership.mem (γ := Filter (α × α)) (comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β)) s ↔ s ∈ 𝓤 α) ↔
    ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
rw :
  𝓤 α ≤ comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) ∧ comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α ↔
    𝓤 α ≤ comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
⊢ IsUniformInducing f ↔ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
rw [isUniformInducing_iff, UniformContinuous, tendsto_iff_comap, le_antisymm_iff, and_comm]

Premises used: UniformContinuous, Filter.tendsto_iff_comap, and_comm, le_antisymm_iff, isUniformInducing_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
⊢ 𝓤 α ≤ comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) ∧ comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α ↔
    𝓤 α ≤ comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
⊢ IsUniformInducing f ↔
    (∀ (i : ι'), p' i → ∃ (j : ι), p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
      ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j

Tactic:
simp [isUniformInducing_iff', h.uniformContinuous_iff h', (h'.comap _).le_basis_iff h, subset_def]

Premises used: Set.subset_def, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap, isUniformInducing_iff', Filter.HasBasis.uniformContinuous_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ ∃ t ∈ 𝓤 β, ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s
⊢ comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α

Tactic:
simp [eq_comm, Filter.ext_iff, subset_def, h]

Premises used: Set.subset_def, eq_comm, Filter.ext_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
inst : UniformSpace α
rw : comap (Prod.map _root_.id _root_.id) (𝓤 α) = 𝓤 α
rw₁ : comap _root_.id (𝓤 α) = 𝓤 α
rw₂ rw₃ : 𝓤 α = 𝓤 α
⊢ comap (fun (x : α × α) ↦ (_root_.id x.1, _root_.id x.2)) (𝓤 α) = 𝓤 α

Tactic:
rw [← Prod.map_def, Prod.map_id, comap_id]

Premises used: Filter.comap_id, Prod.map_def, Prod.map_id
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
rw :
  Eq.{u + 1} (α := Filter (α × α)) (comap (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ))
    (comap ((fun (x : β × β) ↦ (g x.1, g x.2)) ∘ fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 γ))
⊢ comap (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = 𝓤 α

Tactic:
rw [← hf.1, ← hg.1, comap_comap]

Premises used: IsUniformInducing.comap_uniformity, Filter.comap_comap
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ Eq.{u + 1} (α := Filter (α × α)) (comap (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ))
    (comap ((fun (x : β × β) ↦ (g x.1, g x.2)) ∘ fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 γ))

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
⊢ IsUniformInducing (g ∘ f) ↔ IsUniformInducing f

Tactic:
⟨fun h ↦ ?_, hg.comp⟩

Premises used: Iff.intro, IsUniformInducing.comp
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
refine : ∀ (h : IsUniformInducing (g ∘ f)), IsUniformInducing f
⊢ IsUniformInducing (g ∘ f) ↔ IsUniformInducing f

Tactic:
refine ⟨fun h ↦ ?_, hg.comp⟩
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
h : IsUniformInducing (g ∘ f)
rw : comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α
rw₁ :
  comap.{u, v} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (comap (fun (x : β × β) ↦ (g x.1, g x.2)) (𝓤 γ)) = 𝓤 α
rw₂ : comap ((fun (x : β × β) ↦ (g x.1, g x.2)) ∘ fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 γ) = 𝓤 α
rw₃ :
  Eq.{u + 1} (α := Filter (α × α)) (comap ((fun (x : β × β) ↦ (g x.1, g x.2)) ∘ fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 γ))
    (comap (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ))
rw₄ :
  Eq.{u + 1} (α := Filter (α × α)) (comap (fun (x : α × α) ↦ (g (f x.1, f x.2).1, g (f x.1, f x.2).2)) (𝓤 γ))
    (comap (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ))
rw₅ rw₆ :
  Eq.{u + 1} (α := Filter (α × α)) (comap (fun (x : α × α) ↦ (g (f x.1, f x.2).1, g (f x.1, f x.2).2)) (𝓤 γ))
    (comap (fun (x : α × α) ↦ ((fun (x : α) ↦ g (f x)) x.1, (fun (x : α) ↦ g (f x)) x.2)) (𝓤 γ))
⊢ IsUniformInducing f

Tactic:
rw [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, ← h.comap_uniformity,
    Function.comp_def, Function.comp_def]

Premises used: IsUniformInducing.comap_uniformity, Function.comp_def, Filter.comap_comap, isUniformInducing_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
ι : Sort u_1
p : ι → Prop
s : ι → Set (β × β)
H : (𝓤 β).HasBasis p s
⊢ (𝓤 α).HasBasis p fun (i : ι) ↦ Prod.map f f ⁻¹' s i

Tactic:
hf.1 ▸ H.comap _

Premises used: IsUniformInducing.comap_uniformity, Eq.rec, Filter.HasBasis.comap
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
F : Filter α
⊢ Cauchy (map f F) ↔ Cauchy F

Tactic:
simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap, ← hf.comap_uniformity]

Premises used: IsUniformInducing.comap_uniformity, Cauchy, Filter.map_le_iff_le_comap, Filter.prod_map_map_eq, Filter.map_neBot_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
⊢ IsUniformInducing f

Tactic:
⟨le_antisymm ?_ hf.le_comap⟩

Premises used: Filter.Tendsto.le_comap, le_antisymm, IsUniformInducing.mk
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
refine : comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α
⊢ IsUniformInducing f

Tactic:
refine ⟨le_antisymm ?_ hf.le_comap⟩
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
rw : comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))
⊢ comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α

Tactic:
rw [← hgf.1, ← Prod.map_def, ← Prod.map_def, ← Prod.map_comp_map f f g g, ← comap_comap]

Premises used: IsUniformInducing.comap_uniformity, Prod.map_comp_map, Filter.comap_comap, Prod.map_def
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
⊢ comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))

Tactic:
comap_mono hg.le_comap

Premises used: Filter.Tendsto.le_comap, Filter.comap_mono
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
⊢ comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))

Tactic:
exact comap_mono hg.le_comap

Premises used: Filter.Tendsto.le_comap, Filter.comap_mono
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ UniformContinuous f

Tactic:
(isUniformInducing_iff'.1 hf).1

Premises used: And.left, isUniformInducing_iff', Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
g : β → γ
hg : IsUniformInducing g
⊢ map (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) ≤ 𝓤 β ↔ map (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α) ≤ 𝓤 γ

Tactic:
simp only [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, Function.comp_def]

Premises used: IsUniformInducing.comap_uniformity, Filter.map_map, Function.comp_def, Filter.map_le_iff_le_comap
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
rw :
  LE.le.{v} (α := Filter (β × β)) (map (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)))
      (comap (fun (x : β × β) ↦ (g x.1, g x.2)) (𝓤 γ)) ↔
    map (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
rw₁ :
  map (fun (x : β × β) ↦ (g x.1, g x.2)) (map (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S))) ≤ 𝓤 γ ↔
    map (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
rw₂ :
  map ((fun (x : β × β) ↦ (g x.1, g x.2)) ∘ fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ ↔
    map (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
rw₃ :
  map (fun (x : α × α) ↦ (g (f x.1, f x.2).1, g (f x.1, f x.2).2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ ↔
    map (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
rw₄ rw₅ :
  map (fun (x : α × α) ↦ (g (f x.1, f x.2).1, g (f x.1, f x.2).2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ ↔
    map (fun (x : α × α) ↦ ((fun (x : α) ↦ g (f x)) x.1, (fun (x : α) ↦ g (f x)) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
⊢ map (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 β ↔
    map (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ

Tactic:
rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, comp_def, comp_def]

Premises used: IsUniformInducing.comap_uniformity, Filter.map_map, Function.comp_def, Filter.map_le_iff_le_comap
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
h : IsUniformInducing f
obtain : ∀ (h : IsUniformInducing f), IsInducing f
⊢ IsInducing f

Tactic:
obtain rfl := h.comap_uniformSpace

Premises used: IsUniformInducing.comap_uniformSpace, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace β
f : α → β
h : IsUniformInducing f
⊢ IsInducing f

Tactic:
.induced f

Premises used: Topology.IsInducing.induced
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace β
f : α → β
h : IsUniformInducing f
⊢ IsInducing f

Tactic:
exact .induced f
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
α' : Type u_1
β' : Type u_2
inst_2 : UniformSpace α'
inst_3 : UniformSpace β'
e₁ : α → α'
e₂ : β → β'
h₁ : IsUniformInducing e₁
h₂ : IsUniformInducing e₂
⊢ Eq (α := Filter ((α × β) × α × β))
    (comap (β := (α' × β') × α' × β') (fun (x : (α × β) × α × β) ↦ ((e₁ x.1.1, e₂ x.1.2), e₁ x.2.1, e₂ x.2.2))
      (𝓤 (α' × β')))
    (𝓤 (α × β))

Tactic:
simp [Function.comp_def, uniformity_prod, ← h₁.1, ← h₂.1, comap_inf, comap_comap]

Premises used: IsUniformInducing.comap_uniformity, Filter.comap_inf, Function.comp_def, Filter.comap_comap, uniformity_prod
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
inst : UniformSpace α
⊢ IsUniformInducing.{u, u} (α := α) (β := SeparationQuotient α) mk

Tactic:
⟨comap_mk_uniformity⟩

Premises used: IsUniformInducing.mk, SeparationQuotient.comap_mk_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space α
f : α → β
h : IsUniformInducing f
⊢ Injective f

Tactic:
h.isInducing.injective

Premises used: IsUniformInducing.isInducing, Topology.IsInducing.injective
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
rw : IsUniformInducing f ∧ Injective f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
rw₁ : Injective f ∧ IsUniformInducing f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
rw₂ rw₃ :
  Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α ↔
    Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
⊢ IsUniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff']

Premises used: isUniformEmbedding_iff, and_comm, isUniformInducing_iff'
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
rw :
  IsUniformInducing f ∧ Injective f ↔
    Injective f ∧
      (∀ (i : ι'), p' i → ∃ (j : ι), p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
rw₁ :
  Injective f ∧ IsUniformInducing f ↔
    Injective f ∧
      (∀ (i : ι'), p' i → ∃ (j : ι), p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
rw₂ rw₃ :
  (Injective f ∧
      (∀ (i : ι'), p' i → ∃ (j : ι), p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j) ↔
    Injective f ∧
      (∀ (i : ι'), p' i → ∃ (j : ι), p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
⊢ IsUniformEmbedding f ↔
    Injective f ∧
      (∀ (i : ι'), p' i → ∃ (j : ι), p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j

Tactic:
rw [isUniformEmbedding_iff, and_comm, h.isUniformInducing_iff h']

Premises used: isUniformEmbedding_iff, Filter.HasBasis.isUniformInducing_iff, and_comm
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
⊢ IsUniformEmbedding f ↔
    Injective f ∧
      UniformContinuous f ∧ ∀ (j : ι), p j → ∃ (i : ι'), p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j

Tactic:
simp only [h.isUniformEmbedding_iff' h', h.uniformContinuous_iff h']

Premises used: Filter.HasBasis.isUniformEmbedding_iff', Filter.HasBasis.uniformContinuous_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
inst : UniformSpace α
p : α → Prop
⊢ IsUniformEmbedding.{u, u} (α := Subtype p) (Subtype.val (p := p))

Tactic:
{ comap_uniformity := rfl
    injective := Subtype.val_injective }

Premises used: Subtype.val_injective, IsUniformEmbedding.mk, IsUniformInducing.mk, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
inst : UniformSpace α
s t : Set α
hst : s ⊆ t
rw :
  Eq (α := Filter ((↑s : Type u) × (↑s : Type u)))
    (comap
      ((fun (q : { x : α // x ∈ t } × { x : α // x ∈ t }) ↦ ((↑q.1 : α), (↑q.2 : α))) ∘
        fun (x : (↑s : Type u) × (↑s : Type u)) ↦
        (inclusion (s := s) (t := t) hst x.1, inclusion (s := s) (t := t) hst x.2))
      (𝓤 α))
    (comap (fun (q : { x : α // x ∈ s } × { x : α // x ∈ s }) ↦ ((↑q.1 : α), (↑q.2 : α))) (𝓤 α))
⊢ Eq.{u + 1} (α := Filter ((↑s : Type u) × (↑s : Type u)))
    (comap (β := (↑t : Type u) × (↑t : Type u))
      (fun (x : (↑s : Type u) × (↑s : Type u)) ↦
        (inclusion (s := s) (t := t) hst x.1, inclusion (s := s) (t := t) hst x.2))
      (𝓤 (↑t : Type u)))
    (𝓤 (↑s : Type u))

Tactic:
rw [uniformity_subtype, uniformity_subtype, comap_comap]

Premises used: Filter.comap_comap, uniformity_subtype
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
inst : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ Eq (α := Filter ((↑s : Type u) × (↑s : Type u)))
    (comap
      ((fun (q : { x : α // x ∈ t } × { x : α // x ∈ t }) ↦ ((↑q.1 : α), (↑q.2 : α))) ∘
        fun (x : (↑s : Type u) × (↑s : Type u)) ↦
        (inclusion (s := s) (t := t) hst x.1, inclusion (s := s) (t := t) hst x.2))
      (𝓤 α))
    (comap (fun (q : { x : α // x ∈ s } × { x : α // x ∈ s }) ↦ ((↑q.1 : α), (↑q.2 : α))) (𝓤 α))

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
g : β → γ
hg : IsUniformEmbedding g
f : α → β
simp_rw : IsUniformInducing (g ∘ f) ∧ Injective (g ∘ f) ↔ IsUniformInducing f ∧ Injective f
simp_rw₁ : IsUniformInducing f ∧ Injective (g ∘ f) ↔ IsUniformInducing f ∧ Injective f
⊢ IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f

Tactic:
simp_rw [isUniformEmbedding_iff, hg.isUniformInducing.of_comp_iff, hg.injective.of_comp_iff f]

Premises used: IsUniformEmbedding.injective, isUniformEmbedding_iff, IsUniformInducing.of_comp_iff, IsUniformEmbedding.isUniformInducing, Function.Injective.of_comp_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformEmbedding (g ∘ f)
⊢ IsUniformEmbedding f

Tactic:
⟨.of_comp hf hg hgf.isUniformInducing, .of_comp hgf.injective⟩

Premises used: IsUniformEmbedding.injective, IsUniformEmbedding.isUniformInducing, IsUniformInducing.of_comp, IsUniformEmbedding.mk, Function.Injective.of_comp
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α ≃ β
h₁ : UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
h₂ : UniformContinuous.{u_2, u_1} (α := β) (β := α) (⇑f.symm : (a : β) → α)
rwa : comap (⇑(f.prodCongr f) : (a : α × α) → β × β) (𝓤 β) ≤ 𝓤 α
rwa₁ rwa₂ rwa₃ rwa₄ : map (⇑(f.prodCongr f).symm : (a : β × β) → α × α) (𝓤 β) ≤ 𝓤 α
⊢ comap (Prod.map (⇑f : (a : α) → β) (⇑f : (a : α) → β)) (𝓤 β) ≤ 𝓤 α

Tactic:
rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]

Premises used: Equiv.prodCongr_apply, Filter.map_equiv_symm
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
hs : s ∈ 𝓤 α
x : α × α
h :
  x ∈
    preimage (β := (α ⊕ β) × (α ⊕ β)) (Prod.map Sum.inl Sum.inl)
      (Prod.map Sum.inl Sum.inl '' s ∪ range (Prod.map Sum.inr Sum.inr))
⊢ x ∈ s

Tactic:
simpa [Prod.map_apply'] using h

Premises used: Prod.map_apply'
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (β × β)
hs : s ∈ 𝓤 β
x : β × β
h :
  x ∈
    preimage (β := (α ⊕ β) × (α ⊕ β)) (Prod.map Sum.inr Sum.inr)
      (range (Prod.map Sum.inl Sum.inl) ∪ Prod.map Sum.inr Sum.inr '' s)
⊢ x ∈ s

Tactic:
simpa [Prod.map_apply'] using h

Premises used: Prod.map_apply'