awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ eball x ε ∈ 𝓝 x

Tactic:
isOpen_eball.mem_nhds (mem_eball_self ε0)

Premises used: Metric.isOpen_eball, IsOpen.mem_nhds, Metric.mem_eball_self
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ closedEBall x ε ∈ 𝓝 x

Tactic:
mem_of_superset (eball_mem_nhds x ε0) eball_subset_closedEBall

Premises used: Metric.eball_subset_closedEBall, Metric.eball_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ eball x r ×ˢ eball y r ↔ z ∈ eball (x, y) r

Tactic:
simp [Prod.edist_eq]

Premises used: Prod.edist_eq
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ closedEBall x r ×ˢ closedEBall y r ↔ z ∈ closedEBall (x, y) r

Tactic:
simp [Prod.edist_eq]

Premises used: Prod.edist_eq
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ≥0∞
⊢ val (p := fun (a : α) ↦ p a) ⁻¹' eball (↑a : α) r = eball a r

Tactic:
rfl

Premises used: Set.Mem, setOf, Metric.eball, Set.preimage, rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ≥0∞
⊢ val (p := fun (a : α) ↦ p a) ⁻¹' closedEBall (↑a : α) r = closedEBall a r

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Metric.closedEBall, rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ≥0∞
rw :
  image (α := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) (val (p := fun (a : α) ↦ p a) ⁻¹' eball (↑a : α) r) =
    eball (↑a : α) r ∩ {a : α | p a}
rw₁ : eball (↑a : α) r ∩ range (ι := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) = eball (↑a : α) r ∩ {a : α | p a}
rw₂ rw₃ : eball (↑a : α) r ∩ {x : α | p x} = eball (↑a : α) r ∩ {a : α | p a}
⊢ val (p := fun (a : α) ↦ p a) '' eball a r = eball (↑a : α) r ∩ {a : α | p a}

Tactic:
rw [← preimage_eball, image_preimage_eq_inter_range, range_val_subtype]

Premises used: Set.image_preimage_eq_inter_range, Subtype.range_val_subtype, Subtype.preimage_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ≥0∞
rw :
  image (α := { a : α // p a }) (val (p := fun (a : α) ↦ p a))
      (val (p := fun (a : α) ↦ p a) ⁻¹' closedEBall (↑a : α) r) =
    closedEBall (↑a : α) r ∩ {a : α | p a}
rw₁ :
  closedEBall (↑a : α) r ∩ range (ι := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) =
    closedEBall (↑a : α) r ∩ {a : α | p a}
rw₂ rw₃ : closedEBall (↑a : α) r ∩ {x : α | p x} = closedEBall (↑a : α) r ∩ {a : α | p a}
⊢ val (p := fun (a : α) ↦ p a) '' closedEBall a r = closedEBall (↑a : α) r ∩ {a : α | p a}

Tactic:
rw [← preimage_closedEBall, image_preimage_eq_inter_range, range_val_subtype]

Premises used: Subtype.preimage_closedEBall, Set.image_preimage_eq_inter_range, Subtype.range_val_subtype
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
m m' : EMetricSpace α
h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist
mk :
  ∀ [toPseudoEMetricSpace : PseudoEMetricSpace α] (eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y)
    (h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist),
    { toPseudoEMetricSpace := toPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero : EMetricSpace α } = m'
⊢ m = m'

Tactic:
cases m
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
m' : EMetricSpace α
toPseudoEMetricSpace : PseudoEMetricSpace α
eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist
mk :
  ∀ [toPseudoEMetricSpace_1 : PseudoEMetricSpace α] (eq_of_edist_eq_zero_1 : ∀ {x y : α}, edist x y = 0 → x = y)
    (h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist),
    { toPseudoEMetricSpace := toPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero : EMetricSpace α } =
      { toPseudoEMetricSpace := toPseudoEMetricSpace_1, eq_of_edist_eq_zero := @eq_of_edist_eq_zero_1 }
⊢ { toPseudoEMetricSpace := toPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero : EMetricSpace α } = m'

Tactic:
cases m'
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
toPseudoEMetricSpace : PseudoEMetricSpace α
eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace_1 : PseudoEMetricSpace α
eq_of_edist_eq_zero_1 : ∀ {x y : α}, edist x y = 0 → x = y
h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist
mk : toPseudoEMetricSpace = toPseudoEMetricSpace_1
⊢ { toPseudoEMetricSpace := toPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero : EMetricSpace α } =
    { toPseudoEMetricSpace := toPseudoEMetricSpace_1, eq_of_edist_eq_zero := @eq_of_edist_eq_zero_1 }

Tactic:
congr
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
toPseudoEMetricSpace : PseudoEMetricSpace α
eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace_1 : PseudoEMetricSpace α
eq_of_edist_eq_zero_1 : ∀ {x y : α}, edist x y = 0 → x = y
h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist
mk : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist
⊢ toPseudoEMetricSpace = toPseudoEMetricSpace_1

Tactic:
ext1
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
toPseudoEMetricSpace : PseudoEMetricSpace α
eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace_1 : PseudoEMetricSpace α
eq_of_edist_eq_zero_1 : ∀ {x y : α}, edist x y = 0 → x = y
h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist
⊢ Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist

Tactic:
assumption
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
γ : Type w
inst : EMetricSpace γ
x y : γ
⊢ edist x y = 0 ↔ x = y

Tactic:
⟨eq_of_edist_eq_zero, fun h => h ▸ edist_self _⟩

Premises used: Eq.rec, PseudoEMetricSpace.edist_self, EMetricSpace.eq_of_edist_eq_zero, Iff.intro
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
γ : Type w
inst : EMetricSpace γ
x y : γ
⊢ 0 = edist x y ↔ x = y

Tactic:
eq_comm.trans edist_eq_zero

Premises used: eq_comm, Iff.trans, edist_eq_zero
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
γ : Type w
inst : EMetricSpace γ
x y : γ
⊢ edist x y ≤ 0 ↔ x = y

Tactic:
nonpos_iff_eq_zero.trans edist_eq_zero

Premises used: Iff.trans, edist_eq_zero, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
γ : Type w
inst : EMetricSpace γ
x y : γ
⊢ 0 < edist x y ↔ x ≠ y

Tactic:
simp [← not_le]

Premises used: not_le
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
γ : Type w
inst : EMetricSpace γ
x : γ
h : ∀ (x_1 : γ), x_1 ∈ closedEBall x 0 ↔ Membership.mem (γ := Set γ) {x} x_1
⊢ closedEBall x 0 = {x}

Tactic:
ext
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
γ : Type w
inst : EMetricSpace γ
x x_1 : γ
⊢ x_1 ∈ closedEBall x 0 ↔ Membership.mem (γ := Set γ) {x} x_1

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
γ : Type w
inst : EMetricSpace γ
x y : γ
h : ∀ ε > 0, edist x y ≤ ε
⊢ x = y

Tactic:
eq_of_edist_eq_zero (eq_of_le_of_forall_lt_imp_le_of_dense bot_le h)

Premises used: EMetricSpace.eq_of_edist_eq_zero, eq_of_le_of_forall_lt_imp_le_of_dense, bot_le
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
γ : Type w
inst : EMetricSpace γ
⊢ 𝓤 γ = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : γ × γ | edist p.1 p.2 < ε}

Tactic:
PseudoEMetricSpace.uniformity_edist

Premises used: PseudoEMetricSpace.uniformity_edist
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
X : Type u_1
inst : EDist X
a b : X
⊢ edist (α := Additive X) ((ofMul : (a : X) → Additive X) a : Additive X)
      ((ofMul : (a : X) → Additive X) b : Additive X) =
    edist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
X : Type u_1
inst : EDist X
a b : X
⊢ edist (α := Multiplicative X) ((ofAdd : (a : X) → Multiplicative X) a : Multiplicative X)
      ((ofAdd : (a : X) → Multiplicative X) b : Multiplicative X) =
    edist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
X : Type u_1
inst : EDist X
a b : Additive X
⊢ edist (α := X) ((toMul : (a : Additive X) → X) a : X) ((toMul : (a : Additive X) → X) b : X) = edist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
X : Type u_1
inst : EDist X
a b : Multiplicative X
⊢ edist (α := X) ((toAdd : (a : Multiplicative X) → X) a : X) ((toAdd : (a : Multiplicative X) → X) b : X) = edist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
X : Type u_1
inst : EDist X
a b : X
⊢ edist (α := Xᵒᵈ) ((toDual : (a : X) → Xᵒᵈ) a : Xᵒᵈ) ((toDual : (a : X) → Xᵒᵈ) b : Xᵒᵈ) = edist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
X : Type u_1
inst : EDist X
a b : Xᵒᵈ
⊢ edist (α := X) ((ofDual : (a : Xᵒᵈ) → X) a : X) ((ofDual : (a : Xᵒᵈ) → X) b : X) = edist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
inst : TopologicalSpace α
m m' : WeakPseudoEMetricSpace α
h : Eq.{u_2 + 1} (α := EDist α) (toEDist (τ := inst)) (toEDist (τ := inst))
mk :
  ∀ [toEDist : EDist α] (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x)
    (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z)
    (topology_le : UniformSpace.toTopologicalSpace ≤ inst)
    (topology_eq_on_restrict :
      ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r))
    (h :
      Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst))
        (WeakPseudoEMetricSpace.toEDist (τ := inst))),
    { toEDist := toEDist, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
        topology_le := topology_le, topology_eq_on_restrict := topology_eq_on_restrict : WeakPseudoEMetricSpace α } =
      m'
