awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
h : TendstoUniformlyOn F f l s
u : ℕ → ι
hu : Tendsto u atTop l
⊢ TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop s
have rw : ∀ (h : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β)) (u : ℕ → ι) (hu : Tendsto u atTop l),
  Tendsto (fun (q : ℕ × α) ↦ (f q.2, F (u q.1) q.2)) (SProd.sprod (α := Filter ℕ) atTop (𝓟 s)) (𝓤 β)
Tactic: rw [tendstoUniformlyOn_iff_tendsto] at h ⊢
Cleared hypotheses: h, u, hu
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
l : Filter ι
inst_1 : l.IsCountablyGenerated
⊢ TendstoUniformly F f l ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformly (fun (n : ℕ) ↦ F (u n)) f atTop
have simp_rw : TendstoUniformlyOn F f l univ ↔
  ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop univ
Tactic: simp_rw [← tendstoUniformlyOn_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
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 (𝓝 ℓ)
⊢ Tendsto f p' (𝓝 ℓ)
have rw : Tendsto (fun (x : α) ↦ (f x, ℓ)) p' (𝓤 β)
Tactic: rw [tendsto_nhds_left]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
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 ∈ 𝓤 β
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x : α) ↦ (f x, ℓ)) p') s
have rw : ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
Tactic: rw [mem_map, Set.preimage, ← eventually_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
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 ∈ 𝓤 β
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
have obtain : ∀ (t : Set (β × β)) (ht : t ∈ 𝓤 β) (hts : SetRel.comp t (SetRel.comp t t) ⊆ s), ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
Tactic: obtain ⟨t, ht, hts⟩ := comp3_mem_uniformity hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (hypothesis)
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
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
have p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
Tactic: have p1 : ∀ᶠ i in p, (L i, ℓ) ∈ t := tendsto_nhds_left.mp h3 ht
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
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
⊢ ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x : ι |
      Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ Tendsto (F i) p' (𝓝 (L i))) x} x →
        Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ ∀ᶠ (x : α) in p', (F i x, L i) ∈ t) x} x}
    a
Tactic: filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
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
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ Tendsto (F i) p' (𝓝 (L i))) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ ∀ᶠ (x : α) in p', (F i x, L i) ∈ t) x} x}
      a
⊢ ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
have h₁ : ∀ (a : ι), Tendsto (F a) p' (𝓝 (L a)) → ∀ᶠ (x : α) in p', (F a x, L a) ∈ t
Tactic: filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (hypothesis)
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
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
have p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
Tactic: have p2 : ∀ᶠ i in p, ∀ᶠ x in p', (F i x, L i) ∈ t := by
    filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (hypothesis)
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
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
have p3 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
Tactic: have p3 : ∀ᶠ i in p, ∀ᶠ x in p', (f x, F i x) ∈ t := (h1 t ht).curry
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
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
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
have obtain : ∀ (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),
  ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
Tactic: obtain ⟨i, p4, p5, p6⟩ := (p1.and (p2.and p3)).exists
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
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
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
have 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
Tactic: filter_upwards [p5, p6] with x p5 p6 using hts ⟨F i x, p6, L i, p5, p4⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
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
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
have h₁ : ∀ (a : α), (F i a, L i) ∈ t → (f a, F i a) ∈ t → (f a, ℓ) ∈ s
Tactic: filter_upwards [p5, p6] with x p5 p6 using hts ⟨F i x, p6, L i, p5, p4⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
⊢ IsUniformInducing f ↔ UniformSpace.comap f inst_1 = inst
have rw : (∀ (s : Set (α × α)),
    Membership.mem (γ := Filter (α × α)) (comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β)) s ↔ s ∈ 𝓤 α) ↔
  ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
