awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
simp_rw :
  (∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ≥0),
      r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ (↑(nndist (v₁ i₁) (v₁ i₂)) : ℝ) = (↑r : ℝ) * (↑(nndist (v₂ i₁) (v₂ i₂)) : ℝ)
⊢ Similar v₁ v₂ ↔ ∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = (↑r : ℝ) * dist (v₂ i₁) (v₂ i₂)

Tactic:
simp_rw [similar_iff_exists_pairwise_nndist_eq, dist_nndist]

Premises used: dist_nndist, similar_iff_exists_pairwise_nndist_eq
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ (∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ≥0),
      r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ (↑(nndist (v₁ i₁) (v₁ i₂)) : ℝ) = (↑r : ℝ) * (↑(nndist (v₂ i₁) (v₂ i₂)) : ℝ)

Tactic:
exact_mod_cast Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
rw :
  (∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = (↑r : ℝ) * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ), 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
⊢ Similar v₁ v₂ ↔ ∃ (r : ℝ), 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
rw [similar_iff_exists_dist_eq]

Premises used: similar_iff_exists_dist_eq
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
simp_rw :
  (∃ (x : ℝ) (_ : 0 ≤ x), 0 < x ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = x * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ), 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
⊢ (∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = (↑r : ℝ) * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ), 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
simp_rw [← pos_iff_ne_zero, NNReal.exists, ← NNReal.coe_pos, NNReal.coe_mk]

Premises used: NNReal.coe_mk, NNReal.coe_pos, NNReal.exists, pos_iff_ne_zero
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ (∃ (x : ℝ) (_ : 0 ≤ x), 0 < x ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = x * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ), 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
grind
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
simp_rw :
  (∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = (↑r : ℝ) * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ), 0 < r ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
⊢ Similar v₁ v₂ ↔ ∃ (r : ℝ), 0 < r ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
simp_rw [similar_iff_exists_pairwise_dist_eq]

Premises used: similar_iff_exists_pairwise_dist_eq
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
simp_rw :
  (∃ (x : ℝ) (_ : 0 ≤ x), 0 < x ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = x * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ), 0 < r ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
⊢ (∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = (↑r : ℝ) * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ), 0 < r ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
simp_rw [← pos_iff_ne_zero, NNReal.exists, ← NNReal.coe_pos, NNReal.coe_mk]

Premises used: NNReal.coe_mk, NNReal.coe_pos, NNReal.exists, pos_iff_ne_zero
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ (∃ (x : ℝ) (_ : 0 ≤ x), 0 < x ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = x * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ (r : ℝ), 0 < r ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
grind
-- Module: Mathlib.Topology.MetricSpace.Similarity
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'
⊢ let r := dist a b / dist a' b';
  r = dist a b / dist a' b'

Tactic:
set r : ℝ := (dist a b / dist a' b') with hr

Premises used: HDiv.hDiv, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Similarity
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'
⊢ 0 < r

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Similarity
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'
⊢ 0 < r

Tactic:
have hr_pos : 0 < r := by positivity
-- Module: Mathlib.Topology.MetricSpace.Similarity
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
a₁ :
  ∃ (r : ℝ),
    0 < r ∧
      Pairwise fun (i₁ i₂ : Fin (Nat.succ 0).succ.succ) ↦
        dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
⊢ Similar ![a, b, c] ![a', b', c']

Tactic:
apply Similar.of_exists_pos_pairwise_dist_eq

Premises used: Similar.of_exists_pos_pairwise_dist_eq
-- Module: Mathlib.Topology.MetricSpace.Similarity
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
h :
  0 < r ∧
    Pairwise fun (i₁ i₂ : Fin (Nat.succ 0).succ.succ) ↦
      dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
⊢ ∃ (r : ℝ),
    0 < r ∧
      Pairwise fun (i₁ i₂ : Fin (Nat.succ 0).succ.succ) ↦
        dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)

Tactic:
use r
-- Module: Mathlib.Topology.MetricSpace.Similarity
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
⊢ 0 < r ∧
    Pairwise fun (i₁ i₂ : Fin (Nat.succ 0).succ.succ) ↦
      dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)

