awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
-- 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:
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) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
h :
  0 =
    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)))
h₁ : 0 = r * 0
h₂ h₃ : Eq (α := ℝ) 0 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) (⟨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)))

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) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
h :
  0 =
    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)))
h₁ : 0 = r * 0
h₂ h₃ : Eq (α := ℝ) 0 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) (⟨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)))

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) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
h :
  0 =
    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)))
h₁ : 0 = r * 0
h₂ h₃ : Eq (α := ℝ) 0 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) (⟨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)))

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) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
h : dist a b = r * dist a' b'
⊢ 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)))

Tactic:
simp
-- 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) ⟨1, ⋯⟩)
⊢ dist a b = r * dist a' b'

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- 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) ⟨2, ⋯⟩)
h : dist a c = r * dist a' c'
⊢ 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)))

Tactic:
simp
-- 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) ⟨2, ⋯⟩)
⊢ dist a c = r * dist a' c'

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- 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) ⟨0, ⋯⟩)
h : dist b a = r * dist b' a'
⊢ 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)))

Tactic:
simp
-- 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) ⟨0, ⋯⟩)
⊢ dist b a = r * dist b' a'

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- 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) ⟨2, ⋯⟩)
h : dist b c = r * dist b' c'
⊢ 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)))

Tactic:
simp
-- 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) ⟨2, ⋯⟩)
⊢ dist b c = r * dist b' c'

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- 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) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h : dist c a = r * dist c' a'
⊢ 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)))

Tactic:
simp
-- 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) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ dist c a = r * dist c' a'

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- 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) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
h : dist c b = r * dist c' b'
⊢ 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)))

Tactic:
simp
-- 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) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ dist c b = r * dist c' b'

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : SizeOf X
x : X
⊢ sizeOf (α := Snowflaking X α hα₀ hα₁)
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁) =
    1 + sizeOf x

Tactic:
rfl

Premises used: Metric.Snowflaking._sizeOf_1, rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
⊢ Eq.{u_1 + 1} (α := (val : X) → Snowflaking X α hα₀ hα₁) mk (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
⊢ Eq.{u_1 + 1} (α := (self : Snowflaking X α hα₀ hα₁) → X) val (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
⊢ Eq.{u_1 + 1} (α := Snowflaking X α hα₀ hα₁ ≃ X) (Equiv.symm toSnowflaking) ofSnowflaking

Tactic:
rfl

Premises used: Equiv.symm, Metric.Snowflaking.ofSnowflaking, rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
⊢ Eq.{u_1 + 1} (α := X ≃ Snowflaking X α hα₀ hα₁) (Equiv.symm ofSnowflaking) toSnowflaking

Tactic:
rfl

Premises used: Metric.Snowflaking.toSnowflaking, rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
x : Snowflaking X α hα₀ hα₁
⊢ (toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
x : X
⊢ (ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) x : Snowflaking X α hα₀ hα₁) =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
⊢ Eq.{u_1 + 1} (α := X → X)
    (comp (β := Snowflaking X α hα₀ hα₁) (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
      (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
⊢ Eq.{u_1 + 1} (α := Snowflaking X α hα₀ hα₁ → Snowflaking X α hα₀ hα₁)
    (comp (β := X) (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁)
      (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
s : Set X
⊢ Eq (α := Set (Snowflaking X α hα₀ hα₁)) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' s)
    ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) ⁻¹' s)

Tactic:
toSnowflaking.image_eq_preimage_symm _

Premises used: Metric.Snowflaking.toSnowflaking, Equiv.image_eq_preimage_symm
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
s : Set (Snowflaking X α hα₀ hα₁)
⊢ Eq (α := Set X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s)
    ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s)

Tactic:
ofSnowflaking.image_eq_preimage_symm _

Premises used: Equiv.image_eq_preimage_symm, Metric.Snowflaking.ofSnowflaking
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
s : Set (Snowflaking X α hα₀ hα₁)
⊢ Set.image (α := X) (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁)
      ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) =
    s

Tactic:
ofSnowflaking.symm_image_image _

Premises used: Metric.Snowflaking.ofSnowflaking, Equiv.symm_image_image
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
s : Set X
⊢ Set.image (α := Snowflaking X α hα₀ hα₁) (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
      ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' s) =
    s

Tactic:
ofSnowflaking.image_symm_image _

Premises used: Equiv.image_symm_image, Metric.Snowflaking.ofSnowflaking
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : TopologicalSpace X
⊢ Continuous[instTopologicalSpace, inst] (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : TopologicalSpace X
⊢ Continuous[inst, instTopologicalSpace] (⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁)

Tactic:
continuous_induced_rng.2 continuous_id

Premises used: Iff.mpr, continuous_id, continuous_induced_rng
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : TopologicalSpace X
inst_1 : T0Space X
⊢ T0Space.{u_1} (Snowflaking X α hα₀ hα₁)

Tactic:
homeomorph.symm.t0Space

Premises used: Homeomorph.t0Space, Metric.Snowflaking.homeomorph, Homeomorph.symm
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : TopologicalSpace X
inst_1 : T2Space X
⊢ T2Space.{u_1} (Snowflaking X α hα₀ hα₁)

Tactic:
homeomorph.symm.t2Space

Premises used: Metric.Snowflaking.homeomorph, Homeomorph.symm, Homeomorph.t2Space
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : TopologicalSpace X
inst_1 : SecondCountableTopology X
⊢ SecondCountableTopology.{u_1} (Snowflaking X α hα₀ hα₁)

Tactic:
homeomorph.secondCountableTopology

Premises used: Homeomorph.secondCountableTopology, Metric.Snowflaking.homeomorph
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : Bornology X
s : Set (Snowflaking X α hα₀ hα₁)
⊢ IsBounded (α := X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) ↔ IsBounded s

Tactic:
isBounded_induced.symm

Premises used: Bornology.isBounded_induced, Iff.symm
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : Bornology X
s : Set (Snowflaking X α hα₀ hα₁)
rw : IsBounded (α := X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' s) ↔ IsBounded s
rw₁ rw₂ : IsBounded s ↔ IsBounded s
⊢ IsBounded (α := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' s) ↔ IsBounded s

Tactic:
rw [← image_ofSnowflaking_eq_preimage, isBounded_image_ofSnowflaking_iff]

Premises used: Metric.Snowflaking.isBounded_image_ofSnowflaking_iff, Metric.Snowflaking.image_ofSnowflaking_eq_preimage
-- Module: Mathlib.Topology.MetricSpace.Snowflaking
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : Bornology X
s : Set X
rw :
  IsBounded (α := X)
      (Set.image (α := Snowflaking X α hα₀ hα₁) (⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X)
        ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' s)) ↔
    IsBounded s
rw₁ rw₂ : IsBounded s ↔ IsBounded s
⊢ IsBounded (α := Snowflaking X α hα₀ hα₁) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) '' s) ↔ IsBounded s

Tactic:
rw [← isBounded_image_ofSnowflaking_iff, image_ofSnowflaking_image_toSnowflaking]

Premises used: Metric.Snowflaking.isBounded_image_ofSnowflaking_iff, Metric.Snowflaking.image_ofSnowflaking_image_toSnowflaking