awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
f : CauchyFilter α
h_ex :
  ∀ (s : Set (CauchyFilter α × CauchyFilter α)),
    Membership.mem (γ := Filter (CauchyFilter α × CauchyFilter α)) (𝓤 (CauchyFilter α)) s →
      ∃ (y : α), (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : Membership.mem (γ := Filter (CauchyFilter α × CauchyFilter α)) (𝓤 (CauchyFilter α)) s
y : α
hy : (f, pureCauchy y) ∈ s
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty
have this : Membership.mem (γ := Set (CauchyFilter α)) (range pureCauchy ∩ {y : CauchyFilter α | (f, y) ∈ s}) (pureCauchy y)
Tactic: have : pureCauchy y ∈ range pureCauchy ∩ { y : CauchyFilter α | (f, y) ∈ s } :=
      ⟨mem_range_self y, hy⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
⊢ Nonempty.{u + 1} (CauchyFilter α) ↔ Nonempty α
have mp : Nonempty.{u + 1} (CauchyFilter α) → Nonempty α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
mp : Nonempty.{u + 1} (CauchyFilter α) → Nonempty α
⊢ Nonempty.{u + 1} (CauchyFilter α) ↔ Nonempty α
have mpr : Nonempty α → Nonempty.{u + 1} (CauchyFilter α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
c : CauchyFilter α
⊢ Nonempty α
have this : Membership.mem (γ := Set (CauchyFilter α)) (closure (range pureCauchy)) c
Tactic: have := eq_univ_iff_forall.1 isDenseEmbedding_pureCauchy.isDenseInducing.closure_range c
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
c : CauchyFilter α
this : Membership.mem (γ := Set (CauchyFilter α)) (closure (range pureCauchy)) c
⊢ Nonempty α
have mp : ∀ (w : CauchyFilter α), Membership.mem (γ := Set (CauchyFilter α)) univ w → ∀ (a : α), pureCauchy a = w → Nonempty α
Tactic: obtain ⟨_, ⟨_, a, _⟩⟩ := mem_closure_iff.1 this _ isOpen_univ trivial
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ extend f (pureCauchy a) = f a
have rw : IsDenseInducing.extend (β := CauchyFilter α) sorry f (pureCauchy a) = f a
Tactic: rw [extend, if_pos hf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
f : α → β
⊢ UniformContinuous (α := CauchyFilter α) (extend f)
have pos : ∀ (hf : UniformContinuous f), UniformContinuous (α := CauchyFilter α) (extend f)
Tactic: by_cases hf : UniformContinuous f
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
f : α → β
pos : ∀ (hf : UniformContinuous f), UniformContinuous (α := CauchyFilter α) (extend f)
⊢ UniformContinuous (α := CauchyFilter α) (extend f)
have neg : ∀ (hf : ¬UniformContinuous f), UniformContinuous (α := CauchyFilter α) (extend f)
Tactic: by_cases hf : UniformContinuous f
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (α := CauchyFilter α) (extend f)
have pos : UniformContinuous (α := CauchyFilter α) (IsDenseInducing.extend sorry f)
Tactic: rw [extend, if_pos hf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
β : Type v
inst_1 : UniformSpace β
inst_2 : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (α := CauchyFilter α) (extend f)
have neg : UniformContinuous.{u, v} (β := β) fun (x : CauchyFilter α) ↦ f sorry.some
Tactic: rw [extend, if_neg hf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
f g : CauchyFilter α
a b : α
ha : (↑f : Filter α) ≤ 𝓝 a
hb : (↑g : Filter α) ≤ 𝓝 b
⊢ Inseparable a b ↔ Inseparable f g
have ha₁ : Tendsto id (↑f : Filter α) (𝓝 a)
Tactic: rw [← tendsto_id'] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
f g : CauchyFilter α
a b : α
ha : (↑f : Filter α) ≤ 𝓝 a
hb : (↑g : Filter α) ≤ 𝓝 b
ha₁ : Tendsto id (↑f : Filter α) (𝓝 a)
⊢ Inseparable a b ↔ Inseparable f g
have hb₁ : Tendsto id (↑g : Filter α) (𝓝 b)
Tactic: rw [← tendsto_id'] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f : Filter α) (𝓝 a)
hb : Tendsto id (↑g : Filter α) (𝓝 b)
⊢ Inseparable a b ↔ Inseparable f g
have rw : Tendsto (fun (x : α × α) ↦ ((id ∘ Prod.fst) x, (id ∘ Prod.snd) x)) ((↑f : Filter α) ×ˢ (↑g : Filter α)) (𝓤 α) ↔
  (↑f : Filter α) ×ˢ (↑g : Filter α) ≤ 𝓤 α
Tactic: rw [inseparable_iff, (ha.comp tendsto_fst).inseparable_iff_uniformity (hb.comp tendsto_snd)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : CompleteSpace α
inst_2 : T0Space α
f g : CauchyFilter α
⊢ (↑f : Filter α).lim = (↑g : Filter α).lim ↔ Inseparable f g
have rw : Inseparable (↑f : Filter α).lim (↑g : Filter α).lim ↔ Inseparable f g
Tactic: rw [← inseparable_iff_eq, inseparable_lim_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : CompleteSpace α
inst_2 : T0Space α
f g : CauchyFilter α
rw : Inseparable (↑f : Filter α).lim (↑g : Filter α).lim ↔ Inseparable f g
⊢ (↑f : Filter α).lim = (↑g : Filter α).lim ↔ Inseparable f g
have rw₁ : Inseparable f g ↔ Inseparable f g
Tactic: rw [← inseparable_iff_eq, inseparable_lim_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
⊢ Completion (SeparationQuotient α) ≃ Completion α
have refine_1 : ∀ (a : Completion (SeparationQuotient α)),
  Completion.map SeparationQuotient.mk (Completion.extension (lift' coe') a) = a
Tactic: refine ⟨Completion.extension (lift' ((↑) : α → Completion α)),
    Completion.map SeparationQuotient.mk, fun a ↦ ?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
refine_1 :
  ∀ (a : Completion (SeparationQuotient α)),
    Completion.map SeparationQuotient.mk (Completion.extension (lift' coe') a) = a
⊢ Completion (SeparationQuotient α) ≃ Completion α
have refine_2 : ∀ (a : Completion α),
  Completion.extension (α := SeparationQuotient α) (lift' coe') (Completion.map SeparationQuotient.mk a) = a
Tactic: refine ⟨Completion.extension (lift' ((↑) : α → Completion α)),
    Completion.map SeparationQuotient.mk, fun a ↦ ?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a : Completion (SeparationQuotient α)
⊢ Completion.map SeparationQuotient.mk (Completion.extension (lift' coe') a) = a
have refine_1 : ∀ (a : SeparationQuotient α),
  Eq (α := Completion (SeparationQuotient α))
    (Completion.map SeparationQuotient.mk (Completion.extension (lift' coe') (↑a : Completion (SeparationQuotient α))))
    (↑a : Completion (SeparationQuotient α))
Tactic: refine induction_on a (isClosed_eq (continuous_map.comp continuous_extension) continuous_id) ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a : Completion (SeparationQuotient α)
⊢ ∀ (a : SeparationQuotient α),
    Eq (α := Completion (SeparationQuotient α))
      (Completion.map SeparationQuotient.mk
        (Completion.extension (lift' coe') (↑a : Completion (SeparationQuotient α))))
      (↑a : Completion (SeparationQuotient α))
have refine_1 : ∀ (a : α),
  Eq (α := Completion (SeparationQuotient α))
    (Completion.map SeparationQuotient.mk
      (Completion.extension (α := SeparationQuotient α) (lift' coe')
        (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))))
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
Tactic: refine SeparationQuotient.surjective_mk.forall.2 fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a_1 : Completion (SeparationQuotient α)
a : α
⊢ Eq (α := Completion (SeparationQuotient α))
    (Completion.map SeparationQuotient.mk
      (Completion.extension (α := SeparationQuotient α) (lift' coe')
        (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))))
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
have refine_1 : Eq (α := Completion (SeparationQuotient α))
  (Completion.map SeparationQuotient.mk (lift' coe' (SeparationQuotient.mk a)))
  (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
Tactic: rw [extension_coe (uniformContinuous_lift' _), lift'_mk (uniformContinuous_coe α),
      map_coe uniformContinuous_mk]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a_1 : Completion (SeparationQuotient α)
a : α
refine_1 :
  Eq (α := Completion (SeparationQuotient α))
    (Completion.map SeparationQuotient.mk (lift' coe' (SeparationQuotient.mk a)))
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
⊢ Eq (α := Completion (SeparationQuotient α))
    (Completion.map SeparationQuotient.mk
      (Completion.extension (α := SeparationQuotient α) (lift' coe')
        (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))))
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
have refine_1₁ : Eq (α := Completion (SeparationQuotient α)) (Completion.map SeparationQuotient.mk (↑a : Completion α))
  (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
Tactic: rw [extension_coe (uniformContinuous_lift' _), lift'_mk (uniformContinuous_coe α),
      map_coe uniformContinuous_mk]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a_1 : Completion (SeparationQuotient α)
a : α
refine_1 :
  Eq (α := Completion (SeparationQuotient α))
    (Completion.map SeparationQuotient.mk (lift' coe' (SeparationQuotient.mk a)))
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
refine_1₁ :
  Eq (α := Completion (SeparationQuotient α)) (Completion.map SeparationQuotient.mk (↑a : Completion α))
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
⊢ Eq (α := Completion (SeparationQuotient α))
    (Completion.map SeparationQuotient.mk
      (Completion.extension (α := SeparationQuotient α) (lift' coe')
        (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))))
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
have refine_1₂ : Eq (α := Completion (SeparationQuotient α)) (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
  (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α))
Tactic: rw [extension_coe (uniformContinuous_lift' _), lift'_mk (uniformContinuous_coe α),
      map_coe uniformContinuous_mk]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a : Completion α
⊢ Completion.extension (α := SeparationQuotient α) (lift' coe') (Completion.map SeparationQuotient.mk a) = a
have refine_2 : ∀ (a : α),
  Eq (α := Completion α)
    (Completion.extension (α := SeparationQuotient α) (lift' coe')
      (Completion.map SeparationQuotient.mk (↑a : Completion α)))
    (↑a : Completion α)
Tactic: refine induction_on a
      (isClosed_eq (continuous_extension.comp continuous_map) continuous_id) fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a_1 : Completion α
a : α
⊢ Eq (α := Completion α)
    (Completion.extension (α := SeparationQuotient α) (lift' coe')
      (Completion.map SeparationQuotient.mk (↑a : Completion α)))
    (↑a : Completion α)
have refine_2 : Eq (α := Completion α)
  (Completion.extension (α := SeparationQuotient α) (lift' coe')
    (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α)))
  (↑a : Completion α)
Tactic: rw [map_coe uniformContinuous_mk, extension_coe (uniformContinuous_lift' _),
      lift'_mk (uniformContinuous_coe _)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a_1 : Completion α
a : α
refine_2 :
  Eq (α := Completion α)
    (Completion.extension (α := SeparationQuotient α) (lift' coe')
      (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α)))
    (↑a : Completion α)
⊢ Eq (α := Completion α)
    (Completion.extension (α := SeparationQuotient α) (lift' coe')
      (Completion.map SeparationQuotient.mk (↑a : Completion α)))
    (↑a : Completion α)
have refine_2₁ : Eq (α := Completion α) (lift' coe' (SeparationQuotient.mk a)) (↑a : Completion α)
Tactic: rw [map_coe uniformContinuous_mk, extension_coe (uniformContinuous_lift' _),
      lift'_mk (uniformContinuous_coe _)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α_1 : Type u_1
inst : UniformSpace α_1
β : Type u_2
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
α : Type u
inst_3 : UniformSpace α
a_1 : Completion α
a : α
refine_2 :
  Eq (α := Completion α)
    (Completion.extension (α := SeparationQuotient α) (lift' coe')
      (↑(SeparationQuotient.mk a) : Completion (SeparationQuotient α)))
    (↑a : Completion α)
refine_2₁ : Eq (α := Completion α) (lift' coe' (SeparationQuotient.mk a)) (↑a : Completion α)
⊢ Eq (α := Completion α)
    (Completion.extension (α := SeparationQuotient α) (lift' coe')
      (Completion.map SeparationQuotient.mk (↑a : Completion α)))
    (↑a : Completion α)
have refine_2₂ : Eq (α := Completion α) (↑a : Completion α) (↑a : Completion α)
Tactic: rw [map_coe uniformContinuous_mk, extension_coe (uniformContinuous_lift' _),
      lift'_mk (uniformContinuous_coe _)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
R : SetRel α α
f g : Filter α
inst : R.IsSymm
⊢ R ∈ f ×ˢ g ↔ R ∈ g ×ˢ f
have rw : R.inv ∈ f ×ˢ g ↔ R.inv ∈ g ×ˢ f
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← mem_map, ← prod_comm, ← SetRel.inv, R.inv_eq_self]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
R : SetRel α α
f g : Filter α
inst : R.IsSymm
rw : R.inv ∈ f ×ˢ g ↔ R.inv ∈ g ×ˢ f
⊢ R ∈ f ×ˢ g ↔ R ∈ g ×ˢ f
have rw₁ : Prod.swap ⁻¹' R ∈ f ×ˢ g ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← mem_map, ← prod_comm, ← SetRel.inv, R.inv_eq_self]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
R : SetRel α α
f g : Filter α
inst : R.IsSymm
rw : R.inv ∈ f ×ˢ g ↔ R.inv ∈ g ×ˢ f
rw₁ : Prod.swap ⁻¹' R ∈ f ×ˢ g ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
⊢ R ∈ f ×ˢ g ↔ R ∈ g ×ˢ f
have rw₂ : R ∈ map Prod.swap (f ×ˢ g) ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← mem_map, ← prod_comm, ← SetRel.inv, R.inv_eq_self]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
R : SetRel α α
f g : Filter α
inst : R.IsSymm
rw : R.inv ∈ f ×ˢ g ↔ R.inv ∈ g ×ˢ f
rw₁ : Prod.swap ⁻¹' R ∈ f ×ˢ g ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
rw₂ : R ∈ map Prod.swap (f ×ˢ g) ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
⊢ R ∈ f ×ˢ g ↔ R ∈ g ×ˢ f
have rw₃ : R ∈ g ×ˢ f ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← mem_map, ← prod_comm, ← SetRel.inv, R.inv_eq_self]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
R : SetRel α α
f g : Filter α
inst : R.IsSymm
rw : R.inv ∈ f ×ˢ g ↔ R.inv ∈ g ×ˢ f
rw₁ : Prod.swap ⁻¹' R ∈ f ×ˢ g ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
rw₂ : R ∈ map Prod.swap (f ×ˢ g) ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
rw₃ : R ∈ g ×ˢ f ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
⊢ R ∈ f ×ˢ g ↔ R ∈ g ×ˢ f
have rw₄ : R ∈ g ×ˢ f ↔ R.inv ∈ g ×ˢ f
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← mem_map, ← prod_comm, ← SetRel.inv, R.inv_eq_self]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
R : SetRel α α
f g : Filter α
inst : R.IsSymm
rw : R.inv ∈ f ×ˢ g ↔ R.inv ∈ g ×ˢ f
rw₁ : Prod.swap ⁻¹' R ∈ f ×ˢ g ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
rw₂ : R ∈ map Prod.swap (f ×ˢ g) ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
rw₃ : R ∈ g ×ˢ f ↔ Prod.swap ⁻¹' R ∈ g ×ˢ f
rw₄ : R ∈ g ×ˢ f ↔ R.inv ∈ g ×ˢ f
⊢ R ∈ f ×ˢ g ↔ R ∈ g ×ˢ f
have rw₅ : R ∈ g ×ˢ f ↔ R ∈ g ×ˢ f
Tactic: rw [← R.inv_eq_self, SetRel.inv, ← mem_map, ← prod_comm, ← SetRel.inv, R.inv_eq_self]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type u
u : Core α
x : α
⊢ 𝓝 x = comap (Prod.mk x) u.uniformity
have hpure : ∀ (a : α), ∀ i ∈ u.uniformity, a ∈ Prod.mk a ⁻¹' id i
Tactic: apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun _ ↦ (basis_sets _).comap _)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type u
u : Core α
x : α
hpure : ∀ (a : α), ∀ i ∈ u.uniformity, a ∈ Prod.mk a ⁻¹' id i
⊢ 𝓝 x = comap (Prod.mk x) u.uniformity
have hopen : ∀ (a : α),
  ∀ i ∈ u.uniformity, ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id i ∈ comap (Prod.mk x) u.uniformity
Tactic: apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun _ ↦ (basis_sets _).comap _)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
⊢ ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity
have hopen : ∀ (V : Set (α × α)) (hV : V ∈ u.uniformity) (hVU : V ○ V ⊆ U),
  ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity
Tactic: rcases u.comp_mem_uniformity_sets hU with ⟨V, hV, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
⊢ ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity
have h : ∀ (b : α) (hb : b ∈ Prod.mk a ⁻¹' V), Prod.mk a ⁻¹' id U ∈ comap (Prod.mk b) u.uniformity
Tactic: filter_upwards [preimage_mem_comap hV] with b hb
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
V : Set (α × α)
hV : V ∈ u.uniformity
hVU : V ○ V ⊆ U
b : α
hb : b ∈ Prod.mk a ⁻¹' V
⊢ Prod.mk a ⁻¹' id U ∈ comap (Prod.mk b) u.uniformity
have h : ∀ (c : α) (hc : c ∈ Prod.mk b ⁻¹' V), c ∈ Prod.mk a ⁻¹' id U
Tactic: filter_upwards [preimage_mem_comap hV] with c hc
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α_1 : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
u : Core α
t : TopologicalSpace α
h : t = u.toTopologicalSpace
x : α
⊢ 𝓝 x = comap (Prod.mk x) u.uniformity
have rw : 𝓝 x = comap (Prod.mk x) u.uniformity
Tactic: rw [h, u.nhds_toTopologicalSpace]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α_1 : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
u : Core α
t : TopologicalSpace α
h : t = u.toTopologicalSpace
x : α
rw : 𝓝 x = comap (Prod.mk x) u.uniformity
⊢ 𝓝 x = comap (Prod.mk x) u.uniformity
have rw₁ : comap (Prod.mk x) u.uniformity = comap (Prod.mk x) u.uniformity
Tactic: rw [h, u.nhds_toTopologicalSpace]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : Membership.mem (γ := Filter (α × α)) UniformSpace.uniformity U
x : α
⊢ Prod.mk x ⁻¹' U ∈ 𝓝 x
have rw : Prod.mk x ⁻¹' U ∈ comap (Prod.mk x) UniformSpace.uniformity
Tactic: rw [UniformSpace.nhds_eq_comap_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (hypothesis)
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : Membership.mem (γ := Filter (α × α)) UniformSpace.uniformity U
x : α
⊢ (x, x) ∈ U
have this : Prod.mk x ⁻¹' U ∈ 𝓝 x
Tactic: have : Prod.mk x ⁻¹' U ∈ 𝓝 x := by
      rw [UniformSpace.nhds_eq_comap_uniformity]
      exact preimage_mem_comap hU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
u : UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a
have rw : 𝓝 a = comap (Prod.mk a) UniformSpace.uniformity
Tactic: rw [u.nhds_eq_comap_uniformity, u.toCore.nhds_toTopologicalSpace]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
u : UniformSpace α
a : α
rw : 𝓝 a = comap (Prod.mk a) UniformSpace.uniformity
⊢ 𝓝 a = 𝓝 a
have rw₁ : comap (Prod.mk a) u.toCore.uniformity = comap (Prod.mk a) UniformSpace.uniformity
Tactic: rw [u.nhds_eq_comap_uniformity, u.toCore.nhds_toTopologicalSpace]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ 𝓝 x = 𝓝 x
have rw : comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.uniformity
Tactic: rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (hypothesis)
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
⊢ u₁ = u₂
have this : Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace toTopologicalSpace
Tactic: have : u₁.toTopologicalSpace = u₂.toTopologicalSpace := TopologicalSpace.ext_nhds fun x ↦ by
    rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]
    exact congr_arg (comap _) h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
this : Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace toTopologicalSpace
⊢ u₁ = u₂
have mk : ∀ [toTopologicalSpace : TopologicalSpace α] (uniformity : Filter (α × α))
  (symm : Tendsto Prod.swap uniformity uniformity)
  (comp : (uniformity.lift' fun (s : Set (α × α)) ↦ s ○ s) ≤ uniformity)
  (nhds_eq_comap_uniformity : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity) (h : 𝓤 α = 𝓤 α)
  (this : Eq.{ua + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace),
  { toTopologicalSpace := toTopologicalSpace, uniformity := uniformity, symm := symm, comp := comp,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity : UniformSpace α } =
    u₂
Tactic: cases u₁
Cleared hypotheses: u₁, h, this