awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
refine_1 :
  ∀ (k : β),
    nndist.{u_4} (α := Y) (Pi.single (M := fun (a : β) ↦ Y) i a k : Y) (Pi.single (M := fun (j : β) ↦ Y) j b k : Y) ≤
      max (nndist a 0) (nndist b 0)
refine_2 :
  nndist a 0 ≤ nndist (α := (j : β) → Y) (Pi.single (M := fun (a : β) ↦ Y) i a) (Pi.single (M := fun (j : β) ↦ Y) j b)
⊢ nndist (α := (j : β) → Y) (Pi.single (M := fun (a : β) ↦ Y) i a) (Pi.single (M := fun (j : β) ↦ Y) j b) =
    max (nndist a 0) (nndist b 0)
have refine_3 : nndist b 0 ≤ nndist (α := (j : β) → Y) (Pi.single (M := fun (a : β) ↦ Y) i a) (Pi.single (M := fun (j : β) ↦ Y) j b)
Tactic: refine le_antisymm (nndist_pi_le_iff.2 fun k ↦ ?_) (max_le ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
⊢ nndist.{u_4} (α := Y) (Pi.single (M := fun (a : β) ↦ Y) i a k : Y) (Pi.single (M := fun (j : β) ↦ Y) j b k : Y) ≤
    max (nndist a 0) (nndist b 0)
have refine_1 : nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Tactic: simp only [Pi.single_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
have pos : ∀ (hki : k = i), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Tactic: by_cases hki : k = i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
pos : ∀ (hki : k = i), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
have neg : ∀ (hki : ¬k = i), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Tactic: by_cases hki : k = i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
have pos : ∀ (hkj : k = j), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Tactic: by_cases hkj : k = j
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
pos : ∀ (hkj : k = j), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
have neg : ∀ (hkj : ¬k = j), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Tactic: by_cases hkj : k = j
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
have pos : ∀ (hkj : k = j), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Tactic: by_cases hkj : k = j
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
pos : ∀ (hkj : k = j), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
have neg : ∀ (hkj : ¬k = j), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
Tactic: by_cases hkj : k = j
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
⊢ dist x y ≤ dist x' y'
have refine_1 : ∀ (b : ι), x b ∈ uIcc (x' b) (y' b)
Tactic: refine (dist_pi_le_iff dist_nonneg).2 fun b =>
    (Real.dist_le_of_mem_uIcc ?_ ?_).trans (dist_le_pi_dist x' y' b)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
refine_1 : ∀ (b : ι), x b ∈ uIcc (x' b) (y' b)
⊢ dist x y ≤ dist x' y'
have refine_2 : ∀ (b : ι), y b ∈ uIcc (x' b) (y' b)
Tactic: refine (dist_pi_le_iff dist_nonneg).2 fun b =>
    (Real.dist_le_of_mem_uIcc ?_ ?_).trans (dist_le_pi_dist x' y' b)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ x b ∈ uIcc (x' b) (y' b)
have refine_1 : x b ∈ Icc (x' b) (y' b)
Tactic: refine Icc_subset_uIcc ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Real (goal)
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ y b ∈ uIcc (x' b) (y' b)
have refine_2 : y b ∈ Icc (x' b) (y' b)
Tactic: refine Icc_subset_uIcc ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ShrinkingLemma (goal)
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
have rcases : ∀ (v : ι → Set α) (hsv : s ⊆ iUnion v)
  (hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i))
  (hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)), ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
Tactic: rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with
    ⟨v, hsv, hvc, hcv⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ShrinkingLemma (hypothesis)
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
have this : ∀ (i : ι), ∃ r' < r i, v i ⊆ ball (c i) r'
Tactic: have := fun i => exists_lt_subset_ball (hvc i) (hcv i)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ShrinkingLemma (goal)
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
this : ∀ (i : ι), ∃ r' < r i, v i ⊆ ball (c i) r'
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
have choose : ∀ (r' : (i : ι) → ℝ) (hlt : ∀ (i : ι), r' i < r i) (hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)),
  ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
