awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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),
    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α₁))
⊢ edist ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y =
    ENNReal.ofReal (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
toSnowflaking₁ : 0 ≤ α
⊢ 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α₁))

Tactic:
rw [edist_toSnowflaking_toSnowflaking, dist_toSnowflaking_toSnowflaking,
          ← ENNReal.ofReal_rpow_of_nonneg, ← edist_dist]

Premises used: ENNReal.ofReal_rpow_of_nonneg, edist_dist, Metric.Snowflaking.edist_toSnowflaking_toSnowflaking, 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 x_1 : X
⊢ 0 ≤ α

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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α₁)
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
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
rw [← isBounded_preimage_toSnowflaking_iff, Metric.isBounded_iff, Metric.isBounded_iff]

Premises used: Metric.isBounded_iff, Metric.Snowflaking.isBounded_preimage_toSnowflaking_iff
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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
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
⊢ (∃ (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
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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
h : ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C ^ α
⊢ ∃ (C : ℝ), ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C

Tactic:
use C ^ α
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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
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 ^ α
h₁ : dist x y ^ α ≤ C ^ α
h₂ h₃ : C ^ α ≤ C ^ α
⊢ dist (α := Snowflaking X α hα₀ hα₁) { val := x : Snowflaking X α hα₀ hα₁ } { val := y : Snowflaking X α hα₀ hα₁ } ≤
    C ^ α

Tactic:
grw [mk_eq_toSnowflaking, dist_toSnowflaking_toSnowflaking, hC hx hy]

Premises used: Metric.Snowflaking.mk_eq_toSnowflaking, Metric.Snowflaking.dist_toSnowflaking_toSnowflaking
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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 : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
h :
  ∀ ⦃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 : 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:
use C ^ α⁻¹
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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 : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
x : X
hx : Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) x
y : X
hy : Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) y
⊢ 0 ≤ dist x y

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
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 : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
x : X
hx : Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) x
y : X
hy : Membership.mem (γ := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) y
h₂ :
  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α₁) y : Snowflaking X α hα₀ hα₁)
h₃ : 0 ≤ α⁻¹
h :
  dist x y ≤
    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α₁) ^
      α⁻¹
h₁ : dist x y ≤ (dist x y ^ α) ^ α⁻¹
h₄ h₅ : dist x y ≤ dist x y
⊢ dist x y ≤ C ^ α⁻¹

Tactic:
grw [← hC hx hy, dist_toSnowflaking_toSnowflaking, Real.rpow_rpow_inv (by positivity) hα₀.ne']

Premises used: LT.lt.ne', Real.rpow_rpow_inv, Metric.Snowflaking.dist_toSnowflaking_toSnowflaking
-- 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),
    dist (α := X)
        ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
            ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁) :
          X)
        ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) =
      dist ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y ^ α⁻¹
⊢ dist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) =
    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),
    dist (α := X)
        ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
            ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁) :
          X)
        ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
            ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x_1 : Snowflaking X α hα₀ hα₁) :
          X) =
      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α₁) ^
        α⁻¹
⊢ dist (α := X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
          ((Snowflaking.toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁) :
        X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) =
    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
⊢ dist (α := X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
          ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁) :
        X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
          ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x_1 : Snowflaking X α hα₀ hα₁) :
        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α₁) x_1 : Snowflaking X α hα₀ hα₁) ^
      α⁻¹

