awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have hd₃ : r₁ = r₂ ∨ r₁ = -r₂
Tactic: rw [mul_left_inj' hz, mul_self_eq_mul_self_iff] at hd₁
Cleared hypotheses: hd₁, hd₂, hp, hz
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have 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)
Tactic: rw [hp₁, hp₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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₂
⊢ 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
have 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
Tactic: rw [hd₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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₂
⊢ 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)
have neg : -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)
Tactic: rw [hd₁, reflection_vadd_smul_vsub_orthogonalProjection p r₂ s.circumcenter_mem_affineSpan,
        neg_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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'
⊢ ![a, b, c] ≅ ![a', b', c']
have rw : ∀ (i j : Fin 3), dist (![a, b, c] i) (![a, b, c] j) = dist (![a', b', c'] i) (![a', b', c'] j)
Tactic: rw [triangle_congruent_iff_dist_eq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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
⊢ dist (![a, b, c] i) (![a, b, c] j) = dist (![a', b', c'] i) (![a', b', c'] j)
have 0 : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) (![a, b, c] j) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) (![a', b', c'] j)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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)
⊢ dist (![a, b, c] i) (![a, b, c] j) = dist (![a', b', c'] i) (![a', b', c'] j)
have 1 : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) (![a, b, c] j) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) (![a', b', c'] j)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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)
⊢ dist (![a, b, c] i) (![a, b, c] j) = dist (![a', b', c'] i) (![a', b', c'] j)
have 2 : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) (![a, b, c] j) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) (![a', b', c'] j)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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
⊢ 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)
have 0 : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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, ⋯⟩))
⊢ 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)
have 0₁ : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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, ⋯⟩))
⊢ 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)
have 0₁ : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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
⊢ 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)
have 1 : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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, ⋯⟩))
⊢ 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)
have 1₁ : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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, ⋯⟩))
⊢ 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)
have 1₁ : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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
⊢ 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)
have 2 : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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, ⋯⟩))
⊢ 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)
have 2₁ : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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, ⋯⟩))
⊢ 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)
have 2₁ : dist (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) (![a, b, c] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) =
  dist (![a', b', c'] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) (![a', b', c'] ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h : ∠ a b c = ∠ a' b' c'
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
⊢ ![a, b, c] ≅ ![a', b', c']
have apply : dist c a = dist c' a'
Tactic: apply side_side_side hd₁ hd₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h : ∠ a b c = ∠ a' b' c'
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
⊢ dist c a = dist c' a'
have rw : dist a b * dist a b + dist c b * dist c b - 2 * dist a b * dist c b * Real.cos (∠ a b c) =
  dist a' b' * dist a' b' + dist c' b' * dist c' b' - 2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c')
Tactic: rw [dist_comm, dist_comm c' a', ← sq_eq_sq₀ (by positivity) (by positivity), pow_two, pow_two,
    EuclideanGeometry.law_cos a b c, EuclideanGeometry.law_cos a' b' c']