awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
r₁ r₂ : ℝ
hp₁o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)
hp₁ :
  p₁ =
    r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
hp₂o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P)
hp₂ :
  p₂ =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
h : s.points 0 ∈ span_s
hd₁ :
  r₁ * r₁ *
      ⟪p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P),
        p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)⟫ =
    r₂ * r₂ *
      ⟪p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P),
        p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)⟫
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : ¬p = (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P)
hz :
  ⟪p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P),
      p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P)⟫ ≠
    0
hd₃ : r₁ = r₂ ∨ r₁ = -r₂
⊢ dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius

Tactic:
rw [mul_left_inj' hz, mul_self_eq_mul_self_iff] at hd₁

Premises used: mul_self_eq_mul_self_iff, mul_left_inj'
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
r₁ r₂ : ℝ
hp₁o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)
hp₁ :
  p₁ =
    r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
hp₂o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P)
hp₂ :
  p₂ =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
h : s.points 0 ∈ span_s
hd₁ :
  r₁ * r₁ *
      ⟪p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P),
        p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)⟫ =
    r₂ * r₂ *
      ⟪p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P),
        p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)⟫
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : ¬p = (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P)
hz :
  ⟪p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P),
      p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P)⟫ ≠
    0
hd₃ : r₁ = r₂ ∨ r₁ = -r₂
hd₄ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
⊢ ¬p = (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P)

Tactic:
rw [mul_left_inj' hz, mul_self_eq_mul_self_iff] at hd₁

Premises used: mul_self_eq_mul_self_iff, mul_left_inj'
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
r₁ r₂ : ℝ
hp₁o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)
hp₁ :
  p₁ =
    r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
hp₂o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P)
hp₂ :
  p₂ =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
h : s.points 0 ∈ span_s
hd₁ :
  r₁ * r₁ *
      ⟪p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P),
        p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)⟫ =
    r₂ * r₂ *
      ⟪p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P),
        p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)⟫
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : ¬p = (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P)
hz :
  ⟪p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P),
      p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P)⟫ ≠
    0
hd₃ : r₁ = r₂ ∨ r₁ = -r₂
hd₄ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp₃ : ¬p = (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P)
⊢ ⟪p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P),
      p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P)⟫ ≠
    0

Tactic:
rw [mul_left_inj' hz, mul_self_eq_mul_self_iff] at hd₁

Premises used: mul_self_eq_mul_self_iff, mul_left_inj'
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
r₁ r₂ : ℝ
hp₁o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)
hp₁ :
  p₁ =
    r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
hp₂o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P)
hp₂ :
  p₂ =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
h : s.points 0 ∈ span_s
hd₁ : r₁ = r₂ ∨ r₁ = -r₂
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : ¬p = (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P)
hz :
  ⟪p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P),
      p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P)⟫ ≠
    0
neg :
  r₁ •
          (p -ᵥ
            (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                    (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                  p) :
              P)) +ᵥ
        s.circumcenter =
      r₂ •
          (p -ᵥ
            (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                    (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                  p) :
              P)) +ᵥ
        s.circumcenter ∨
    r₁ •
          (p -ᵥ
            (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                    (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                  p) :
              P)) +ᵥ
        s.circumcenter =
      (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P)
        (r₂ •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          s.circumcenter)
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂

Tactic:
rw [hp₁, hp₂]
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
r₁ r₂ : ℝ
hp₁o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)
hp₁ :
  p₁ =
    r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
hp₂o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P)
hp₂ :
  p₂ =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
h : s.points 0 ∈ span_s
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : ¬p = (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P)
hz :
  ⟪p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P),
      p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P)⟫ ≠
    0
hd₁ : r₁ = r₂
neg neg₁ :
  r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
⊢ r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter

Tactic:
rw [hd₁]
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
t₁ : Fin 3 → P₁
t₂ : Fin 3 → P₂
⊢ t₁ ≅ t₂ ↔ ∀ (i j : Fin 3), dist (t₁ i) (t₁ j) = dist (t₂ i) (t₂ j)

Tactic:
congruent_iff_dist_eq

Premises used: congruent_iff_dist_eq
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
rw : ∀ (i j : Fin 3), dist (![a, b, c] i) (![a, b, c] j) = dist (![a', b', c'] i) (![a', b', c'] j)
⊢ ![a, b, c] ≅ ![a', b', c']

Tactic:
rw [triangle_congruent_iff_dist_eq]

Premises used: EuclideanGeometry.triangle_congruent_iff_dist_eq
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
i j : Fin 3
0 :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a, b, c] j) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a', b', c'] j)
1 :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a, b, c] j) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a', b', c'] j)
2 :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a, b, c] j) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a', b', c'] j)
⊢ dist (![a, b, c] i) (![a, b, c] j) = dist (![a', b', c'] i) (![a', b', c'] j)

Tactic:
fin_cases i
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
j : Fin 3
0 :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩))
h :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩))
h_1 :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩))
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a, b, c] j) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a', b', c'] j)

Tactic:
fin_cases j
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
j : Fin 3
1 :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩))
h :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩))
h_1 :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩))
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a, b, c] j) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a', b', c'] j)

Tactic:
fin_cases j
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
j : Fin 3
2 :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩))
h :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩))
h_1 :
  dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩))
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a, b, c] j) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a', b', c'] j)

Tactic:
fin_cases j
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩))

Tactic:
simp_all [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩))

Tactic:
simp_all [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩))

Tactic:
simp_all [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩))

Tactic:
simp_all [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩))

Tactic:
simp_all [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩))

Tactic:
simp_all [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩))

Tactic:
simp_all [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩))

Tactic:
simp_all [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
P₁ : Type u_4
P₂ : Type u_5
inst : MetricSpace P₁
inst_1 : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) =
    dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩))

Tactic:
simp_all [dist_comm]

Premises used: dist_comm