awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
rw :
  Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' eball x d : Set X)
    (eball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
⊢ Eq (α := Set X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' eball x d : Set X)
    (eball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
have rw₁ : Eq (α := Set X) (eball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
  (eball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
Tactic: rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_eball]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
⊢ Eq (α := Set (Snowflaking X α hα₀ hα₁))
    ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' closedEBall x r : Set (Snowflaking X α hα₀ hα₁))
    (closedEBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
have h : ∀ (y : X),
  Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
      ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' closedEBall x r) { val := y } ↔
    Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
      (closedEBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
      { val := y }
Tactic: ext ⟨y⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
⊢ Eq (α := Set (Snowflaking X α hα₀ hα₁))
    ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' closedEBall x r : Set (Snowflaking X α hα₀ hα₁))
    (closedEBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
have rw : Eq (α := Set (Snowflaking X α hα₀ hα₁))
  ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' closedEBall x r : Set (Snowflaking X α hα₀ hα₁))
  (closedEBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
Tactic: rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_closedEBall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
rw :
  Eq (α := Set (Snowflaking X α hα₀ hα₁))
    ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' closedEBall x r : Set (Snowflaking X α hα₀ hα₁))
    (closedEBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
⊢ Eq (α := Set (Snowflaking X α hα₀ hα₁))
    ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' closedEBall x r : Set (Snowflaking X α hα₀ hα₁))
    (closedEBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
have rw₁ : Eq (α := Set (Snowflaking X α hα₀ hα₁))
  (closedEBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
  (closedEBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
Tactic: rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_closedEBall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
⊢ Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' closedEBall x d : Set X)
    (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
have rw : closedEBall x d =
  Set.image (α := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) : (a : X) → Snowflaking X α hα₀ hα₁)
    (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedEBall,
    toSnowflaking_ofSnowflaking, ENNReal.rpow_inv_rpow hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
rw :
  closedEBall x d =
    Set.image (α := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) : (a : X) → Snowflaking X α hα₀ hα₁)
      (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
⊢ Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' closedEBall x d : Set X)
    (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
have rw₁ : closedEBall x d =
  closedEBall
    ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X))
    ((d ^ α⁻¹) ^ α)
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedEBall,
    toSnowflaking_ofSnowflaking, ENNReal.rpow_inv_rpow hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
rw :
  closedEBall x d =
    Set.image (α := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) : (a : X) → Snowflaking X α hα₀ hα₁)
      (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
rw₁ :
  closedEBall x d =
    closedEBall
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X))
      ((d ^ α⁻¹) ^ α)
⊢ Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' closedEBall x d : Set X)
    (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
have rw₂ : closedEBall x d = closedEBall x ((d ^ α⁻¹) ^ α)
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedEBall,
    toSnowflaking_ofSnowflaking, ENNReal.rpow_inv_rpow hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
rw :
  closedEBall x d =
    Set.image (α := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) : (a : X) → Snowflaking X α hα₀ hα₁)
      (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
rw₁ :
  closedEBall x d =
    closedEBall
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X))
      ((d ^ α⁻¹) ^ α)
rw₂ : closedEBall x d = closedEBall x ((d ^ α⁻¹) ^ α)
⊢ Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' closedEBall x d : Set X)
    (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
have rw₃ : closedEBall x d = closedEBall x d
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedEBall,
    toSnowflaking_ofSnowflaking, ENNReal.rpow_inv_rpow hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
⊢ Eq (α := Set X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' closedEBall x d : Set X)
    (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
have rw : Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' closedEBall x d : Set X)
  (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
Tactic: rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_closedEBall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
rw :
  Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' closedEBall x d : Set X)
    (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
⊢ Eq (α := Set X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' closedEBall x d : Set X)
    (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
have rw₁ : Eq (α := Set X) (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
  (closedEBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
Tactic: rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_closedEBall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
s : Set (Snowflaking X α hα₀ hα₁)
⊢ ediam (X := X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) = ediam s ^ α⁻¹
have refine : ∀ (c : ℝ≥0∞), ediam (X := X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) ≤ c ↔ ediam s ^ α⁻¹ ≤ c
Tactic: refine eq_of_forall_ge_iff fun c ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
s : Set (Snowflaking X α hα₀ hα₁)
⊢ ediam (X := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) = ediam s ^ α⁻¹
have rw : ediam (X := X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) = ediam s ^ α⁻¹
Tactic: rw [← image_ofSnowflaking_eq_preimage, ediam_image_ofSnowflaking]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
s : Set (Snowflaking X α hα₀ hα₁)
rw : ediam (X := X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) = ediam s ^ α⁻¹
⊢ ediam (X := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) = ediam s ^ α⁻¹
have rw₁ : ediam s ^ α⁻¹ = ediam s ^ α⁻¹
Tactic: rw [← image_ofSnowflaking_eq_preimage, ediam_image_ofSnowflaking]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
s : Set X
⊢ ediam (X := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) = ediam s ^ α
have rw : (ediam (X := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) ^ α⁻¹) ^ α =
  ediam s ^ α
Tactic: rw [← ENNReal.rpow_inv_rpow hα₀.ne' (ediam _), ← ediam_preimage_toSnowflaking,
    ← Set.preimage_comp, ofSnowflaking_comp_toSnowflaking, Set.preimage_id]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
s : Set X
rw :
  (ediam (X := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) ^ α⁻¹) ^ α =
    ediam s ^ α
⊢ ediam (X := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) = ediam s ^ α
have rw₁ : ediam (X := X)
      (Set.preimage (β := Snowflaking X α hα₀ hα₁) (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁)
        ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s)) ^
    α =
  ediam s ^ α
Tactic: rw [← ENNReal.rpow_inv_rpow hα₀.ne' (ediam _), ← ediam_preimage_toSnowflaking,
    ← Set.preimage_comp, ofSnowflaking_comp_toSnowflaking, Set.preimage_id]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
s : Set X
rw :
  (ediam (X := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) ^ α⁻¹) ^ α =
    ediam s ^ α
rw₁ :
  ediam (X := X)
        (Set.preimage (β := Snowflaking X α hα₀ hα₁) (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁)
          ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s)) ^
      α =
    ediam s ^ α
⊢ ediam (X := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) = ediam s ^ α
have rw₂ : ediam (X := X)
      (comp (β := Snowflaking X α hα₀ hα₁) (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
          (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹'
        s) ^
    α =
  ediam s ^ α
Tactic: rw [← ENNReal.rpow_inv_rpow hα₀.ne' (ediam _), ← ediam_preimage_toSnowflaking,
    ← Set.preimage_comp, ofSnowflaking_comp_toSnowflaking, Set.preimage_id]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
s : Set X
rw :
  (ediam (X := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) ^ α⁻¹) ^ α =
    ediam s ^ α
rw₁ :
  ediam (X := X)
        (Set.preimage (β := Snowflaking X α hα₀ hα₁) (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁)
          ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s)) ^
      α =
    ediam s ^ α
rw₂ :
  ediam (X := X)
        (comp (β := Snowflaking X α hα₀ hα₁) (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
            (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹'
          s) ^
      α =
    ediam s ^ α
⊢ ediam (X := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) = ediam s ^ α
have rw₃ : ediam (id ⁻¹' s) ^ α = ediam s ^ α
Tactic: rw [← ENNReal.rpow_inv_rpow hα₀.ne' (ediam _), ← ediam_preimage_toSnowflaking,
    ← Set.preimage_comp, ofSnowflaking_comp_toSnowflaking, Set.preimage_id]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
s : Set X
rw :
  (ediam (X := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) ^ α⁻¹) ^ α =
    ediam s ^ α
rw₁ :
  ediam (X := X)
        (Set.preimage (β := Snowflaking X α hα₀ hα₁) (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁)
          ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s)) ^
      α =
    ediam s ^ α
rw₂ :
  ediam (X := X)
        (comp (β := Snowflaking X α hα₀ hα₁) (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
            (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹'
          s) ^
      α =
    ediam s ^ α
rw₃ : ediam (id ⁻¹' s) ^ α = ediam s ^ α
⊢ ediam (X := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) = ediam s ^ α
have rw₄ : ediam s ^ α = ediam s ^ α
Tactic: rw [← ENNReal.rpow_inv_rpow hα₀.ne' (ediam _), ← ediam_preimage_toSnowflaking,
    ← Set.preimage_comp, ofSnowflaking_comp_toSnowflaking, Set.preimage_id]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ 0 ≤ dist x y
have toSnowflaking : ∀ (x : X), 0 ≤ dist ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x : X
⊢ 0 ≤ dist ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y
have toSnowflaking : ∀ (x_1 : X),
  0 ≤
    dist (α := Snowflaking X α hα₀ hα₁)
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁)
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x_1 : Snowflaking X α hα₀ hα₁)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x x_1 : X
⊢ 0 ≤
    dist (α := Snowflaking X α hα₀ hα₁)
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁)
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x_1 : Snowflaking X α hα₀ hα₁)
have toSnowflaking : 0 ≤ dist x x_1 ^ α
Tactic: rw [dist_toSnowflaking_toSnowflaking]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ edist x y = ENNReal.ofReal (dist x y)
have toSnowflaking : ∀ (x : X),
  edist ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y =
    ENNReal.ofReal (dist ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x : X
⊢ edist ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y =
    ENNReal.ofReal (dist ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y)
have toSnowflaking : ∀ (x_1 : X),
  edist (α := Snowflaking X α hα₀ hα₁) ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁)
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x_1 : Snowflaking X α hα₀ hα₁) =
    ENNReal.ofReal
      (dist (α := Snowflaking X α hα₀ hα₁)
        ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁)
        ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x_1 : Snowflaking X α hα₀ hα₁))
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x x_1 : X
⊢ edist (α := Snowflaking X α hα₀ hα₁) ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁)
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x_1 : Snowflaking X α hα₀ hα₁) =
    ENNReal.ofReal
      (dist (α := Snowflaking X α hα₀ hα₁)
        ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁)
        ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x_1 : Snowflaking X α hα₀ hα₁))
have toSnowflaking : 0 ≤ dist x x_1
Tactic: rw [edist_toSnowflaking_toSnowflaking, dist_toSnowflaking_toSnowflaking,
          ← ENNReal.ofReal_rpow_of_nonneg, ← edist_dist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x x_1 : X
toSnowflaking : 0 ≤ dist x x_1
⊢ edist (α := Snowflaking X α hα₀ hα₁)
      ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁)
      ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x_1 : Snowflaking X α hα₀ hα₁) =
    ENNReal.ofReal
      (dist (α := Snowflaking X α hα₀ hα₁)
        ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁)
        ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x_1 : Snowflaking X α hα₀ hα₁))
have toSnowflaking₁ : 0 ≤ α
Tactic: rw [edist_toSnowflaking_toSnowflaking, dist_toSnowflaking_toSnowflaking,
          ← ENNReal.ofReal_rpow_of_nonneg, ← edist_dist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s
have rw : (∃ (C : ℝ),
    ∀ ⦃x : X⦄,
      Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) x →
        ∀ ⦃y : X⦄,
          Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) y → dist x y ≤ C) ↔
  ∃ (C : ℝ), ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
Tactic: rw [← isBounded_preimage_toSnowflaking_iff, Metric.isBounded_iff, Metric.isBounded_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
⊢ (∃ (C : ℝ),
      ∀ ⦃x : X⦄,
        Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) x →
          ∀ ⦃y : X⦄,
            Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) y → dist x y ≤ C) ↔
    ∃ (C : ℝ), ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
have mp : (∃ (C : ℝ),
    ∀ ⦃x : X⦄,
      Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) x →
        ∀ ⦃y : X⦄,
          Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) y → dist x y ≤ C) →
  ∃ (C : ℝ), ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
mp :
  (∃ (C : ℝ),
      ∀ ⦃x : X⦄,
        Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) x →
          ∀ ⦃y : X⦄,
            Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) y → dist x y ≤ C) →
    ∃ (C : ℝ), ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
⊢ (∃ (C : ℝ),
      ∀ ⦃x : X⦄,
        Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) x →
          ∀ ⦃y : X⦄,
            Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) y → dist x y ≤ C) ↔
    ∃ (C : ℝ), ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
have mpr : (∃ (C : ℝ), ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C) →
  ∃ (C : ℝ),
    ∀ ⦃x : X⦄,
      Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) x →
        ∀ ⦃y : X⦄,
          Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) y → dist x y ≤ C
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC :
  ∀ ⦃x : X⦄,
    Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) x →
      ∀ ⦃y : X⦄,
        Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) y → dist x y ≤ C
⊢ ∃ (C : ℝ), ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
have h : ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C ^ α
Tactic: use C ^ α
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC :
  ∀ ⦃x : X⦄,
    Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) x →
      ∀ ⦃y : X⦄,
        Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) y → dist x y ≤ C
x : X
hx : { val := x } ∈ s
y : X
hy : { val := y } ∈ s
⊢ dist (α := Snowflaking X α hα₀ hα₁) { val := x : Snowflaking X α hα₀ hα₁ } { val := y : Snowflaking X α hα₀ hα₁ } ≤
    C ^ α
have h : dist (α := Snowflaking X α hα₀ hα₁) ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁)
    ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) y : Snowflaking X α hα₀ hα₁) ≤
  C ^ α
Tactic: grw [mk_eq_toSnowflaking, dist_toSnowflaking_toSnowflaking, hC hx hy]