awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : Bornology X
s : Set X
rw : IsBounded (α := Snowflaking X α hα₀ hα₁) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' s) ↔ IsBounded s
rw₁ rw₂ : IsBounded s ↔ IsBounded s
⊢ IsBounded (α := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) ↔ IsBounded s

Tactic:
rw [← image_toSnowflaking_eq_preimage, isBounded_image_toSnowflaking_iff]

Premises used: Metric.Snowflaking.image_toSnowflaking_eq_preimage, Metric.Snowflaking.isBounded_image_toSnowflaking_iff
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : UniformSpace X
⊢ UniformContinuous.{u_1, u_1} (α := Snowflaking X α hα₀ hα₁) (β := X)
    (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)

Tactic:
uniformContinuous_comap

Premises used: uniformContinuous_comap
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : UniformSpace X
⊢ UniformContinuous.{u_1, u_1} (α := X) (β := Snowflaking X α hα₀ hα₁)
    (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁)

Tactic:
uniformContinuous_comap' uniformContinuous_id

Premises used: uniformContinuous_id, uniformContinuous_comap'
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : EDist X
x y : Snowflaking X α hα₀ hα₁
⊢ edist x y =
    edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
        ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) ^
      α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : EDist X
x y : 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α₁) y : Snowflaking X α hα₀ hα₁) =
    edist x y ^ α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : EDist X
x y : Snowflaking X α hα₀ hα₁
rw :
  edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) =
    (edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
          ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) ^
        α) ^
      α⁻¹
rw₁ rw₂ :
  edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) =
    edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X)
⊢ edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) =
    edist x y ^ α⁻¹

Tactic:
rw [edist_def, ENNReal.rpow_rpow_inv hα₀.ne']

Premises used: ENNReal.rpow_rpow_inv, LT.lt.ne', Metric.Snowflaking.edist_def
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
⊢ edist x x = 0

Tactic:
simp [edist_def, hα₀]

Premises used: Metric.Snowflaking.edist_def
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x y : Snowflaking X α hα₀ hα₁
rw :
  edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
        ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) ^
      α =
    edist y x
rw₁ :
  edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
        ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) ^
      α =
    edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X)
        ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X) ^
      α
rw₂ rw₃ :
  edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X)
        ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X) ^
      α =
    edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X)
        ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X) ^
      α
⊢ edist x y = edist y x

Tactic:
rw [edist_def, edist_def, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, Metric.Snowflaking.edist_def
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x y z : Snowflaking X α hα₀ hα₁
h₁ : 0 ≤ α
grw :
  (edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
          ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) +
        edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X)
          ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) z : X)) ^
      α ≤
    edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
          ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) ^
        α +
      edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X)
          ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) z : X) ^
        α
grw₁ grw₂ :
  edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
          ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) ^
        α +
      edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X)
          ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) z : X) ^
        α ≤
    edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
          ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) ^
        α +
      edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X)
          ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) z : X) ^
        α
⊢ edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
        ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) z : X) ^
      α ≤
    edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
          ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) ^
        α +
      edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X)
          ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) z : X) ^
        α

Tactic:
grw [edist_triangle x.ofSnowflaking y.ofSnowflaking z.ofSnowflaking,
      ENNReal.rpow_add_le_add_rpow _ _ hα₀.le hα₁]

Premises used: ENNReal.rpow_add_le_add_rpow, LT.lt.le, Metric.Snowflaking.ofSnowflaking, DFunLike.coe, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : ℝ≥0∞
h : 0 < x
⊢ 0 < x ^ α⁻¹

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
ε : ℝ≥0∞
hε : 0 < ε
⊢ 0 < ε ^ α

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
refine : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), (ε ^ α) ^ α⁻¹ ≤ ε
⊢ (𝓤 X).HasBasis (fun (x : ℝ≥0∞) ↦ 0 < x) fun (x : ℝ≥0∞) ↦ {p : X × X | edist p.1 p.2 < x ^ α⁻¹}

Tactic:
refine EMetric.mk_uniformity_basis (fun _ _ ↦ by positivity) fun ε hε ↦
        ⟨ε ^ α, by positivity, ?_⟩