⊢ m = m'

Tactic:
cases m
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
inst : TopologicalSpace α
m' : WeakPseudoEMetricSpace α
toEDist : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le : UniformSpace.toTopologicalSpace ≤ inst
topology_eq_on_restrict :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
h :
  Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))
mk :
  ∀ [toEDist_1 : EDist α] (edist_self_1 : ∀ (x : α), edist x x = 0) (edist_comm_1 : ∀ (x y : α), edist x y = edist y x)
    (edist_triangle_1 : ∀ (x y z : α), edist x z ≤ edist x y + edist y z)
    (topology_le_1 : UniformSpace.toTopologicalSpace ≤ inst)
    (topology_eq_on_restrict_1 :
      ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r))
    (h :
      Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst))
        (WeakPseudoEMetricSpace.toEDist (τ := inst))),
    { toEDist := toEDist, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
        topology_le := topology_le, topology_eq_on_restrict := topology_eq_on_restrict : WeakPseudoEMetricSpace α } =
      { toEDist := toEDist_1, edist_self := edist_self_1, edist_comm := edist_comm_1,
        edist_triangle := edist_triangle_1, topology_le := topology_le_1,
        topology_eq_on_restrict := topology_eq_on_restrict_1 }
⊢ { toEDist := toEDist, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
      topology_le := topology_le, topology_eq_on_restrict := topology_eq_on_restrict : WeakPseudoEMetricSpace α } =
    m'