Tactic:
simp [Real.rpow_rpow_inv dist_nonneg hα₀.ne']

Premises used: dist_nonneg, LT.lt.ne', Real.rpow_rpow_inv
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
h :
  ∀ (y : X),
    Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
        ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' ball x r) { val := y } ↔
      Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
        (ball ((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) ⁻¹' ball x r : Set (Snowflaking X α hα₀ hα₁))
    (ball ((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 : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
y : X
⊢ Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
      ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' ball x r) { val := y } ↔
    Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
      (ball ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
      { val := y }

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

Premises used: Real.rpow_lt_rpow_iff
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
rw :
  Eq (α := Set (Snowflaking X α hα₀ hα₁))
    ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' ball x r : Set (Snowflaking X α hα₀ hα₁))
    (ball ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
rw₁ rw₂ :
  Eq (α := Set (Snowflaking X α hα₀ hα₁))
    (ball ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
    (ball ((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α₁) '' ball x r : Set (Snowflaking X α hα₀ hα₁))
    (ball ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))

Tactic:
rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_ball x hr]

Premises used: Metric.Snowflaking.image_toSnowflaking_eq_preimage, Metric.Snowflaking.preimage_ofSnowflaking_ball
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ r ^ α⁻¹

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
rw :
  ball x r =
    Set.image (α := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) : (a : X) → Snowflaking X α hα₀ hα₁)
      (ball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
rw₁ :
  ball x r =
    ball
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X))
      ((r ^ α⁻¹) ^ α)
rw₂ : ball x r = ball x ((r ^ α⁻¹) ^ α)
rw₃ rw₄ : ball x r = ball x r
⊢ Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' ball x r : Set X)
    (ball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)

Tactic:
rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_ball _ (by positivity),
    toSnowflaking_ofSnowflaking, Real.rpow_inv_rpow hr hα₀.ne']

Premises used: Metric.Snowflaking.toSnowflaking, Metric.Snowflaking.toSnowflaking_ofSnowflaking, LT.lt.ne', Equiv.preimage_eq_iff_eq_image, Metric.Snowflaking.image_toSnowflaking_ball, Real.rpow_inv_rpow
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
rw :
  Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' ball x r : Set X)
    (ball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
rw₁ rw₂ :
  Eq (α := Set X) (ball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
    (ball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
⊢ Eq (α := Set X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' ball x r : Set X)
    (ball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)

Tactic:
rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_ball _ hr]

Premises used: Metric.Snowflaking.image_ofSnowflaking_eq_preimage, Metric.Snowflaking.preimage_toSnowflaking_ball
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
h :
  ∀ (y : X),
    Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
        ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' closedBall x r) { val := y } ↔
      Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
        (closedBall ((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) ⁻¹' closedBall x r : Set (Snowflaking X α hα₀ hα₁))
    (closedBall ((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 : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
y : X
⊢ Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
      ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' closedBall x r) { val := y } ↔
    Membership.mem (γ := Set (Snowflaking X α hα₀ hα₁))
      (closedBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
      { val := y }

Tactic:
simp (disch := positivity) [Real.rpow_le_rpow_iff]

Premises used: Real.rpow_le_rpow_iff
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
rw :
  Eq (α := Set (Snowflaking X α hα₀ hα₁))
    ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' closedBall x r : Set (Snowflaking X α hα₀ hα₁))
    (closedBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
rw₁ rw₂ :
  Eq (α := Set (Snowflaking X α hα₀ hα₁))
    (closedBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))
    (closedBall ((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α₁) '' closedBall x r : Set (Snowflaking X α hα₀ hα₁))
    (closedBall ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) (r ^ α) : Set (Snowflaking X α hα₀ hα₁))

Tactic:
rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_closedBall x hr]

Premises used: Metric.Snowflaking.preimage_ofSnowflaking_closedBall, Metric.Snowflaking.image_toSnowflaking_eq_preimage
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
rw :
  closedBall x r =
    Set.image (α := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) : (a : X) → Snowflaking X α hα₀ hα₁)
      (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
rw₁ :
  closedBall x r =
    closedBall
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X))
      ((r ^ α⁻¹) ^ α)
rw₂ : closedBall x r = closedBall x ((r ^ α⁻¹) ^ α)
rw₃ rw₄ : closedBall x r = closedBall x r
⊢ Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' closedBall x r : Set X)
    (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)

Tactic:
rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedBall _ (by positivity),
    toSnowflaking_ofSnowflaking, Real.rpow_inv_rpow hr hα₀.ne']

Premises used: Metric.Snowflaking.toSnowflaking, Metric.Snowflaking.toSnowflaking_ofSnowflaking, LT.lt.ne', Equiv.preimage_eq_iff_eq_image, Metric.Snowflaking.image_toSnowflaking_closedBall, Real.rpow_inv_rpow
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
rw :
  Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' closedBall x r : Set X)
    (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
rw₁ rw₂ :
  Eq (α := Set X) (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
    (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
⊢ Eq (α := Set X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' closedBall x r : Set X)
    (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)

Tactic:
rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_closedBall _ hr]

Premises used: Metric.Snowflaking.image_ofSnowflaking_eq_preimage, Metric.Snowflaking.preimage_toSnowflaking_closedBall
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : (x : α) → ℝ≥0 × ℝ≥0∞ := fun (x : α) ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : (p : ℝ≥0 × ℝ≥0∞) → ℝ≥0∞ := fun (p : ℝ≥0 × ℝ≥0∞) ↦ (↑p.1 : ℝ≥0∞) - p.2
⊢ (fun (x : α) ↦ 1 - infEDist x E / ENNReal.ofReal δ) = sub ∘ f

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : (x : α) → ℝ≥0 × ℝ≥0∞ := fun (x : α) ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : (p : ℝ≥0 × ℝ≥0∞) → ℝ≥0∞ := fun (p : ℝ≥0 × ℝ≥0∞) ↦ (↑p.1 : ℝ≥0∞) - p.2
rw : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] (sub ∘ f)
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : α) ↦ 1 - infEDist x E / ENNReal.ofReal δ

Tactic:
rw [show (fun x : α => (1 : ℝ≥0∞) - infEDist x E / ENNReal.ofReal δ) = sub ∘ f by rfl]
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : (x : α) → ℝ≥0 × ℝ≥0∞ := fun (x : α) ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : (p : ℝ≥0 × ℝ≥0∞) → ℝ≥0∞ := fun (p : ℝ≥0 × ℝ≥0∞) ↦ (↑p.1 : ℝ≥0∞) - p.2
apply : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : α) ↦ (f x).2
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] (sub ∘ f)

Tactic:
apply (@ENNReal.continuous_nnreal_sub 1).comp

Premises used: ENNReal.continuous_nnreal_sub, Continuous.comp
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : (x : α) → ℝ≥0 × ℝ≥0∞ := fun (x : α) ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : (p : ℝ≥0 × ℝ≥0∞) → ℝ≥0∞ := fun (p : ℝ≥0 × ℝ≥0∞) ↦ (↑p.1 : ℝ≥0∞) - p.2
apply : ENNReal.ofReal δ ≠ 0
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : α) ↦ (f x).2

Tactic:
apply (ENNReal.continuous_div_const (ENNReal.ofReal δ) _).comp continuous_infEDist

Premises used: ENNReal.ofReal, Continuous.comp, Metric.continuous_infEDist, ENNReal.continuous_div_const
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : (x : α) → ℝ≥0 × ℝ≥0∞ := fun (x : α) ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : (p : ℝ≥0 × ℝ≥0∞) → ℝ≥0∞ := fun (p : ℝ≥0 × ℝ≥0∞) ↦ (↑p.1 : ℝ≥0∞) - p.2
⊢ ENNReal.ofReal δ ≠ 0

Tactic:
norm_num [δ_pos]