awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Similarity
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
f : P₂ → P₃
hf : Isometry f
⊢ v₁ ∼ f ∘ v₂ ↔ v₁ ∼ v₂

Tactic:
comp_right_iff hf.toDilation

Premises used: Similar.comp_right_iff, Isometry.toDilation
-- Module: Mathlib.Topology.MetricSpace.Similarity
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']
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
⊢ ![b, a, c] = ![a, b, c] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)

Tactic:
ext i
-- Module: Mathlib.Topology.MetricSpace.Similarity
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, ⋯⟩)
h₃ :
  ![b, a, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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, ⋯⟩)
⊢ ![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:
fin_cases i
-- Module: Mathlib.Topology.MetricSpace.Similarity
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] ((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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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] ((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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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)

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]
-- Module: Mathlib.Topology.MetricSpace.Similarity
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)
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
⊢ ![b', a', c'] = ![a', b', c'] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)

Tactic:
ext i
-- Module: Mathlib.Topology.MetricSpace.Similarity
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, ⋯⟩)
h₃ :
  ![b', a', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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, ⋯⟩)
⊢ ![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:
fin_cases i
-- Module: Mathlib.Topology.MetricSpace.Similarity
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'] ((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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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'] ((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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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)

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]
-- Module: Mathlib.Topology.MetricSpace.Similarity
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)
hr : ![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']

Tactic:
grind [index_equiv]

Premises used: Similar.index_equiv
-- Module: Mathlib.Topology.MetricSpace.Similarity
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']
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
⊢ ![a, c, b] = ![a, b, c] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)

Tactic:
ext i
-- Module: Mathlib.Topology.MetricSpace.Similarity
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, ⋯⟩)
h₃ :
  ![a, c, b] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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, ⋯⟩)
⊢ ![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:
fin_cases i
-- Module: Mathlib.Topology.MetricSpace.Similarity
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] ((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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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] ((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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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)

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]
-- Module: Mathlib.Topology.MetricSpace.Similarity
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)
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
⊢ ![a', c', b'] = ![a', b', c'] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)

Tactic:
ext i
-- Module: Mathlib.Topology.MetricSpace.Similarity
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, ⋯⟩)
h₃ :
  ![a', c', b'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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, ⋯⟩)
⊢ ![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:
fin_cases i
-- Module: Mathlib.Topology.MetricSpace.Similarity
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'] ((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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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'] ((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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : 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, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Topology.MetricSpace.Similarity
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)

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]
-- Module: Mathlib.Topology.MetricSpace.Similarity
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)
hr : ![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']

Tactic:
grind [index_equiv]

Premises used: Similar.index_equiv
-- Module: Mathlib.Topology.MetricSpace.Similarity
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']
⊢ ![c, b, a] ∼ ![c', b', a']

Tactic:
h.comm_left.comm_right.comm_left

Premises used: Similar.comm_right, Similar.comm_left
-- 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_1 x_2 : ι
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)
⊢ 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)

Tactic:
rw [edist_nndist, edist_nndist]

Premises used: edist_nndist
-- 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_1 x_2 : ι
norm_cast norm_cast₁ norm_cast₂ 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)
⊢ (↑(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:
norm_cast
-- 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_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)
rw₁ rw₂ rw₃ 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)
⊢ 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)

Tactic:
{ rw [edist_nndist, edist_nndist]; norm_cast }

Premises used: edist_nndist
-- 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₂)) : 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₂)
⊢ Similar v₁ v₂ ↔ ∃ (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]

Premises used: similar_iff_exists_pairwise_edist_eq, edist_nndist
-- 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₂)) : 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:
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₂
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 : ℝ) * (↑(nndist (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)

Tactic:
rw [dist_nndist, dist_nndist]

Premises used: dist_nndist
-- 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_1 x_2 : ι
norm_cast norm_cast₁ norm_cast₂ 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)
⊢ 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
-- 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_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)
rw₁ rw₂ rw₃ 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)) : ℝ)
⊢ 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)

Tactic:
{ rw [dist_nndist, dist_nndist]; norm_cast }

Premises used: dist_nndist