awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
x : ℝ≥0
x_1 x_2 : ι
⊢ (↑(nndist (v₁ x_1) (v₁ x_2)) : ENNReal) = (↑x : ENNReal) * (↑(nndist (v₂ x_1) (v₂ x_2)) : ENNReal) ↔
    nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2)
have norm_cast : nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2) ↔ nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2)
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
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
x : ℝ≥0
x_1 x_2 : ι
⊢ edist (v₁ x_1) (v₁ x_2) = (↑x : ENNReal) * edist (v₂ x_1) (v₂ x_2) ↔
    nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2)
have rw : (↑(nndist (v₁ x_1) (v₁ x_2)) : ENNReal) = (↑x : ENNReal) * edist (v₂ x_1) (v₂ x_2) ↔
  nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2)
Tactic: { rw [edist_nndist, edist_nndist]; norm_cast }
-- 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 : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
x : ℝ≥0
x_1 x_2 : ι
rw :
  (↑(nndist (v₁ x_1) (v₁ x_2)) : ENNReal) = (↑x : ENNReal) * edist (v₂ x_1) (v₂ x_2) ↔
    nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2)
⊢ edist (v₁ x_1) (v₁ x_2) = (↑x : ENNReal) * edist (v₂ x_1) (v₂ x_2) ↔
    nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2)
have rw₁ : (↑(nndist (v₁ x_1) (v₁ x_2)) : ENNReal) = (↑x : ENNReal) * (↑(nndist (v₂ x_1) (v₂ x_2)) : ENNReal) ↔
  nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2)
Tactic: { rw [edist_nndist, edist_nndist]; norm_cast }
-- 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 : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)
have simp_rw : (∃ (r : ℝ≥0),
    r ≠ 0 ∧
      Pairwise fun (i₁ i₂ : ι) ↦
        (↑(nndist (v₁ i₁) (v₁ i₂)) : ENNReal) = (↑r : ENNReal) * (↑(nndist (v₂ i₁) (v₂ i₂)) : ENNReal)) ↔
  ∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)
Tactic: simp_rw [similar_iff_exists_pairwise_edist_eq, edist_nndist]
-- 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 : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
x : ℝ≥0
x_1 x_2 : ι
⊢ nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2) ↔ dist (v₁ x_1) (v₁ x_2) = (↑x : ℝ) * dist (v₂ x_1) (v₂ x_2)
have rw : nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2) ↔
  (↑(nndist (v₁ x_1) (v₁ x_2)) : ℝ) = (↑x : ℝ) * (↑(nndist (v₂ x_1) (v₂ x_2)) : ℝ)
Tactic: rw [dist_nndist, dist_nndist]
-- 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 : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
x : ℝ≥0
x_1 x_2 : ι
⊢ nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2) ↔
    (↑(nndist (v₁ x_1) (v₁ x_2)) : ℝ) = (↑x : ℝ) * (↑(nndist (v₂ x_1) (v₂ x_2)) : ℝ)
have norm_cast : nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2) ↔ nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2)
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
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
x : ℝ≥0
x_1 x_2 : ι
⊢ nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2) ↔ dist (v₁ x_1) (v₁ x_2) = (↑x : ℝ) * dist (v₂ x_1) (v₂ x_2)
have rw : nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2) ↔
  (↑(nndist (v₁ x_1) (v₁ x_2)) : ℝ) = (↑x : ℝ) * dist (v₂ x_1) (v₂ x_2)
Tactic: { rw [dist_nndist, dist_nndist]; norm_cast }
-- 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 : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
x : ℝ≥0
x_1 x_2 : ι
rw :
  nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2) ↔
    (↑(nndist (v₁ x_1) (v₁ x_2)) : ℝ) = (↑x : ℝ) * dist (v₂ x_1) (v₂ x_2)
⊢ nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2) ↔ dist (v₁ x_1) (v₁ x_2) = (↑x : ℝ) * dist (v₂ x_1) (v₂ x_2)
have rw₁ : nndist (v₁ x_1) (v₁ x_2) = x * nndist (v₂ x_1) (v₂ x_2) ↔
  (↑(nndist (v₁ x_1) (v₁ x_2)) : ℝ) = (↑x : ℝ) * (↑(nndist (v₂ x_1) (v₂ x_2)) : ℝ)
Tactic: { rw [dist_nndist, dist_nndist]; norm_cast }
-- 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 : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ (r : ℝ≥0), r ≠ 0 ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = (↑r : ℝ) * dist (v₂ i₁) (v₂ i₂)
have 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₂)) : ℝ)
Tactic: simp_rw [similar_iff_exists_pairwise_nndist_eq, dist_nndist]
-- 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 : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ (r : ℝ), 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
have 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₂)
Tactic: rw [similar_iff_exists_dist_eq]
-- 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 : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ (∃ (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₂)
have 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₂)
Tactic: simp_rw [← pos_iff_ne_zero, NNReal.exists, ← NNReal.coe_pos, NNReal.coe_mk]
-- 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 : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ (r : ℝ), 0 < r ∧ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
have 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₂)
Tactic: simp_rw [similar_iff_exists_pairwise_dist_eq]
-- 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 : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ (∃ (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₂)
have 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₂)
Tactic: simp_rw [← pos_iff_ne_zero, NNReal.exists, ← NNReal.coe_pos, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (hypothesis)
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'
⊢ Similar ![a, b, c] ![a', b', c']
have hr : 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (hypothesis)
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'
⊢ Similar ![a, b, c] ![a', b', c']
have hr_pos : 0 < r
Tactic: have hr_pos : 0 < r := by positivity
-- 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
⊢ Similar ![a, b, c] ![a', b', c']
have 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₂)
Tactic: apply Similar.of_exists_pos_pairwise_dist_eq
-- 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
⊢ ∃ (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₂)
have 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₂)
Tactic: use r
-- 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
⊢ 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₂)
have 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₂)
Tactic: refine ⟨hr_pos, ?_⟩
-- 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
i j : Fin (Nat.succ 0).succ.succ
hij : i ≠ j
⊢ dist (![a, b, c] i) (![a, b, c] j) = r * dist (![a', b', c'] i) (![a', b', c'] j)
have h : ∀ (hij : (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩ ≠ j),
  dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : 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, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] j)
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- 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
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)
⊢ dist (![a, b, c] i) (![a, b, c] j) = r * dist (![a', b', c'] i) (![a', b', c'] j)
have h₁ : ∀ (hij : (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩ ≠ j),
  dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : 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, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] j)
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- 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
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)
⊢ dist (![a, b, c] i) (![a, b, c] j) = r * dist (![a', b', c'] i) (![a', b', c'] j)
have h₂ : ∀ (hij : (fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩ ≠ j),
  dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : 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, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] j)
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- 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
j : Fin (Nat.succ 0).succ.succ
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)
have h : ∀
  (hij :
    Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)),
  dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ))) =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
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)))
⊢ 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)
have h₁ : ∀
  (hij :
    Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)),
  dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ))) =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
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)))
⊢ 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)
have h₂ : ∀
  (hij :
    Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)),
  dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ))) =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
j : Fin (Nat.succ 0).succ.succ
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)
have h : ∀
  (hij :
    Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)),
  dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ))) =
    r *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)))
Tactic: fin_cases j
Cleared hypotheses: j, hij