awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₃ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₄ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₅ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₆ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr₁ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₂ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₃ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₄ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₅ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₆ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₇ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₈ : x ∈ s → edist x a < δ → x ∉ s → f x ∈ t ∧ edist (f x) b < ε
mp₉ mp₁₀ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t ∧ edist (f x) b < ε
mp₁₁ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t
mp₁₂ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → edist (f x) b < ε
mpr₇ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₈ : edist x a < δ → x ∈ s → ¬edist x a < δ → edist (f x) b < ε ∧ f x ∈ t
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mpr₉ : edist x a < δ → x ∈ s → f x ∈ t → edist (f x) b < ε → edist (f x) b < ε ∧ f x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₃ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₄ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₅ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₆ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr₁ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₂ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₃ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₄ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₅ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₆ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₇ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₈ : x ∈ s → edist x a < δ → x ∉ s → f x ∈ t ∧ edist (f x) b < ε
mp₉ mp₁₀ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t ∧ edist (f x) b < ε
mp₁₁ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t
mp₁₂ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → edist (f x) b < ε
mpr₇ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₈ : edist x a < δ → x ∈ s → ¬edist x a < δ → edist (f x) b < ε ∧ f x ∈ t
mpr₉ mpr₁₀ : edist x a < δ → x ∈ s → f x ∈ t → edist (f x) b < ε → edist (f x) b < ε ∧ f x ∈ t
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mpr₁₁ : edist x a < δ → x ∈ s → f x ∈ t → edist (f x) b < ε → edist (f x) b < ε
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₃ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₄ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₅ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₆ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr₁ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₂ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₃ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₄ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₅ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₆ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₇ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₈ : x ∈ s → edist x a < δ → x ∉ s → f x ∈ t ∧ edist (f x) b < ε
mp₉ mp₁₀ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t ∧ edist (f x) b < ε
mp₁₁ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t
mp₁₂ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → edist (f x) b < ε
mpr₇ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₈ : edist x a < δ → x ∈ s → ¬edist x a < δ → edist (f x) b < ε ∧ f x ∈ t
mpr₉ mpr₁₀ : edist x a < δ → x ∈ s → f x ∈ t → edist (f x) b < ε → edist (f x) b < ε ∧ f x ∈ t
mpr₁₁ : edist x a < δ → x ∈ s → f x ∈ t → edist (f x) b < ε → edist (f x) b < ε
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
have mpr₁₂ : edist x a < δ → x ∈ s → f x ∈ t → edist (f x) b < ε → f x ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
have rw : (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → Membership.mem (γ := Set β) univ (f x) ∧ edist (f x) b < ε) ↔
  ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