Tactic:
cases m'
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
inst : TopologicalSpace α
toEDist : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le : UniformSpace.toTopologicalSpace ≤ inst
topology_eq_on_restrict :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
toEDist_1 : EDist α
edist_self_1 : ∀ (x : α), edist x x = 0
edist_comm_1 : ∀ (x y : α), edist x y = edist y x
edist_triangle_1 : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le_1 : UniformSpace.toTopologicalSpace ≤ inst
topology_eq_on_restrict_1 :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
h :
  Eq.{u_2 + 1} (α := EDist α) (WeakPseudoEMetricSpace.toEDist (τ := inst)) (WeakPseudoEMetricSpace.toEDist (τ := inst))
⊢ { toEDist := toEDist, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
      topology_le := topology_le, topology_eq_on_restrict := topology_eq_on_restrict : WeakPseudoEMetricSpace α } =
    { toEDist := toEDist_1, edist_self := edist_self_1, edist_comm := edist_comm_1, edist_triangle := edist_triangle_1,
      topology_le := topology_le_1, topology_eq_on_restrict := topology_eq_on_restrict_1 }

Tactic:
congr
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst_1 : PseudoEMetricSpace α_1
γ : Type w
inst_2 : EMetricSpace γ
α : Type u
inst : PseudoEMetricSpace α
rw rw₁ : LE.le.{u} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace
⊢ LE.le.{u} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace

Tactic:
rw [uniformSpace_edist]

Premises used: uniformSpace_edist
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
rw : UniformSpace.toTopologicalSpace ≤ TopologicalSpace.induced f n
⊢ UniformSpace.toTopologicalSpace ≤ e

Tactic:
rw [(isInducing_iff f).mp hf]

Premises used: Iff.mp, Topology.isInducing_iff
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
⊢ UniformSpace.toTopologicalSpace ≤ TopologicalSpace.induced f n

Tactic:
(continuous_le_rng m.topology_le ?_).le_induced

