awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
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)
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:
⟨ι, c, r, r', fun i => ⟨(hr' i).1, (hlt i).1, (hlt i).2, (hr' i).2.2⟩, hfin, hsub⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
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)
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:
exact ⟨ι, c, r, r', fun i => ⟨(hr' i).1, (hlt i).1, (hlt i).2, (hr' i).2.2⟩, hfin, hsub⟩
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
inst : MetricSpace α
inst_1 : ProperSpace α
R : α → ℝ
hR : ∀ (x : α), 0 < R x
⊢ ∃ (ι : Type u) (c : ι → α) (r : ι → ℝ) (r' : ι → ℝ),
    (∀ (i : ι), 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite (X := α) fun (i : ι) ↦ ball (c i) (r' i)) ∧
        Eq.{u + 1} (α := Set α) (⋃ (i : ι), ball (c i) (r i)) univ

Tactic:
let ⟨ι, c, r, r', hlt, hfin, hsub⟩ :=
    exists_locallyFinite_subset_iUnion_ball_radius_lt isClosed_univ fun x _ => hR x
  ⟨ι, c, r, r', fun i => (hlt i).2, hfin, univ_subset_iff.1 hsub⟩

Premises used: isClosed_univ, Set.univ_subset_iff, Set.univ, Exists, Metric.ball, LocallyFinite, And, And.right, And.intro, Exists.intro, Iff.mp, exists_locallyFinite_subset_iUnion_ball_radius_lt, _private.0.exists_locallyFinite_iUnion_eq_ball_radius_lt.match_1, Eq, Set.iUnion
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Similar
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)
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₂)
⊢ (∃ (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 ⟨?_, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)

Tactic:
⟨r, hr, fun i₁ i₂ ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)
refine_1 :
  ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → (fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)) i₁ i₂
⊢ ∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)

Tactic:
refine ⟨r, hr, fun i₁ i₂ ↦ ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)

Tactic:
⟨r, hr, fun i₁ i₂ ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)
refine_2 : ∀ (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 ⟨r, hr, fun i₁ i₂ ↦ ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)
i₁ i₂ : ι
⊢ i₁ ≠ i₂ → (fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)) i₁ i₂

Tactic:
fun _ ↦ h i₁ i₂
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)
i₁ i₂ : ι
⊢ i₁ ≠ i₂ → (fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)) i₁ i₂

Tactic:
exact fun _ ↦ h i₁ i₂
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)
neg : ∀ (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₂)

Tactic:
by_cases hi : i₁ = i₂
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂ : ι
hi : i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)

Tactic:
simp [hi]
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂ : ι
hi : ¬i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)

Tactic:
h hi
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂ : ι
hi : ¬i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)

Tactic:
exact h hi
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ≅ v₂
i₁ i₂ : ι
⊢ edist (v₁ i₁) (v₁ i₂) = (↑1 : ENNReal) * edist (v₂ i₁) (v₂ i₂)

Tactic:
simpa using h i₁ i₂
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
inst : PseudoEMetricSpace P₁
v₁ : ι → P₁
x x_1 : ι
rw rw₁ : edist (v₁ x) (v₁ x_1) = edist (v₁ x) (v₁ x_1)
⊢ edist (v₁ x) (v₁ x_1) = 1 * edist (v₁ x) (v₁ x_1)

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
inst : PseudoEMetricSpace P₁
v₁ : ι → P₁
x x_1 : ι
rw rw₁ rw₂ rw₃ rw₄ rw₅ : edist (v₁ x) (v₁ x_1) = 1 * edist (v₁ x) (v₁ x_1)
⊢ edist (v₁ x) (v₁ x_1) = (↑1 : ENNReal) * edist (v₁ x) (v₁ x_1)

Tactic:
{norm_cast; rw [one_mul]}

Premises used: one_mul
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂
rcases :
  ∀ (r : ℝ≥0) (hr : r ≠ 0) (h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)), v₂ ∼ v₁
⊢ v₂ ∼ v₁

Tactic:
rcases h with ⟨r, hr, h⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₁