Premises used: HPow.hPow, And.intro, EMetric.mk_uniformity_basis, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
ε : ℝ≥0∞
hε : 0 < ε
rw rw₁ : ε ≤ ε
⊢ (ε ^ α) ^ α⁻¹ ≤ ε

Tactic:
rw [ENNReal.rpow_rpow_inv hα₀.ne']

Premises used: ENNReal.rpow_rpow_inv, LT.lt.ne'
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
⊢ (𝓤 X).HasBasis (fun (x : ℝ≥0∞) ↦ 0 < x) fun (x : ℝ≥0∞) ↦ {p : X × X | edist p.1 p.2 < x ^ α⁻¹}

Tactic:
have H : (𝓤 X).HasBasis (0 < ·) fun x => {p | edist p.1 p.2 < x ^ (α⁻¹)} := by
      refine EMetric.mk_uniformity_basis (fun _ _ ↦ by positivity) fun ε hε ↦
        ⟨ε ^ α, by positivity, ?_⟩
      rw [ENNReal.rpow_rpow_inv hα₀.ne']
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
H : (𝓤 X).HasBasis (fun (x : ℝ≥0∞) ↦ 0 < x) fun (x : ℝ≥0∞) ↦ {p : X × X | edist p.1 p.2 < x ^ α⁻¹}
⊢ Eq.{u_1 + 1} (α := Filter (Snowflaking X α hα₀ hα₁ × Snowflaking X α hα₀ hα₁)) (𝓤 (Snowflaking X α hα₀ hα₁))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : Snowflaking X α hα₀ hα₁ × Snowflaking X α hα₀ hα₁ | edist p.1 p.2 < ε})

Tactic:
simp (disch := positivity) [uniformity_comap, H.eq_biInf, ENNReal.rpow_lt_rpow_iff]

Premises used: ENNReal.rpow_lt_rpow_iff, Filter.HasBasis.eq_biInf, uniformity_comap
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
h :
  ∀ (y : X),
    Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
        ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' eball x r) { val := y } ↔
      Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
        (eball ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
        { val := y }
⊢ Eq (α := Set (Snowflaking X α hα₀ hα₁))
    ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' eball x r : Set (Snowflaking X α hα₀ hα₁))
    (eball ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))

Tactic:
ext ⟨y⟩
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
y : X
⊢ Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
      ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' eball x r) { val := y } ↔
    Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
      (eball ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
      { val := y }

Tactic:
simp (disch := positivity) [ENNReal.rpow_lt_rpow_iff]

Premises used: ENNReal.rpow_lt_rpow_iff
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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) ⁻¹' eball x r : Set (Snowflaking X α hα₀ hα₁))
    (eball ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
rw₁ rw₂ :
  Eq (α := Set (Snowflaking X α hα₀ hα₁))
    (eball ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
    (eball ((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α₁) '' eball x r : Set (Snowflaking X α hα₀ hα₁))
    (eball ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))

Tactic:
rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_eball]

Premises used: Metric.Snowflaking.image_toSnowflaking_eq_preimage, Metric.Snowflaking.preimage_ofSnowflaking_eball
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
rw :
  eball x d =
    Set.image (α := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) : (a : X) → Snowflaking X α hα₀ hα₁)
      (eball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
rw₁ :
  eball x d =
    eball
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X))
      ((d ^ α⁻¹) ^ α)
rw₂ : eball x d = eball x ((d ^ α⁻¹) ^ α)
rw₃ rw₄ : eball x d = eball x d
⊢ 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)

Tactic:
rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_eball,
    toSnowflaking_ofSnowflaking, ENNReal.rpow_inv_rpow hα₀.ne']

Premises used: ENNReal.rpow_inv_rpow, Metric.Snowflaking.toSnowflaking, Metric.Snowflaking.image_toSnowflaking_eball, Metric.Snowflaking.toSnowflaking_ofSnowflaking, LT.lt.ne', Equiv.preimage_eq_iff_eq_image
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_eball]

Premises used: Metric.Snowflaking.image_ofSnowflaking_eq_preimage, Metric.Snowflaking.preimage_toSnowflaking_eball
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
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 }
⊢ 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:
ext ⟨y⟩
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
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:
simp (disch := positivity) [ENNReal.rpow_le_rpow_iff]