Premises used: WeakPseudoEMetricSpace.topology_le, continuous_le_rng, Continuous.le_induced
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
refine :
  Continuous[(uniformSpaceOfEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯).toTopologicalSpace,
      (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace]
    f
⊢ UniformSpace.toTopologicalSpace ≤ TopologicalSpace.induced f n

Tactic:
refine (continuous_le_rng m.topology_le ?_).le_induced

Premises used: WeakPseudoEMetricSpace.topology_le, continuous_le_rng, Continuous.le_induced
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
⊢ Continuous[(uniformSpaceOfEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯).toTopologicalSpace,
      (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace]
    f

Tactic:
@Continuous.mk α β hα.toUniformSpace.toTopologicalSpace
      hβ.toUniformSpace.toTopologicalSpace f fun s hs ↦ ?_

Premises used: Continuous.mk
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
refine :
  ∀ (s : Set β) (hs : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s),
    IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (f ⁻¹' s)
⊢ Continuous[(uniformSpaceOfEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯).toTopologicalSpace,
      (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace]
    f

Tactic:
refine @Continuous.mk α β hα.toUniformSpace.toTopologicalSpace
      hβ.toUniformSpace.toTopologicalSpace f fun s hs ↦ ?_

Premises used: Continuous.mk
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
rw : ∀ (hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s), ∀ x ∈ f ⁻¹' s, ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s
⊢ IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (f ⁻¹' s)

Tactic:
rw [isOpen_iff] at hs ⊢

Premises used: EMetric.isOpen_iff
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
x : α
f₁ : ∀ (hx : f x ∈ s), ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s
⊢ x ∈ f ⁻¹' s → ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s

Tactic:
(hx : f x ∈ s)
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
x : α
hx : f x ∈ s
obtain : ∀ (ε : ℝ≥0∞) (hε : ε > 0) (hεs : Metric.eball (f x) ε ⊆ s), ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s
⊢ ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s

Tactic:
obtain ⟨ε, hε, hεs⟩ := hs (f x) hx
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
x : α
hx : f x ∈ s
ε : ℝ≥0∞
hε : ε > 0
hεs : Metric.eball (f x) ε ⊆ s
⊢ ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s

Tactic:
⟨ε, hε, fun y hy ↦ hεs hy⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun (x y : α) ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
x : α
hx : f x ∈ s
ε : ℝ≥0∞
hε : ε > 0
hεs : Metric.eball (f x) ε ⊆ s
⊢ ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s

Tactic:
exact ⟨ε, hε, fun y hy ↦ hεs hy⟩
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
obtain :
  ∀ (u : Set β) (hu : IsOpen[n] u)
    (uy :
      Eq (α := Set { x_1 : β // x_1 ∈ Metric.eball (f x) ∞ })
        (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ Metric.eball (f x) ∞) ⁻¹' u)
        (Metric.eball (f x) ∞ ↓∩ Metric.eball (f x) r)),
    IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
⊢ IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)

Tactic:
obtain ⟨u, hu, uy⟩ := m.topology_eq_on_restrict (f x) r

Premises used: WeakPseudoEMetricSpace.topology_eq_on_restrict
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
u : Set β
hu : IsOpen[n] u
uy :
  Eq (α := Set { x_1 : β // x_1 ∈ Metric.eball (f x) ∞ })
    (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ Metric.eball (f x) ∞) ⁻¹' u) (Metric.eball (f x) ∞ ↓∩ Metric.eball (f x) r)
rw : IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
⊢ IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)

Tactic:
rw [(isInducing_iff f).mp hf]

Premises used: Iff.mp, Topology.isInducing_iff
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
γ : Type w
inst_1 : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
u : Set β
hu : IsOpen[n] u
uy :
  Eq (α := Set { x_1 : β // x_1 ∈ Metric.eball (f x) ∞ })
    (Subtype.val (p := fun (x_1 : β) ↦ x_1 ∈ Metric.eball (f x) ∞) ⁻¹' u) (Metric.eball (f x) ∞ ↓∩ Metric.eball (f x) r)
⊢ Eq (α := Set { x_1 : α // x_1 ∈ Metric.eball x ∞ })
    (Subtype.val (p := fun (x_1 : α) ↦ x_1 ∈ Metric.eball x ∞) ⁻¹' f ⁻¹' u) (Metric.eball x ∞ ↓∩ Metric.eball x r)

Tactic:
aesop (add simp [Set.ext_iff])

Premises used: Set.ext_iff