Tactic:
⟨r⁻¹, inv_ne_zero hr, fun _ _ => ?_⟩

Premises used: Similar, Inv.inv, And.intro, Exists.intro, inv_ne_zero
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)
refine : ∀ (x x_1 : ι), edist (v₂ x) (v₂ x_1) = (↑r⁻¹ : ENNReal) * edist (v₁ x) (v₁ x_1)
⊢ v₂ ∼ v₁

Tactic:
refine ⟨r⁻¹, inv_ne_zero hr, fun _ _ => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
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 : ι
rw : (↑r : ENNReal) ≠ 0
⊢ edist (v₂ x) (v₂ x_1) = (↑r⁻¹ : ENNReal) * edist (v₁ x) (v₁ x_1)

Tactic:
rw [ENNReal.coe_inv hr, ← ENNReal.div_eq_inv_mul, ENNReal.eq_div_iff _ ENNReal.coe_ne_top, h]

Premises used: ENNReal.coe_inv, ENNReal.div_eq_inv_mul, ENNReal.coe_ne_top, ENNReal.eq_div_iff
-- Module: Mathlib.Topology.MetricSpace.Similarity
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 : ι
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬r = 0
⊢ (↑r : ENNReal) ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
⊢ v₁ ∼ v₂ ↔ v₂ ∼ v₁

Tactic:
⟨Similar.symm, Similar.symm⟩

Premises used: Similar.symm, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₃
rcases :
  ∀ (r₁ : ℝ≥0) (hr₁ : r₁ ≠ 0) (h₁ : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r₁ : ENNReal) * edist (v₂ i₁) (v₂ i₂)),
    v₁ ∼ v₃
⊢ v₁ ∼ v₃

Tactic:
rcases h₁ with ⟨r₁, hr₁, h₁⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)
rcases :
  ∀ (r₂ : ℝ≥0) (hr₂ : r₂ ≠ 0) (h₂ : ∀ (i₁ i₂ : ι), edist (v₂ i₁) (v₂ i₂) = (↑r₂ : ENNReal) * edist (v₃ i₁) (v₃ i₂)),
    v₁ ∼ v₃
⊢ v₁ ∼ v₃

Tactic:
rcases h₂ with ⟨r₂, hr₂, h₂⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₃

Tactic:
⟨r₁ * r₂, mul_ne_zero hr₁ hr₂, fun _ _ => ?_⟩

Premises used: HMul.hMul, Similar, And.intro, Exists.intro, mul_ne_zero
-- Module: Mathlib.Topology.MetricSpace.Similarity
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₂)
refine : ∀ (x x_1 : ι), edist (v₁ x) (v₁ x_1) = (↑(r₁ * r₂) : ENNReal) * edist (v₃ x) (v₃ x_1)
⊢ v₁ ∼ v₃

Tactic:
refine ⟨r₁ * r₂, mul_ne_zero hr₁ hr₂, fun _ _ => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
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))
rw₂ : (↑r₁ : ENNReal) * edist (v₂ x) (v₂ x_1) = (↑r₁ : ENNReal) * ((↑r₂ : ENNReal) * edist (v₃ x) (v₃ x_1))
rw₃ rw₄ :
  (↑r₁ : ENNReal) * ((↑r₂ : ENNReal) * 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)

Tactic:
rw [ENNReal.coe_mul, mul_assoc, h₁, h₂]

Premises used: mul_assoc, ENNReal.coe_mul
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
h : v₁ ∼ v₂
f : ι' → ι
rcases :
  ∀ (r : ℝ≥0) (hr : r ≠ 0) (h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)),
    v₁ ∘ f ∼ v₂ ∘ f
⊢ v₁ ∘ f ∼ v₂ ∘ f

Tactic:
rcases h with ⟨r, hr, h⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
f : ι' → ι
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
⊢ v₁ ∘ f ∼ v₂ ∘ f

Tactic:
⟨r, hr, fun _ _ => ?_⟩