Tactic:
⟨hr_pos, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Topology.MetricSpace.Similarity
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
h :
  Pairwise fun (i₁ i₂ : Fin (Nat.succ 0).succ.succ) ↦
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
⊢ 0 < r ∧
    Pairwise fun (i₁ i₂ : Fin (Nat.succ 0).succ.succ) ↦
      dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)

Tactic:
refine ⟨hr_pos, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Similarity
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
i j : Fin (Nat.succ 0).succ.succ
hij : i ≠ j
h :
  ∀ (hij : (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩ ≠ j),
    dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a, b, c] j) =
      r *
        dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
          (![a', b', c'] j)
h₁ :
  ∀ (hij : (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩ ≠ j),
    dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a, b, c] j) =
      r *
        dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
          (![a', b', c'] j)
h₂ :
  ∀ (hij : (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩ ≠ j),
    dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a, b, c] j) =
      r *
        dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
          (![a', b', c'] j)
⊢ dist (![a, b, c] i) (![a, b, c] j) = r * dist (![a', b', c'] i) (![a', b', c'] j)

Tactic:
fin_cases i
-- Module: Mathlib.Topology.MetricSpace.Similarity
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
j : Fin (Nat.succ 0).succ.succ
hij : (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩ ≠ j
h :
  ∀
    (hij :
      Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)),
    dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : 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) (⟨0, ⋯⟩ : 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)))
h₁ :
  ∀
    (hij :
      Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)),
    dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : 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) (⟨0, ⋯⟩ : 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)))
h₂ :
  ∀
    (hij :
      Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)),
    dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : 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) (⟨0, ⋯⟩ : 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)))
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ))) (![a, b, c] j) =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] j)

Tactic:
fin_cases j
-- Module: Mathlib.Topology.MetricSpace.Similarity
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
j : Fin (Nat.succ 0).succ.succ
hij : (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩ ≠ j
h :
  ∀
    (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)))
h₁ :
  ∀
    (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) ⟨1, ⋯⟩)),
    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) (⟨1, ⋯⟩ : 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) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
h₂ :
  ∀
    (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)))
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ))) (![a, b, c] j) =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] j)

Tactic:
fin_cases j
-- Module: Mathlib.Topology.MetricSpace.Similarity
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
j : Fin (Nat.succ 0).succ.succ
hij : (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩ ≠ j
h :
  ∀
    (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)))
h₁ :
  ∀
    (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)))
h₂ :
  ∀
    (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) ⟨2, ⋯⟩)),
    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) (⟨2, ⋯⟩ : 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) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ))) (![a, b, c] j) =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] j)

Tactic:
fin_cases j
-- Module: Mathlib.Topology.MetricSpace.Similarity
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) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h :
  0 =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : 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)))
h₁ : 0 = r * 0
h₂ h₃ : Eq (α := ℝ) 0 0
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : 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) (⟨0, ⋯⟩ : 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)))

Tactic:
rw [dist_self, dist_self, mul_zero]

Premises used: MulZeroClass.mul_zero, dist_self
-- Module: Mathlib.Topology.MetricSpace.Similarity
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) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h :
  0 =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : 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)))
h₁ : 0 = r * 0
h₂ h₃ : Eq (α := ℝ) 0 0
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : 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) (⟨0, ⋯⟩ : 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)))

Tactic:
{rw [dist_self, dist_self, mul_zero]}

Premises used: MulZeroClass.mul_zero, dist_self
-- Module: Mathlib.Topology.MetricSpace.Similarity
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) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h :
  0 =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : 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)))
h₁ : 0 = r * 0
h₂ h₃ : Eq (α := ℝ) 0 0
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : 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) (⟨0, ⋯⟩ : 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)))

Tactic:
try {rw [dist_self, dist_self, mul_zero]}

Premises used: MulZeroClass.mul_zero, dist_self
-- Module: Mathlib.Topology.MetricSpace.Similarity
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) ⟨1, ⋯⟩)
h :
  0 =
    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) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
h₁ : 0 = r * 0
h₂ h₃ : Eq (α := ℝ) 0 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) (⟨1, ⋯⟩ : 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) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))

Tactic:
rw [dist_self, dist_self, mul_zero]

Premises used: MulZeroClass.mul_zero, dist_self