Tactic: rw [isUniformInducing_iff, UniformSpace.ext_iff, Filter.ext_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
⊢ IsUniformInducing f ↔ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
have 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) (𝓤 β) ≤ 𝓤 α
Tactic: rw [isUniformInducing_iff, UniformContinuous, tendsto_iff_comap, le_antisymm_iff, and_comm]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
inst : UniformSpace α
⊢ comap (fun (x : α × α) ↦ (_root_.id x.1, _root_.id x.2)) (𝓤 α) = 𝓤 α
have rw : comap (Prod.map _root_.id _root_.id) (𝓤 α) = 𝓤 α
Tactic: rw [← Prod.map_def, Prod.map_id, comap_id]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
inst : UniformSpace α
rw : comap (Prod.map _root_.id _root_.id) (𝓤 α) = 𝓤 α
⊢ comap (fun (x : α × α) ↦ (_root_.id x.1, _root_.id x.2)) (𝓤 α) = 𝓤 α
have rw₁ : comap _root_.id (𝓤 α) = 𝓤 α
Tactic: rw [← Prod.map_def, Prod.map_id, comap_id]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
inst : UniformSpace α
rw : comap (Prod.map _root_.id _root_.id) (𝓤 α) = 𝓤 α
rw₁ : comap _root_.id (𝓤 α) = 𝓤 α
⊢ comap (fun (x : α × α) ↦ (_root_.id x.1, _root_.id x.2)) (𝓤 α) = 𝓤 α
have rw₂ : 𝓤 α = 𝓤 α
Tactic: rw [← Prod.map_def, Prod.map_id, comap_id]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = 𝓤 α
have 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)) (𝓤 γ))
Tactic: rw [← hf.1, ← hg.1, comap_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
have refine : ∀ (h : IsUniformInducing (g ∘ f)), IsUniformInducing f
Tactic: refine ⟨fun h ↦ ?_, hg.comp⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
h : IsUniformInducing (g ∘ f)
⊢ IsUniformInducing f
have rw : comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α
Tactic: rw [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, ← h.comap_uniformity,
    Function.comp_def, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)) (𝓤 β) = 𝓤 α
⊢ IsUniformInducing f
have rw₁ : comap.{u, v} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (comap (fun (x : β × β) ↦ (g x.1, g x.2)) (𝓤 γ)) = 𝓤 α
Tactic: rw [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, ← h.comap_uniformity,
    Function.comp_def, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)) (𝓤 γ)) = 𝓤 α
⊢ IsUniformInducing f
have rw₂ : comap ((fun (x : β × β) ↦ (g x.1, g x.2)) ∘ fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 γ) = 𝓤 α
Tactic: rw [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, ← h.comap_uniformity,
    Function.comp_def, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)) (𝓤 γ) = 𝓤 α
⊢ IsUniformInducing f
have 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)) (𝓤 γ))
Tactic: rw [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, ← h.comap_uniformity,
    Function.comp_def, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)) (𝓤 γ))
⊢ IsUniformInducing f
have 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)) (𝓤 γ))
Tactic: rw [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, ← h.comap_uniformity,
    Function.comp_def, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)) (𝓤 γ))
⊢ IsUniformInducing f
have 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)) (𝓤 γ))
Tactic: rw [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, ← h.comap_uniformity,
    Function.comp_def, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
have refine : comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α
Tactic: refine ⟨le_antisymm ?_ hf.le_comap⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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 (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α
have rw : comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))
Tactic: rw [← hgf.1, ← Prod.map_def, ← Prod.map_def, ← Prod.map_comp_map f f g g, ← comap_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ map (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 β ↔
    map (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
have 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)) ≤ 𝓤 γ
Tactic: rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, comp_def, comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)) ≤ 𝓤 γ
⊢ map (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 β ↔
    map (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
have 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)) ≤ 𝓤 γ
Tactic: rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, comp_def, comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)) ≤ 𝓤 γ
⊢ map (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 β ↔
    map (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
have 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)) ≤ 𝓤 γ
Tactic: rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, comp_def, comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)) ≤ 𝓤 γ
⊢ map (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 β ↔
    map (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
have 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)) ≤ 𝓤 γ
Tactic: rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, comp_def, comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)) ≤ 𝓤 γ
⊢ map (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 β ↔
    map (fun (x : α × α) ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
have 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)) ≤ 𝓤 γ
Tactic: rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, comp_def, comp_def]