Premises used: Similar, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
f : ι' → ι
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
refine : ∀ (x x_1 : ι'), edist ((v₁ ∘ f) x) ((v₁ ∘ f) x_1) = (↑r : ENNReal) * edist ((v₂ ∘ f) x) ((v₂ ∘ f) x_1)
⊢ v₁ ∘ f ∼ v₂ ∘ f

Tactic:
refine ⟨r, hr, fun _ _ => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
f : ι' → ι
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₁ ∘ f) x) ((v₁ ∘ f) x_1) = (↑r : ENNReal) * edist ((v₂ ∘ f) x) ((v₂ ∘ f) x_1)

Tactic:
apply h
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
f : ι' ≃ ι
v₁ : ι → P₁
v₂ : ι → P₂
⊢ Similar.{u_2, u_3, u_4} (ι := ι') (v₁ ∘ (⇑f : (a : ι') → ι)) (v₂ ∘ (⇑f : (a : ι') → ι)) ↔ v₁ ∼ v₂

Tactic:
⟨fun h => ?_, fun h => Similar.index_map h f⟩

Premises used: Iff.intro, Similar.index_map, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
f : ι' ≃ ι
v₁ : ι → P₁
v₂ : ι → P₂
refine : ∀ (h : Similar.{u_2, u_3, u_4} (ι := ι') (v₁ ∘ (⇑f : (a : ι') → ι)) (v₂ ∘ (⇑f : (a : ι') → ι))), v₁ ∼ v₂
⊢ Similar.{u_2, u_3, u_4} (ι := ι') (v₁ ∘ (⇑f : (a : ι') → ι)) (v₂ ∘ (⇑f : (a : ι') → ι)) ↔ v₁ ∼ v₂

Tactic:
refine ⟨fun h => ?_, fun h => Similar.index_map h f⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
f : ι' ≃ ι
v₁ : ι → P₁
v₂ : ι → P₂
h : Similar.{u_2, u_3, u_4} (ι := ι') (v₁ ∘ (⇑f : (a : ι') → ι)) (v₂ ∘ (⇑f : (a : ι') → ι))
rcases :
  ∀ (r : ℝ≥0) (hr : r ≠ 0)
    (h :
      ∀ (i₁ i₂ : ι'),
        edist ((v₁ ∘ (⇑f : (a : ι') → ι)) i₁) ((v₁ ∘ (⇑f : (a : ι') → ι)) i₂) =
          (↑r : ENNReal) * edist ((v₂ ∘ (⇑f : (a : ι') → ι)) i₁) ((v₂ ∘ (⇑f : (a : ι') → ι)) i₂)),
    v₁ ∼ v₂
⊢ v₁ ∼ v₂

Tactic:
rcases h with ⟨r, hr, h⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
f : ι' ≃ ι
v₁ : ι → P₁
v₂ : ι → P₂
r : ℝ≥0
hr : r ≠ 0
h :
  ∀ (i₁ i₂ : ι'),
    edist ((v₁ ∘ (⇑f : (a : ι') → ι)) i₁) ((v₁ ∘ (⇑f : (a : ι') → ι)) i₂) =
      (↑r : ENNReal) * edist ((v₂ ∘ (⇑f : (a : ι') → ι)) i₁) ((v₂ ∘ (⇑f : (a : ι') → ι)) i₂)
⊢ v₁ ∼ v₂

Tactic:
⟨r, hr, fun i₁ i₂ => ?_⟩

Premises used: Similar, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
f : ι' ≃ ι
v₁ : ι → P₁
v₂ : ι → P₂
r : ℝ≥0
hr : r ≠ 0
h :
  ∀ (i₁ i₂ : ι'),
    edist ((v₁ ∘ (⇑f : (a : ι') → ι)) i₁) ((v₁ ∘ (⇑f : (a : ι') → ι)) i₂) =
      (↑r : ENNReal) * edist ((v₂ ∘ (⇑f : (a : ι') → ι)) i₁) ((v₂ ∘ (⇑f : (a : ι') → ι)) i₂)
refine : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
⊢ v₁ ∼ v₂

Tactic:
refine ⟨r, hr, fun i₁ i₂ => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
f : ι' ≃ ι
v₁ : ι → P₁
v₂ : ι → P₂
r : ℝ≥0
hr : r ≠ 0
h :
  ∀ (i₁ i₂ : ι'),
    edist ((v₁ ∘ (⇑f : (a : ι') → ι)) i₁) ((v₁ ∘ (⇑f : (a : ι') → ι)) i₂) =
      (↑r : ENNReal) * edist ((v₂ ∘ (⇑f : (a : ι') → ι)) i₁) ((v₂ ∘ (⇑f : (a : ι') → ι)) i₂)
i₁ i₂ : ι
⊢ edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)

Tactic:
simpa [f.right_inv i₁, f.right_inv i₂] using h (f.symm i₁) (f.symm i₂)

Premises used: Equiv.right_inv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : Subsingleton ι
⊢ v₁ ∼ v₂

Tactic:
Congruent.of_subsingleton_index.similar

Premises used: Congruent.of_subsingleton_index, Congruent.similar
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
F : Type u_6
inst_3 : FunLike F P₁ P₃
inst_4 : DilationClass F P₁ P₃
f : F
h : v₁ ∼ v₂
⊢ Similar.{u_1, u_5, u_4} (P₁ := P₃) ((⇑f : (a : P₁) → P₃) ∘ v₁) v₂

Tactic:
.trans ⟨Dilation.ratio f, Dilation.ratio_ne_zero f, fun _ _ => Dilation.edist_eq f _ _⟩ h

Premises used: Similar.trans, Dilation.edist_eq, Dilation.ratio, And.intro, Exists.intro, Dilation.ratio_ne_zero
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
F : Type u_6
inst_3 : FunLike F P₂ P₃
inst_4 : DilationClass F P₂ P₃
f : F
h : v₁ ∼ v₂
⊢ Similar.{u_1, u_3, u_5} (P₂ := P₃) v₁ ((⇑f : (a : P₂) → P₃) ∘ v₂)

Tactic:
.symm (h.symm.comp_left f)

Premises used: Similar.symm, Similar.comp_left
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
F : Type u_6
inst_3 : FunLike F P₁ P₃
inst_4 : DilationClass F P₁ P₃
f : F
⊢ Similar.{u_1, u_5, u_4} (P₁ := P₃) ((⇑f : (a : P₁) → P₃) ∘ v₁) v₂ ↔ v₁ ∼ v₂

Tactic:
⟨.trans <| .comp_right f (.refl _), .comp_left f⟩

Premises used: Similar.trans, Similar.comp_right, Similar.comp_left, Iff.intro, Similar.refl
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
F : Type u_6
inst_3 : FunLike F P₂ P₃
inst_4 : DilationClass F P₂ P₃
f : F
rw : Similar.{u_1, u_5, u_3} (P₁ := P₃) ((⇑f : (a : P₂) → P₃) ∘ v₂) v₁ ↔ v₁ ∼ v₂
rw₁ : v₂ ∼ v₁ ↔ v₁ ∼ v₂
rw₂ rw₃ : v₁ ∼ v₂ ↔ v₁ ∼ v₂
⊢ Similar.{u_1, u_3, u_5} (P₂ := P₃) v₁ ((⇑f : (a : P₂) → P₃) ∘ v₂) ↔ v₁ ∼ v₂

Tactic:
rw [similar_comm, comp_left_iff, similar_comm]

Premises used: similar_comm, Similar.comp_left_iff
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
f : P₁ → P₃
hf : Isometry f
h : v₁ ∼ v₂
⊢ f ∘ v₁ ∼ v₂

Tactic:
comp_left hf.toDilation h

Premises used: Isometry.toDilation, Similar.comp_left
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
f : P₂ → P₃
hf : Isometry f
h : v₁ ∼ v₂
⊢ v₁ ∼ f ∘ v₂

Tactic:
comp_right hf.toDilation h

Premises used: Similar.comp_right, Isometry.toDilation
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
f : P₁ → P₃
hf : Isometry f
⊢ f ∘ v₁ ∼ v₂ ↔ v₁ ∼ v₂

Tactic:
comp_left_iff hf.toDilation

Premises used: Isometry.toDilation, Similar.comp_left_iff