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 : 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 ^ α
⊢ dist (α := Snowflaking X α hα₀ hα₁) { val := x : Snowflaking X α hα₀ hα₁ } { val := y : Snowflaking X α hα₀ hα₁ } ≤
    C ^ α
have h₁ : dist x y ^ α ≤ C ^ α
Tactic: grw [mk_eq_toSnowflaking, dist_toSnowflaking_toSnowflaking, hC hx hy]
-- 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
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 ^ α
⊢ dist (α := Snowflaking X α hα₀ hα₁) { val := x : Snowflaking X α hα₀ hα₁ } { val := y : Snowflaking X α hα₀ hα₁ } ≤
    C ^ α
have h₂ : C ^ α ≤ C ^ α
Tactic: grw [mk_eq_toSnowflaking, dist_toSnowflaking_toSnowflaking, hC hx hy]
-- 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 : 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
have 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 ^ α⁻¹
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 : 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
⊢ dist x y ≤ C ^ α⁻¹
have 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α₁)
Tactic: grw [← hC hx hy, dist_toSnowflaking_toSnowflaking, Real.rpow_rpow_inv (by positivity) hα₀.ne']
-- 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 : 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α₁)
⊢ dist x y ≤ C ^ α⁻¹
have h₃ : 0 ≤ α⁻¹
Tactic: grw [← hC hx hy, dist_toSnowflaking_toSnowflaking, Real.rpow_rpow_inv (by positivity) hα₀.ne']
-- 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 : 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 ≤ α⁻¹
⊢ dist x y ≤ C ^ α⁻¹
have 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α₁) ^
    α⁻¹
Tactic: grw [← hC hx hy, dist_toSnowflaking_toSnowflaking, Real.rpow_rpow_inv (by positivity) hα₀.ne']
-- 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 : 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α₁) ^
      α⁻¹
⊢ dist x y ≤ C ^ α⁻¹
have h₁ : dist x y ≤ (dist x y ^ α) ^ α⁻¹
Tactic: grw [← hC hx hy, dist_toSnowflaking_toSnowflaking, Real.rpow_rpow_inv (by positivity) hα₀.ne']
-- 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 : 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 ^ α) ^ α⁻¹
⊢ dist x y ≤ C ^ α⁻¹
have h₄ : dist x y ≤ dist x y
Tactic: grw [← hC hx hy, dist_toSnowflaking_toSnowflaking, Real.rpow_rpow_inv (by positivity) hα₀.ne']
-- 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α₁
⊢ dist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) =
    dist x y ^ α⁻¹
have toSnowflaking : ∀ (x : 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) y : X) =
    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
⊢ 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) y : X) =
    dist ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x) y ^ α⁻¹
have toSnowflaking : ∀ (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: 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
r : ℝ
hr : 0 ≤ r
⊢ 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α₁))
have 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 }
Tactic: ext ⟨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
r : ℝ
hr : 0 ≤ r
⊢ 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α₁))
have 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α₁))
Tactic: rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_ball x hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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α₁))
⊢ 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α₁))
have 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α₁))
Tactic: rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_ball x hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ 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)
have 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)
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_ball _ (by positivity),
    toSnowflaking_ofSnowflaking, Real.rpow_inv_rpow hr hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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)
⊢ 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)
have rw₁ : ball x r =
  ball ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X))
    ((r ^ α⁻¹) ^ α)
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_ball _ (by positivity),
    toSnowflaking_ofSnowflaking, Real.rpow_inv_rpow hr hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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 ^ α⁻¹) ^ α)
⊢ 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)
have rw₂ : ball x r = ball x ((r ^ α⁻¹) ^ α)
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_ball _ (by positivity),
    toSnowflaking_ofSnowflaking, Real.rpow_inv_rpow hr hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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 ^ α⁻¹) ^ α)
⊢ 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)
have rw₃ : ball x r = ball x r
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_ball _ (by positivity),
    toSnowflaking_ofSnowflaking, Real.rpow_inv_rpow hr hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
⊢ 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)
have 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)
Tactic: rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_ball _ hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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)
⊢ 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)
have 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)
Tactic: rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_ball _ hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
⊢ 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α₁))
have 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 }
Tactic: ext ⟨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
r : ℝ
hr : 0 ≤ r
⊢ 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α₁))
have 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α₁))
Tactic: rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_closedBall x hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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α₁))
⊢ 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α₁))
have 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α₁))
Tactic: rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_closedBall x hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ 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)
have 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)
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedBall _ (by positivity),
    toSnowflaking_ofSnowflaking, Real.rpow_inv_rpow hr hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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)
⊢ 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)
have rw₁ : closedBall x r =
  closedBall
    ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X))
    ((r ^ α⁻¹) ^ α)
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedBall _ (by positivity),
    toSnowflaking_ofSnowflaking, Real.rpow_inv_rpow hr hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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 ^ α⁻¹) ^ α)
⊢ 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)
have rw₂ : closedBall x r = closedBall x ((r ^ α⁻¹) ^ α)
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedBall _ (by positivity),
    toSnowflaking_ofSnowflaking, Real.rpow_inv_rpow hr hα₀.ne']