awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ))) =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
have h : dist b a = r * dist b' a'
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ))) =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
have h : dist b c = r * dist b' c'
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ))) =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
have h : dist c a = r * dist c' a'
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ))) =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
have h : dist c b = r * dist c' b'
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : Bornology X
s : Set (Snowflaking X α hα₀ hα₁)
⊢ IsBounded (α := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) ↔ IsBounded s
have rw : IsBounded (α := X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) ↔ IsBounded s
Tactic: rw [← image_ofSnowflaking_eq_preimage, isBounded_image_ofSnowflaking_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : Bornology X
s : Set (Snowflaking X α hα₀ hα₁)
rw : IsBounded (α := X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) ↔ IsBounded s
⊢ IsBounded (α := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) ↔ IsBounded s
have rw₁ : IsBounded s ↔ IsBounded s
Tactic: rw [← image_ofSnowflaking_eq_preimage, isBounded_image_ofSnowflaking_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : Bornology X
s : Set X
⊢ IsBounded (α := Snowflaking X α hα₀ hα₁) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' s) ↔ IsBounded s
have rw : IsBounded (α := X)
    (Set.image (α := Snowflaking X α hα₀ hα₁) (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
      ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' s)) ↔
  IsBounded s
Tactic: rw [← isBounded_image_ofSnowflaking_iff, image_ofSnowflaking_image_toSnowflaking]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : Bornology X
s : Set X
rw :
  IsBounded (α := X)
      (Set.image (α := Snowflaking X α hα₀ hα₁) (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
        ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' s)) ↔
    IsBounded s
⊢ IsBounded (α := Snowflaking X α hα₀ hα₁) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' s) ↔ IsBounded s
have rw₁ : IsBounded s ↔ IsBounded s
Tactic: rw [← isBounded_image_ofSnowflaking_iff, image_ofSnowflaking_image_toSnowflaking]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : Bornology X
s : Set X
⊢ IsBounded (α := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) ↔ IsBounded s
have rw : IsBounded (α := Snowflaking X α hα₀ hα₁) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' s) ↔ IsBounded s
Tactic: rw [← image_toSnowflaking_eq_preimage, isBounded_image_toSnowflaking_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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
⊢ IsBounded (α := Snowflaking X α hα₀ hα₁) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s) ↔ IsBounded s
have rw₁ : IsBounded s ↔ IsBounded s
Tactic: rw [← image_toSnowflaking_eq_preimage, isBounded_image_toSnowflaking_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : EDist X
x y : Snowflaking X α hα₀ hα₁
⊢ edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) =
    edist x y ^ α⁻¹
have 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) ^
      α) ^
    α⁻¹
Tactic: rw [edist_def, ENNReal.rpow_rpow_inv hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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) ^
        α) ^
      α⁻¹
⊢ edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) =
    edist x y ^ α⁻¹
have 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)
Tactic: rw [edist_def, ENNReal.rpow_rpow_inv 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 y : Snowflaking X α hα₀ hα₁
⊢ edist x y = edist y x
have rw : edist (α := X) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X)
      ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) y : X) ^
    α =
  edist y x
Tactic: rw [edist_def, edist_def, edist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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
⊢ edist x y = edist y x
have 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) ^
    α
Tactic: rw [edist_def, edist_def, edist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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) ^
      α
⊢ edist x y = edist y x
have 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) ^
    α
Tactic: rw [edist_def, edist_def, edist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x y z : Snowflaking X α hα₀ hα₁
⊢ 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) ^
        α
have h₁ : 0 ≤ α
Tactic: grw [edist_triangle x.ofSnowflaking y.ofSnowflaking z.ofSnowflaking,
      ENNReal.rpow_add_le_add_rpow _ _ hα₀.le hα₁]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
x y z : Snowflaking X α hα₀ hα₁
h₁ : 0 ≤ α
⊢ 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) ^
        α
have 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) ^
      α
Tactic: grw [edist_triangle x.ofSnowflaking y.ofSnowflaking z.ofSnowflaking,
      ENNReal.rpow_add_le_add_rpow _ _ hα₀.le hα₁]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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) ^
        α
⊢ 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) ^
        α
have 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) ^
      α
Tactic: grw [edist_triangle x.ofSnowflaking y.ofSnowflaking z.ofSnowflaking,
      ENNReal.rpow_add_le_add_rpow _ _ hα₀.le hα₁]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
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 ^ α⁻¹}
have refine : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), (ε ^ α) ^ α⁻¹ ≤ ε
Tactic: refine EMetric.mk_uniformity_basis (fun _ _ ↦ by positivity) fun ε hε ↦
        ⟨ε ^ α, by positivity, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace X
ε : ℝ≥0∞
hε : 0 < ε
⊢ (ε ^ α) ^ α⁻¹ ≤ ε
have rw : ε ≤ ε
Tactic: rw [ENNReal.rpow_rpow_inv hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (hypothesis)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoEMetricSpace 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 < ε})
have H : (𝓤 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']
-- 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) ⁻¹' eball x r : Set (Snowflaking X α hα₀ hα₁))
    (eball ((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) ⁻¹' 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: 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α₁) '' eball x r : Set (Snowflaking X α hα₀ hα₁))
    (eball ((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) ⁻¹' 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]
-- 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) ⁻¹' eball 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α₁))
have 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α₁))
Tactic: rw [image_toSnowflaking_eq_preimage, preimage_ofSnowflaking_eball]
-- 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α₁) ⁻¹' eball x d : Set X)
    (eball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
have 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)
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_eball,
    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 :
  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)
⊢ 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)
have rw₁ : eball x d =
  eball
    ((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_eball,
    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 :
  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 ^ α⁻¹) ^ α)
⊢ 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)
have rw₂ : eball x d = eball x ((d ^ α⁻¹) ^ α)
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_eball,
    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 :
  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 ^ α⁻¹) ^ α)
⊢ 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)
have rw₃ : eball x d = eball x d
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_eball,
    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) '' eball x d : Set X)
    (eball ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (d ^ α⁻¹) : Set X)
have 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)
Tactic: rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_eball]