Tactic: choose r' hlt hsub using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ShrinkingLemma (goal)
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
have rcases : ∀ (v : ι → Set α) (hsv : s ⊆ iUnion v)
  (hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i))
  (hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)),
  ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
Tactic: rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with
    ⟨v, hsv, hvc, hcv⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ShrinkingLemma (hypothesis)
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
have this : ∀ (i : ι), ∃ r' ∈ Ioo 0 (r i), v i ⊆ ball (c i) r'
Tactic: have := fun i => exists_pos_lt_subset_ball (hr i) (hvc i) (hcv i)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ShrinkingLemma (goal)
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
this : ∀ (i : ι), ∃ r' ∈ Ioo 0 (r i), v i ⊆ ball (c i) r'
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
have choose : ∀ (r' : (i : ι) → ℝ) (hlt : ∀ (i : ι), r' i ∈ Ioo 0 (r i)) (hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)),
  ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
Tactic: choose r' hlt hsub using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ShrinkingLemma (hypothesis)
Goal:
α : Type u
inst : MetricSpace α
inst_1 : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
⊢ ∃ (ι : Type u) (c : ι → α) (r : ι → ℝ) (r' : ι → ℝ),
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite (X := α) fun (i : ι) ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
have this : ∀ x ∈ s, (𝓝 x).HasBasis (fun (r : ℝ) ↦ 0 < r ∧ r < R x) fun (r : ℝ) ↦ ball x r
Tactic: have : ∀ x ∈ s, (𝓝 x).HasBasis (fun r : ℝ => 0 < r ∧ r < R x) fun r => ball x r := fun x hx =>
    nhds_basis_uniformity (uniformity_basis_dist_lt (hR x hx))
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ShrinkingLemma (goal)
Goal:
α : Type u
inst : MetricSpace α
inst_1 : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (fun (r : ℝ) ↦ 0 < r ∧ r < R x) fun (r : ℝ) ↦ ball x r
⊢ ∃ (ι : Type u) (c : ι → α) (r : ι → ℝ) (r' : ι → ℝ),
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite (X := α) fun (i : ι) ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
have rcases : ∀ (ι : Type u) (c : ι → α) (r' : (a : ι) → ℝ) (hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a))
  (hsub' : s ⊆ ⋃ (a : ι), ball (c a) (r' a)) (hfin : LocallyFinite (X := α) fun (a : ι) ↦ ball (c a) (r' a)),
  ∃ (ι : Type u) (c : ι → α) (r : ι → ℝ) (r' : ι → ℝ),
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite (X := α) fun (i : ι) ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
Tactic: rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs this with
    ⟨ι, c, r', hr', hsub', hfin⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ShrinkingLemma (goal)
Goal:
α : Type u
inst : MetricSpace α
inst_1 : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (fun (r : ℝ) ↦ 0 < r ∧ r < R x) fun (r : ℝ) ↦ ball x r
ι : Type u
c : ι → α
r' : (a : ι) → ℝ
hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a)
hsub' : s ⊆ ⋃ (a : ι), ball (c a) (r' a)
hfin : LocallyFinite (X := α) fun (a : ι) ↦ ball (c a) (r' a)
⊢ ∃ (ι : Type u) (c : ι → α) (r : ι → ℝ) (r' : ι → ℝ),
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite (X := α) fun (i : ι) ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
have rcases : ∀ (r : ι → ℝ) (hsub : s ⊆ ⋃ (i : ι), ball (c i) (r i)) (hlt : ∀ (i : ι), r i ∈ Ioo 0 (r' i)),
  ∃ (ι : Type u) (c : ι → α) (r : ι → ℝ) (r' : ι → ℝ),
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite (X := α) fun (i : ι) ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
Tactic: rcases exists_subset_iUnion_ball_radius_pos_lt (fun i => (hr' i).2.1) hs
      (fun x _ => hfin.point_finite x) hsub' with
    ⟨r, hsub, hlt⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
⊢ (∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
have refine_1 : (∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)) →
  ∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
refine_1 :
  (∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)) →
    ∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
⊢ (∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
have refine_2 : (∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)) →
  ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
⊢ ∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
have refine_1 : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → (fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)) i₁ i₂
Tactic: refine ⟨r, hr, fun i₁ i₂ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
r : ℝ≥0
hr : r ≠ 0
h : Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
⊢ ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
have refine_2 : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
Tactic: refine ⟨r, hr, fun i₁ i₂ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
r : ℝ≥0
hr : r ≠ 0
h : Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
⊢ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
have pos : ∀ (hi : i₁ = i₂), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
Tactic: by_cases hi : i₁ = i₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
r : ℝ≥0
hr : r ≠ 0
h : Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
pos : ∀ (hi : i₁ = i₂), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
⊢ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
have neg : ∀ (hi : ¬i₁ = i₂), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
Tactic: by_cases hi : i₁ = i₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
inst : PseudoEMetricSpace P₁
v₁ : ι → P₁
x x_1 : ι
⊢ edist (v₁ x) (v₁ x_1) = 1 * edist (v₁ x) (v₁ x_1)
have rw : edist (v₁ x) (v₁ x_1) = edist (v₁ x) (v₁ x_1)
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
inst : PseudoEMetricSpace P₁
v₁ : ι → P₁
x x_1 : ι
⊢ edist (v₁ x) (v₁ x_1) = (↑1 : ENNReal) * edist (v₁ x) (v₁ x_1)
have rw : edist (v₁ x) (v₁ x_1) = 1 * edist (v₁ x) (v₁ x_1)
Tactic: {norm_cast; rw [one_mul]}
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
h : v₁ ∼ v₂
⊢ v₂ ∼ v₁
have rcases : ∀ (r : ℝ≥0) (hr : r ≠ 0) (h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)), v₂ ∼ v₁
Tactic: rcases h with ⟨r, hr, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
⊢ v₂ ∼ v₁
have refine : ∀ (x x_1 : ι), edist (v₂ x) (v₂ x_1) = (↑r⁻¹ : ENNReal) * edist (v₁ x) (v₁ x_1)
Tactic: refine ⟨r⁻¹, inv_ne_zero hr, fun _ _ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
x x_1 : ι
⊢ edist (v₂ x) (v₂ x_1) = (↑r⁻¹ : ENNReal) * edist (v₁ x) (v₁ x_1)
have rw : (↑r : ENNReal) ≠ 0
Tactic: rw [ENNReal.coe_inv hr, ← ENNReal.div_eq_inv_mul, ENNReal.eq_div_iff _ ENNReal.coe_ne_top, h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
x x_1 : ι
⊢ (↑r : ENNReal) ≠ 0
have norm_cast : ¬r = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
v₃ : ι → P₃
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
h₁ : v₁ ∼ v₂
h₂ : v₂ ∼ v₃
⊢ v₁ ∼ v₃
have rcases : ∀ (r₁ : ℝ≥0) (hr₁ : r₁ ≠ 0) (h₁ : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r₁ : ENNReal) * edist (v₂ i₁) (v₂ i₂)),
  v₁ ∼ v₃
Tactic: rcases h₁ with ⟨r₁, hr₁, h₁⟩
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
v₃ : ι → P₃
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
h₂ : v₂ ∼ v₃
r₁ : ℝ≥0
hr₁ : r₁ ≠ 0
h₁ : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r₁ : ENNReal) * edist (v₂ i₁) (v₂ i₂)
⊢ v₁ ∼ v₃
have rcases : ∀ (r₂ : ℝ≥0) (hr₂ : r₂ ≠ 0) (h₂ : ∀ (i₁ i₂ : ι), edist (v₂ i₁) (v₂ i₂) = (↑r₂ : ENNReal) * edist (v₃ i₁) (v₃ i₂)),
  v₁ ∼ v₃
Tactic: rcases h₂ with ⟨r₂, hr₂, h₂⟩
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
v₃ : ι → P₃
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
r₁ : ℝ≥0
hr₁ : r₁ ≠ 0
h₁ : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r₁ : ENNReal) * edist (v₂ i₁) (v₂ i₂)
r₂ : ℝ≥0
hr₂ : r₂ ≠ 0
h₂ : ∀ (i₁ i₂ : ι), edist (v₂ i₁) (v₂ i₂) = (↑r₂ : ENNReal) * edist (v₃ i₁) (v₃ i₂)
⊢ v₁ ∼ v₃
have refine : ∀ (x x_1 : ι), edist (v₁ x) (v₁ x_1) = (↑(r₁ * r₂) : ENNReal) * edist (v₃ x) (v₃ x_1)
Tactic: refine ⟨r₁ * r₂, mul_ne_zero hr₁ hr₂, fun _ _ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
v₃ : ι → P₃
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
r₁ : ℝ≥0
hr₁ : r₁ ≠ 0
h₁ : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r₁ : ENNReal) * edist (v₂ i₁) (v₂ i₂)
r₂ : ℝ≥0
hr₂ : r₂ ≠ 0
h₂ : ∀ (i₁ i₂ : ι), edist (v₂ i₁) (v₂ i₂) = (↑r₂ : ENNReal) * edist (v₃ i₁) (v₃ i₂)
x x_1 : ι
⊢ edist (v₁ x) (v₁ x_1) = (↑(r₁ * r₂) : ENNReal) * edist (v₃ x) (v₃ x_1)
have rw : edist (v₁ x) (v₁ x_1) = (↑r₁ : ENNReal) * (↑r₂ : ENNReal) * edist (v₃ x) (v₃ x_1)
Tactic: rw [ENNReal.coe_mul, mul_assoc, h₁, h₂]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
v₃ : ι → P₃
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
r₁ : ℝ≥0
hr₁ : r₁ ≠ 0
h₁ : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r₁ : ENNReal) * edist (v₂ i₁) (v₂ i₂)
r₂ : ℝ≥0
hr₂ : r₂ ≠ 0
h₂ : ∀ (i₁ i₂ : ι), edist (v₂ i₁) (v₂ i₂) = (↑r₂ : ENNReal) * edist (v₃ i₁) (v₃ i₂)
x x_1 : ι
rw : edist (v₁ x) (v₁ x_1) = (↑r₁ : ENNReal) * (↑r₂ : ENNReal) * edist (v₃ x) (v₃ x_1)
⊢ edist (v₁ x) (v₁ x_1) = (↑(r₁ * r₂) : ENNReal) * edist (v₃ x) (v₃ x_1)
have rw₁ : edist (v₁ x) (v₁ x_1) = (↑r₁ : ENNReal) * ((↑r₂ : ENNReal) * edist (v₃ x) (v₃ x_1))
Tactic: rw [ENNReal.coe_mul, mul_assoc, h₁, h₂]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
v₃ : ι → P₃
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
r₁ : ℝ≥0
hr₁ : r₁ ≠ 0
h₁ : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r₁ : ENNReal) * edist (v₂ i₁) (v₂ i₂)
r₂ : ℝ≥0
hr₂ : r₂ ≠ 0
h₂ : ∀ (i₁ i₂ : ι), edist (v₂ i₁) (v₂ i₂) = (↑r₂ : ENNReal) * edist (v₃ i₁) (v₃ i₂)
x x_1 : ι
rw : edist (v₁ x) (v₁ x_1) = (↑r₁ : ENNReal) * (↑r₂ : ENNReal) * edist (v₃ x) (v₃ x_1)
rw₁ : edist (v₁ x) (v₁ x_1) = (↑r₁ : ENNReal) * ((↑r₂ : ENNReal) * edist (v₃ x) (v₃ x_1))
⊢ edist (v₁ x) (v₁ x_1) = (↑(r₁ * r₂) : ENNReal) * edist (v₃ x) (v₃ x_1)
have rw₂ : (↑r₁ : ENNReal) * edist (v₂ x) (v₂ x_1) = (↑r₁ : ENNReal) * ((↑r₂ : ENNReal) * edist (v₃ x) (v₃ x_1))
Tactic: rw [ENNReal.coe_mul, mul_assoc, h₁, h₂]