Premises used: ENNReal.rpow_le_rpow_iff
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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α₁))
rw₁ 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α₁))
⊢ 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α₁))

Tactic:
rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_closedEBall]

Premises used: Metric.Snowflaking.image_toSnowflaking_eq_preimage, Metric.Snowflaking.preimage_ofSnowflaking_closedEBall
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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 ^ α⁻¹) ^ α)
rw₃ 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)

Tactic:
rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedEBall,
    toSnowflaking_ofSnowflaking, ENNReal.rpow_inv_rpow hα₀.ne']

Premises used: ENNReal.rpow_inv_rpow, Metric.Snowflaking.toSnowflaking, Metric.Snowflaking.toSnowflaking_ofSnowflaking, LT.lt.ne', Equiv.preimage_eq_iff_eq_image, Metric.Snowflaking.image_toSnowflaking_closedEBall
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_closedEBall]

Premises used: Metric.Snowflaking.image_ofSnowflaking_eq_preimage, Metric.Snowflaking.preimage_toSnowflaking_closedEBall
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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 ^ α⁻¹

Tactic:
eq_of_forall_ge_iff fun c ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
s : Set (Snowflaking X α hα₀ hα₁)
refine :
  ∀ (c : ℝ≥0∞), ediam (X := X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) ≤ c ↔ ediam s ^ α⁻¹ ≤ c
⊢ ediam (X := X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) = ediam s ^ α⁻¹

Tactic:
refine eq_of_forall_ge_iff fun c ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
s : Set (Snowflaking X α hα₀ hα₁)
c : ℝ≥0∞
⊢ ediam (X := X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) ≤ c ↔ ediam s ^ α⁻¹ ≤ c

Tactic:
simp only [ENNReal.rpow_inv_le_iff hα₀, ediam_le_iff, Set.forall_mem_image,
    edist_ofSnowflaking_ofSnowflaking]

Premises used: ENNReal.rpow_inv_le_iff, Metric.Snowflaking.edist_ofSnowflaking_ofSnowflaking, Metric.ediam_le_iff, Set.forall_mem_image
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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 ^ α⁻¹
rw₁ rw₂ : ediam s ^ α⁻¹ = ediam s ^ α⁻¹
⊢ ediam (X := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) = ediam s ^ α⁻¹

Tactic:
rw [← image_ofSnowflaking_eq_preimage, ediam_image_ofSnowflaking]

Premises used: Metric.Snowflaking.ediam_image_ofSnowflaking, Metric.Snowflaking.image_ofSnowflaking_eq_preimage
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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 ^ α
rw₄ rw₅ : ediam s ^ α = ediam s ^ α
⊢ 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]

Premises used: ENNReal.rpow_inv_rpow, Metric.Snowflaking.ofSnowflaking_comp_toSnowflaking, Set.preimage_id, Set.preimage_comp, LT.lt.ne', Metric.ediam, Metric.Snowflaking.ediam_preimage_toSnowflaking
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
s : Set X
⊢ ediam (X := Snowflaking X α hα₀ hα₁) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' s) = ediam s ^ α

Tactic:
simp [image_toSnowflaking_eq_preimage]

Premises used: Metric.Snowflaking.image_toSnowflaking_eq_preimage
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : Dist X
x y : X
⊢ 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α₁) =
    dist x y ^ α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
toSnowflaking : ∀ (x : X), 0 ≤ dist ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y
⊢ 0 ≤ dist x y

Tactic:
cases x
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x : X
toSnowflaking :
  ∀ (x_1 : X),
    0 ≤
      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α₁)
⊢ 0 ≤ dist ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y

Tactic:
cases y
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x x_1 : X
toSnowflaking : 0 ≤ dist x x_1 ^ α
⊢ 0 ≤
    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α₁)

Tactic:
rw [dist_toSnowflaking_toSnowflaking]

Premises used: Metric.Snowflaking.dist_toSnowflaking_toSnowflaking
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x x_1 : X
⊢ 0 ≤ dist x x_1 ^ α

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
toSnowflaking :
  ∀ (x : X),
    edist ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y =
      ENNReal.ofReal (dist ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y)
⊢ edist x y = ENNReal.ofReal (dist x y)

Tactic:
cases x