awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
rw :
  Tendsto.{ua, ub} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (⨅ (i : ι), 𝓤 β) ↔
    ∀ (i : ι), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔
    ∀ (i : ι), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
have rw₁ : (∀ (i : ι), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)) ↔
  ∀ (i : ι), Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Tactic: rw [iInf_uniformity, tendsto_iInf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
s : Set α
inst : UniformSpace α
⊢ map (α := (↑s : Type ua) × (↑s : Type ua))
      (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (𝓤 (↑s : Type ua)) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
have rw : map (α := (↑s : Type ua) × (↑s : Type ua))
    (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
    (comap (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (𝓤 α)) =
  𝓤 α ⊓ 𝓟 (s ×ˢ s)
Tactic: rw [uniformity_setCoe, map_comap, range_prodMap, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
s : Set α
inst : UniformSpace α
rw :
  map (α := (↑s : Type ua) × (↑s : Type ua))
      (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
      (comap (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (𝓤 α)) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
⊢ map (α := (↑s : Type ua) × (↑s : Type ua))
      (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (𝓤 (↑s : Type ua)) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
have rw₁ : 𝓤 α ⊓
    𝓟
      (range (ι := (↑s : Type ua) × (↑s : Type ua))
        (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))) =
  𝓤 α ⊓ 𝓟 (s ×ˢ s)
Tactic: rw [uniformity_setCoe, map_comap, range_prodMap, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
s : Set α
inst : UniformSpace α
rw :
  map (α := (↑s : Type ua) × (↑s : Type ua))
      (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
      (comap (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (𝓤 α)) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
rw₁ :
  𝓤 α ⊓
      𝓟
        (range (ι := (↑s : Type ua) × (↑s : Type ua))
          (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
⊢ map (α := (↑s : Type ua) × (↑s : Type ua))
      (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (𝓤 (↑s : Type ua)) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
have rw₂ : 𝓤 α ⊓
    𝓟
      (SProd.sprod (α := Set α) (β := Set α) (range (ι := (↑s : Type ua)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
        (range (ι := (↑s : Type ua)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))) =
  𝓤 α ⊓ 𝓟 (s ×ˢ s)
Tactic: rw [uniformity_setCoe, map_comap, range_prodMap, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
s : Set α
inst : UniformSpace α
rw :
  map (α := (↑s : Type ua) × (↑s : Type ua))
      (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
      (comap (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (𝓤 α)) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
rw₁ :
  𝓤 α ⊓
      𝓟
        (range (ι := (↑s : Type ua) × (↑s : Type ua))
          (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
rw₂ :
  𝓤 α ⊓
      𝓟
        (SProd.sprod (α := Set α) (β := Set α) (range (ι := (↑s : Type ua)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
          (range (ι := (↑s : Type ua)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
⊢ map (α := (↑s : Type ua) × (↑s : Type ua))
      (Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (𝓤 (↑s : Type ua)) =
    𝓤 α ⊓ 𝓟 (s ×ˢ s)
have rw₃ : 𝓤 α ⊓ 𝓟 (s ×ˢ s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)
Tactic: rw [uniformity_setCoe, map_comap, range_prodMap, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) ↔
    Tendsto
      (fun (x : (↑s : Type ua) × (↑s : Type ua)) ↦
        (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2))
      (𝓤 (↑s : Type ua)) (𝓤 β)
have rw : Tendsto.{ua, ub} (α := (↑s : Type ua) × (↑s : Type ua))
    ((fun (x : α × α) ↦ (f x.1, f x.2)) ∘
      Prod.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
    (𝓤 (↑s : Type ua)) (𝓤 β) ↔
  Tendsto
    (fun (x : (↑s : Type ua) × (↑s : Type ua)) ↦
      (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2))
    (𝓤 (↑s : Type ua)) (𝓤 β)
Tactic: rw [← map_uniformity_set_coe, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous.{ua, ub} (β := β) fun (x : (↑s : Type ua)) ↦ f (↑x : α)
ha : s ∈ 𝓝 a
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
have rw : Tendsto f (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a sorry))) (𝓝 (f a))
Tactic: rw [(@map_nhds_subtype_coe_eq_nhds α _ (· ∈ s) a (mem_of_mem_nhds ha) ha).symm]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h : UniformContinuousOn f s
⊢ ContinuousOn f s
have h₁ : UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)
Tactic: rw [uniformContinuousOn_iff_restrict] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)
⊢ ContinuousOn f s
have rw : Continuous[instTopologicalSpaceSubtype, inst_1.toTopologicalSpace] (s.restrict (π := fun (a : α) ↦ β) f)
Tactic: rw [continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
have simp_rw : Eq (α := Filter ((α × β) × α × β))
  (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
    Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
  (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
Tactic: simp_rw [uniformity_prod, prod_eq_inf, Filter.comap_inf, Filter.comap_comap, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
simp_rw :
  Eq (α := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
⊢ Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
have simp_rw₁ : Eq (α := Filter ((α × β) × α × β))
  (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
    Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
  (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
    (Filter.comap Prod.fst (𝓤 α) ⊓ Filter.comap Prod.snd (𝓤 β)))
Tactic: simp_rw [uniformity_prod, prod_eq_inf, Filter.comap_inf, Filter.comap_comap, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
simp_rw :
  Eq (α := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
simp_rw₁ :
  Eq (α := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      (Filter.comap Prod.fst (𝓤 α) ⊓ Filter.comap Prod.snd (𝓤 β)))
⊢ Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
have simp_rw₂ : Eq (α := Filter ((α × β) × α × β))
  (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
    Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
  (Filter.comap (β := Prod.{ua, ub} (α × α) (β × β)) (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      (Filter.comap Prod.fst (𝓤 α)) ⊓
    Filter.comap (β := Prod.{ua, ub} (α × α) (β × β)) (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      (Filter.comap Prod.snd (𝓤 β)))
Tactic: simp_rw [uniformity_prod, prod_eq_inf, Filter.comap_inf, Filter.comap_comap, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
simp_rw :
  Eq (α := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
simp_rw₁ :
  Eq (α := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      (Filter.comap Prod.fst (𝓤 α) ⊓ Filter.comap Prod.snd (𝓤 β)))
simp_rw₂ :
  Eq (α := Filter ((α × β) × α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (Filter.comap (β := Prod.{ua, ub} (α × α) (β × β)) (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
        (Filter.comap Prod.fst (𝓤 α)) ⊓
      Filter.comap (β := Prod.{ua, ub} (α × α) (β × β)) (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
        (Filter.comap Prod.snd (𝓤 β)))
⊢ Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
have simp_rw₃ : Eq (α := Filter ((α × β) × α × β))
  (Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
    Filter.comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
  (Filter.comap
      (Function.comp (β := Prod.{ua, ub} (α × α) (β × β)) Prod.fst fun (p : (α × β) × α × β) ↦
        ((p.1.1, p.2.1), p.1.2, p.2.2))
      (𝓤 α) ⊓
    Filter.comap
      (Function.comp (β := Prod.{ua, ub} (α × α) (β × β)) Prod.snd fun (p : (α × β) × α × β) ↦
        ((p.1.1, p.2.1), p.1.2, p.2.2))
      (𝓤 β))
Tactic: simp_rw [uniformity_prod, prod_eq_inf, Filter.comap_inf, Filter.comap_comap, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
⊢ Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
    (map (fun (p : Prod.{ua, ub} (α × α) (β × β)) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
have rw : Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
  (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
Tactic: rw [map_swap4_eq_comap, uniformity_prod_eq_comap_prod]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
rw :
  Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
    (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
⊢ Eq (α := Filter ((α × β) × α × β)) (𝓤 (α × β))
    (map (fun (p : Prod.{ua, ub} (α × α) (β × β)) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
have rw₁ : Eq (α := Filter ((α × β) × α × β))
  (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
  (Filter.comap (fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β))
Tactic: rw [map_swap4_eq_comap, uniformity_prod_eq_comap_prod]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : SetRel β β
f : α → α → β
hf : UniformContinuous.{ua, ub} (β := β) fun (p : α × α) ↦ f p.1 p.2
hs : s ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
have hf₁ : Tendsto
  ((fun (x : (α × α) × α × α) ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun (p : (α × α) × α × α) ↦
    ((p.1.1, p.2.1), p.1.2, p.2.2))
  (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
Tactic: rw [UniformContinuous, uniformity_prod_eq_prod, tendsto_map'_iff] at hf
Cleared hypotheses: hf, hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : SetRel β β
f : α → α → β
hf :
  Tendsto
    ((fun (x : (α × α) × α × α) ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun (p : (α × α) × α × α) ↦
      ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
have rcases : ∀ (u : Set (α × α)) (hu : u ∈ 𝓤 α) (v : Set (α × α)) (hv : v ∈ 𝓤 α)
  (huvt :
    u ×ˢ v ⊆
      ((fun (x : (α × α) × α × α) ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun (p : (α × α) × α × α) ↦
          ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹'
        s),
  ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
Tactic: rcases mem_prod_iff.1 (mem_map.1 <| hf hs) with ⟨u, hu, v, hv, huvt⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
x : α × β
⊢ ball x (entourageProd u v) = ball x.1 u ×ˢ ball x.2 v
have h : ∀ (p : α × β), p ∈ ball x (entourageProd u v) ↔ p ∈ ball x.1 u ×ˢ ball x.2 v
Tactic: ext p
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
s : Set α
t : Set β
⊢ (entourageProd u v).image (s ×ˢ t) = u.image s ×ˢ v.image t
have h : ∀ (x : α × β), x ∈ (entourageProd u v).image (s ×ˢ t) ↔ x ∈ u.image s ×ˢ v.image t
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
s : Set α
t : Set β
x : α × β
⊢ x ∈ (entourageProd u v).image (s ×ˢ t) ↔ x ∈ u.image s ×ˢ v.image t
have h : (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ (a, x.1) ∈ u ∧ (b, x.2) ∈ v) ↔ (∃ a ∈ s, (a, x.1) ∈ u) ∧ ∃ a ∈ t, (a, x.2) ∈ v
Tactic: simp only [mem_entourageProd, SetRel.mem_image, Set.mem_prod, Prod.exists]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set ((α × β) × α × β)
h : Membership.mem (γ := Filter ((α × β) × α × β)) (𝓤 (α × β)) s
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s
have rcases : ∀ (w : Prod.{ua, ub} (Set (α × α)) (Set (β × β))) (hw : (w.1 ∈ 𝓤 α ∧ w.2 ∈ 𝓤 β) ∧ entourageProd (id w.1) (id w.2) ⊆ s),
  ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s
Tactic: rcases (((𝓤 α).basis_sets.uniformity_prod (𝓤 β).basis_sets).mem_iff' s).1 h with ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set ((α × β) × α × β)
h : Membership.mem (γ := Filter ((α × β) × α × β)) (𝓤 (α × β)) s
w : Prod.{ua, ub} (Set (α × α)) (Set (β × β))
hw : (w.1 ∈ 𝓤 α ∧ w.2 ∈ 𝓤 β) ∧ entourageProd (id w.1) (id w.2) ⊆ s
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s
have w₁ : Set (α × α)
Tactic: use w.1, hw.1.1, w.2, hw.1.2, hw.2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set ((α × β) × α × β)
h : Membership.mem (γ := Filter ((α × β) × α × β)) (𝓤 (α × β)) s
w : Prod.{ua, ub} (Set (α × α)) (Set (β × β))
hw : (w.1 ∈ 𝓤 α ∧ w.2 ∈ 𝓤 β) ∧ entourageProd (id w.1) (id w.2) ⊆ s
w₁ : Set (α × α)
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s
have left : w.1 ∈ 𝓤 α
Tactic: use w.1, hw.1.1, w.2, hw.1.2, hw.2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set ((α × β) × α × β)
h : Membership.mem (γ := Filter ((α × β) × α × β)) (𝓤 (α × β)) s
w : Prod.{ua, ub} (Set (α × α)) (Set (β × β))
hw : (w.1 ∈ 𝓤 α ∧ w.2 ∈ 𝓤 β) ∧ entourageProd (id w.1) (id w.2) ⊆ s
w₁ : Set (α × α)
left : w.1 ∈ 𝓤 α
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s
have w₂ : Set (β × β)
Tactic: use w.1, hw.1.1, w.2, hw.1.2, hw.2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set ((α × β) × α × β)
h : Membership.mem (γ := Filter ((α × β) × α × β)) (𝓤 (α × β)) s
w : Prod.{ua, ub} (Set (α × α)) (Set (β × β))
hw : (w.1 ∈ 𝓤 α ∧ w.2 ∈ 𝓤 β) ∧ entourageProd (id w.1) (id w.2) ⊆ s
w₁ : Set (α × α)
left : w.1 ∈ 𝓤 α
w₂ : Set (β × β)
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s
have left₁ : w.2 ∈ 𝓤 β
Tactic: use w.1, hw.1.1, w.2, hw.1.2, hw.2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set ((α × β) × α × β)
h : Membership.mem (γ := Filter ((α × β) × α × β)) (𝓤 (α × β)) s
w : Prod.{ua, ub} (Set (α × α)) (Set (β × β))
hw : (w.1 ∈ 𝓤 α ∧ w.2 ∈ 𝓤 β) ∧ entourageProd (id w.1) (id w.2) ⊆ s
w₁ : Set (α × α)
left : w.1 ∈ 𝓤 α
w₂ : Set (β × β)
left₁ : w.2 ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s
have right : entourageProd w.1 w.2 ⊆ s
Tactic: use w.1, hw.1.1, w.2, hw.1.2, hw.2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α_1 : Type ua
β_1 : Type ub
γ_1 : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α_1
inst_1 : UniformSpace β_1
inst_2 : UniformSpace γ_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
⊢ Prop
have haveI : (this : UniformSpace α) → Prop
Tactic: haveI := ua1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α_1 : Type ua
β_1 : Type ub
γ_1 : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α_1
inst_1 : UniformSpace β_1
inst_2 : UniformSpace γ_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
this : UniformSpace α
⊢ Prop
have haveI : (this : UniformSpace β) → Prop
Tactic: haveI := ub1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α_1 : Type ua
β_1 : Type ub
γ_1 : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α_1
inst_1 : UniformSpace β_1
inst_2 : UniformSpace γ_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
⊢ Prop
have haveI : (this : UniformSpace α) → Prop
Tactic: haveI := ua1 ⊓ ua2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α_1 : Type ua
β_1 : Type ub
γ_1 : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α_1
inst_1 : UniformSpace β_1
inst_2 : UniformSpace γ_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
this : UniformSpace α
⊢ Prop
have haveI : (this : UniformSpace β) → Prop
Tactic: haveI := ub1 ⊓ ub2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
⊢ UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
have ha : UniformContinuous.{u_2, u_2} (α := α) id
Tactic: have ha := @UniformContinuous.inf_dom_left _ _ id ua1 ua2 ua1 (@uniformContinuous_id _ (id _))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
ha : UniformContinuous.{u_2, u_2} (α := α) id
⊢ UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
have hb : UniformContinuous.{u_3, u_3} (α := β) id
Tactic: have hb := @UniformContinuous.inf_dom_left _ _ id ub1 ub2 ub1 (@uniformContinuous_id _ (id _))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
ha : UniformContinuous.{u_2, u_2} (α := α) id
hb : UniformContinuous.{u_3, u_3} (α := β) id
⊢ UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
have h_unif_cont_id : UniformContinuous (α := α × β) (Prod.map id id)
Tactic: have h_unif_cont_id :=
    @UniformContinuous.prodMap _ _ _ _ (ua1 ⊓ ua2) (ub1 ⊓ ub2) ua1 ub1 _ _ ha hb
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α_1 : Type ua
β_1 : Type ub
γ_1 : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α_1
inst_1 : UniformSpace β_1
inst_2 : UniformSpace γ_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
⊢ Prop
have haveI : (this : UniformSpace α) → Prop
Tactic: haveI := ua2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α_1 : Type ua
β_1 : Type ub
γ_1 : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α_1
inst_1 : UniformSpace β_1
inst_2 : UniformSpace γ_1
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
this : UniformSpace α
⊢ Prop
have haveI : (this : UniformSpace β) → Prop
Tactic: haveI := ub2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
⊢ UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
have ha : UniformContinuous.{u_2, u_2} (α := α) id
Tactic: have ha := @UniformContinuous.inf_dom_right _ _ id ua1 ua2 ua2 (@uniformContinuous_id _ (id _))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
ha : UniformContinuous.{u_2, u_2} (α := α) id
⊢ UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
have hb : UniformContinuous.{u_3, u_3} (α := β) id
Tactic: have hb := @UniformContinuous.inf_dom_right _ _ id ub1 ub2 ub2 (@uniformContinuous_id _ (id _))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
ha : UniformContinuous.{u_2, u_2} (α := α) id
hb : UniformContinuous.{u_3, u_3} (α := β) id
⊢ UniformContinuous (β := γ) fun (p : α × β) ↦ f p.1 p.2
have h_unif_cont_id : UniformContinuous (α := α × β) (Prod.map id id)
Tactic: have h_unif_cont_id :=
    @UniformContinuous.prodMap _ _ _ _ (ua1 ⊓ ua2) (ub1 ⊓ ub2) ua2 ub2 _ _ ha hb