Tactic: rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε
have rw : Tendsto f (𝓝 a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε
Tactic: rw [ContinuousAt, tendsto_nhds_nhds]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
a : α
rw : Tendsto f (𝓝 a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε
have rw₁ : (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε) ↔
  ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε
Tactic: rw [ContinuousAt, tendsto_nhds_nhds]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
a : α
s : Set α
⊢ ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε
have rw : Tendsto f (𝓝[s] a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε
Tactic: rw [ContinuousWithinAt, tendsto_nhdsWithin_nhds]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
a : α
s : Set α
rw : Tendsto f (𝓝[s] a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε
⊢ ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε
have rw₁ : (∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) (f a) < ε) ↔
  ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε
Tactic: rw [ContinuousWithinAt, tendsto_nhdsWithin_nhds]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε
have rw : Tendsto f (𝓝 b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε
Tactic: rw [ContinuousAt, tendsto_nhds]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
rw : Tendsto f (𝓝 b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε
have rw₁ : (∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε
Tactic: rw [ContinuousAt, tendsto_nhds]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε
have rw : Tendsto f (𝓝[s] b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε
Tactic: rw [ContinuousWithinAt, tendsto_nhds]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
s : Set β
rw : Tendsto f (𝓝[s] b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε
⊢ ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε
have rw₁ : (∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε
Tactic: rw [ContinuousWithinAt, tendsto_nhds]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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 ∩ {a : α | p a}
have 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}
Tactic: rw [← preimage_eball, image_preimage_eq_inter_range, range_val_subtype]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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}
⊢ val (p := fun (a : α) ↦ p a) '' eball a r = eball (↑a : α) r ∩ {a : α | p a}
have rw₁ : eball (↑a : α) r ∩ range (ι := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) = eball (↑a : α) r ∩ {a : α | p a}
Tactic: rw [← preimage_eball, image_preimage_eq_inter_range, range_val_subtype]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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}
⊢ val (p := fun (a : α) ↦ p a) '' eball a r = eball (↑a : α) r ∩ {a : α | p a}
have rw₂ : eball (↑a : α) r ∩ {x : α | p x} = eball (↑a : α) r ∩ {a : α | p a}
Tactic: rw [← preimage_eball, image_preimage_eq_inter_range, range_val_subtype]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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 ∩ {a : α | p a}
have 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}
Tactic: rw [← preimage_closedEBall, image_preimage_eq_inter_range, range_val_subtype]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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}
⊢ val (p := fun (a : α) ↦ p a) '' closedEBall a r = closedEBall (↑a : α) r ∩ {a : α | p a}
have rw₁ : closedEBall (↑a : α) r ∩ range (ι := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) =
  closedEBall (↑a : α) r ∩ {a : α | p a}
Tactic: rw [← preimage_closedEBall, image_preimage_eq_inter_range, range_val_subtype]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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}
⊢ val (p := fun (a : α) ↦ p a) '' closedEBall a r = closedEBall (↑a : α) r ∩ {a : α | p a}
have rw₂ : closedEBall (↑a : α) r ∩ {x : α | p x} = closedEBall (↑a : α) r ∩ {a : α | p a}
Tactic: rw [← preimage_closedEBall, image_preimage_eq_inter_range, range_val_subtype]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u_2
m m' : EMetricSpace α
h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist
⊢ m = m'
have 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'
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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
⊢ { toPseudoEMetricSpace := toPseudoEMetricSpace, eq_of_edist_eq_zero := @eq_of_edist_eq_zero : EMetricSpace α } = m'
have 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 }
Tactic: cases m'
Cleared hypotheses: m', h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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
⊢ { 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 }
have mk : toPseudoEMetricSpace = toPseudoEMetricSpace_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
γ : Type w
inst : EMetricSpace γ
x : γ
⊢ closedEBall x 0 = {x}
have h : ∀ (x_1 : γ), x_1 ∈ closedEBall x 0 ↔ Membership.mem (γ := Set γ) {x} x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
m m' : WeakPseudoEMetricSpace α
h : Eq.{u_2 + 1} (α := EDist α) (toEDist (τ := inst)) (toEDist (τ := inst))
⊢ m = m'
have 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'
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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))
⊢ { 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'
have 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 }
Tactic: cases m'
Cleared hypotheses: m', h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst_1 : PseudoEMetricSpace α_1
γ : Type w
inst_2 : EMetricSpace γ
α : Type u
inst : PseudoEMetricSpace α
⊢ LE.le.{u} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace
have rw : LE.le.{u} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace
Tactic: rw [uniformSpace_edist]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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 ≤ e
have rw : UniformSpace.toTopologicalSpace ≤ TopologicalSpace.induced f n
Tactic: rw [(isInducing_iff f).mp hf]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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
have refine : Continuous[(uniformSpaceOfEDist (fun (x y : α) ↦ edist (f x) (f y)) sorry sorry sorry).toTopologicalSpace,
    (uniformSpaceOfEDist edist sorry sorry sorry).toTopologicalSpace]
  f
Tactic: refine (continuous_le_rng m.topology_le ?_).le_induced
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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
have refine : ∀ (s : Set β) (hs : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s),
  IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (f ⁻¹' s)
Tactic: refine @Continuous.mk α β hα.toUniformSpace.toTopologicalSpace
      hβ.toUniformSpace.toTopologicalSpace f fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Defs (goal)
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
⊢ IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (f ⁻¹' s)
have rw : ∀ (hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s), ∀ x ∈ f ⁻¹' s, ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s
Tactic: rw [isOpen_iff] at hs ⊢
Cleared hypotheses: hs