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
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))
⊢ edist (v₁ x) (v₁ x_1) = (↑(r₁ * r₂) : ENNReal) * edist (v₃ x) (v₃ x_1)
have rw₃ : (↑r₁ : ENNReal) * ((↑r₂ : ENNReal) * edist (v₃ x) (v₃ x_1)) =
  (↑r₁ : ENNReal) * ((↑r₂ : ENNReal) * edist (v₃ x) (v₃ x_1))
Tactic: rw [ENNReal.coe_mul, mul_assoc, h₁, h₂]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
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 : ι' → ι
⊢ v₁ ∘ f ∼ v₂ ∘ f
have 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
Tactic: rcases h with ⟨r, hr, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
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
have refine : ∀ (x x_1 : ι'), edist ((v₁ ∘ f) x) ((v₁ ∘ f) x_1) = (↑r : ENNReal) * edist ((v₂ ∘ f) x) ((v₂ ∘ f) x_1)
Tactic: refine ⟨r, hr, fun _ _ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
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₂
have refine : ∀ (h : 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⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
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 : ι') → ι))
⊢ v₁ ∼ v₂
have 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₂
Tactic: rcases h with ⟨r, hr, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
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₂
have refine : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = (↑r : ENNReal) * edist (v₂ i₁) (v₂ i₂)
Tactic: refine ⟨r, hr, fun i₁ i₂ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
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_3, u_5} (P₂ := P₃) v₁ ((⇑f : (a : P₂) → P₃) ∘ v₂) ↔ v₁ ∼ v₂
have rw : Similar.{u_1, u_5, u_3} (P₁ := P₃) ((⇑f : (a : P₂) → P₃) ∘ v₂) v₁ ↔ v₁ ∼ v₂
Tactic: rw [similar_comm, comp_left_iff, similar_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
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₂
⊢ Similar.{u_1, u_3, u_5} (P₂ := P₃) v₁ ((⇑f : (a : P₂) → P₃) ∘ v₂) ↔ v₁ ∼ v₂
have rw₁ : v₂ ∼ v₁ ↔ v₁ ∼ v₂
Tactic: rw [similar_comm, comp_left_iff, similar_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
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₂
⊢ Similar.{u_1, u_3, u_5} (P₂ := P₃) v₁ ((⇑f : (a : P₂) → P₃) ∘ v₂) ↔ v₁ ∼ v₂
have rw₂ : v₁ ∼ v₂ ↔ v₁ ∼ v₂
Tactic: rw [similar_comm, comp_left_iff, similar_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
⊢ ![b, a, c] = ![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
have h₁ : ∀ (i : Fin (Nat.succ 0).succ.succ),
  ![b, a, c] i = (![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
i : Fin (Nat.succ 0).succ.succ
⊢ ![b, a, c] i = (![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₁ : ![b, a, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
    (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
i : Fin (Nat.succ 0).succ.succ
h₁ :
  ![b, a, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
      (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![b, a, c] i = (![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₂ : ![b, a, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
    (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
i : Fin (Nat.succ 0).succ.succ
h₁ :
  ![b, a, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
      (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₂ :
  ![b, a, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
      (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![b, a, c] i = (![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₃ : ![b, a, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
    (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (hypothesis)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
⊢ ![b, a, c] ∼ ![b', a', c']
have hl : ![b, a, c] = ![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
Tactic: have hl : ![b, a, c] = ![a, b, c] ∘ Equiv.swap 0 1 := by
    ext i
    fin_cases i <;> simp [Equiv.swap_apply_of_ne_of_ne]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![b, a, c] = ![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
⊢ ![b', a', c'] = ![a', b', c'] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
have h₁ : ∀ (i : Fin (Nat.succ 0).succ.succ),
  ![b', a', c'] i =
    (![a', b', c'] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![b, a, c] = ![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
i : Fin (Nat.succ 0).succ.succ
⊢ ![b', a', c'] i =
    (![a', b', c'] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₁ : ![b', a', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
    (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![b, a, c] = ![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
i : Fin (Nat.succ 0).succ.succ
h₁ :
  ![b', a', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
      (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![b', a', c'] i =
    (![a', b', c'] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₂ : ![b', a', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
    (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![b, a, c] = ![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
i : Fin (Nat.succ 0).succ.succ
h₁ :
  ![b', a', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
      (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₂ :
  ![b', a', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
      (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![b', a', c'] i =
    (![a', b', c'] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₃ : ![b', a', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
    (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (hypothesis)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![b, a, c] = ![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
⊢ ![b, a, c] ∼ ![b', a', c']
have hr : ![b', a', c'] = ![a', b', c'] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
Tactic: have hr : ![b', a', c'] = ![a', b', c'] ∘ Equiv.swap 0 1 := by
    ext i
    fin_cases i <;> simp [Equiv.swap_apply_of_ne_of_ne]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
⊢ ![a, c, b] = ![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
have h₁ : ∀ (i : Fin (Nat.succ 0).succ.succ),
  ![a, c, b] i = (![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
i : Fin (Nat.succ 0).succ.succ
⊢ ![a, c, b] i = (![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₁ : ![a, c, b] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
    (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
i : Fin (Nat.succ 0).succ.succ
h₁ :
  ![a, c, b] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
      (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![a, c, b] i = (![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₂ : ![a, c, b] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
    (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
i : Fin (Nat.succ 0).succ.succ
h₁ :
  ![a, c, b] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
      (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₂ :
  ![a, c, b] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
      (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![a, c, b] i = (![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₃ : ![a, c, b] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a, b, c]
    (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (hypothesis)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
⊢ ![a, c, b] ∼ ![a', c', b']
have hl : ![a, c, b] = ![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
Tactic: have hl : ![a, c, b] = ![a, b, c] ∘ Equiv.swap 1 2 := by
    ext i
    fin_cases i <;> simp [Equiv.swap_apply_of_ne_of_ne]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![a, c, b] = ![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
⊢ ![a', c', b'] = ![a', b', c'] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
have h₁ : ∀ (i : Fin (Nat.succ 0).succ.succ),
  ![a', c', b'] i =
    (![a', b', c'] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![a, c, b] = ![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
i : Fin (Nat.succ 0).succ.succ
⊢ ![a', c', b'] i =
    (![a', b', c'] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₁ : ![a', c', b'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
    (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![a, c, b] = ![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
i : Fin (Nat.succ 0).succ.succ
h₁ :
  ![a', c', b'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
      (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ ![a', c', b'] i =
    (![a', b', c'] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₂ : ![a', c', b'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
    (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (goal)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![a, c, b] = ![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
i : Fin (Nat.succ 0).succ.succ
h₁ :
  ![a', c', b'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
      (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₂ :
  ![a', c', b'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
      (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![a', c', b'] i =
    (![a', b', c'] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) i
have h₃ : ![a', c', b'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  Function.comp (α := Fin (Nat.succ 0).succ.succ) ![a', b', c']
    (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Similarity (hypothesis)
Goal:
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![a, c, b] = ![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
⊢ ![a, c, b] ∼ ![a', c', b']
have hr : ![a', c', b'] = ![a', b', c'] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
Tactic: have hr : ![a', c', b'] = ![a', b', c'] ∘ Equiv.swap 1 2 := by
    ext i
    fin_cases i <;> simp [Equiv.swap_apply_of_ne_of_ne]
-- 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) * (↑(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]