awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Congruence
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'
apply : dist c a = dist c' a'
⊢ ![a, b, c] ≅ ![a', b', c']

Tactic:
apply side_side_side hd₁ hd₂

Premises used: EuclideanGeometry.side_side_side
-- Module: Mathlib.Geometry.Euclidean.Congruence
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'
⊢ 0 ≤ dist a c

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Congruence
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'
⊢ 0 ≤ dist a' c'

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Congruence
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'
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')
⊢ dist c a = dist c' a'

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']

Premises used: pow_two, dist_comm, EuclideanGeometry.law_cos, sq_eq_sq₀
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 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:
simp [h, hd₁, hd₂, dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
⊢ ¬Collinear ℝ (P := P₂) {a', b', c'}

Tactic:
grind only [collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, angle_self_right,
      angle_self_left, dist_eq_zero, Set.insert_comm, Set.pair_comm]

Premises used: EuclideanGeometry.angle_self_right, Set.insert_comm, EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, dist_eq_zero, EuclideanGeometry.angle_self_left, Set.pair_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
⊢ ¬Collinear ℝ (P := P₂) {a', b', c'}

Tactic:
have h' : ¬Collinear ℝ {a', b', c'} := by
    grind only [collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, angle_self_right,
      angle_self_left, dist_eq_zero, Set.insert_comm, Set.pair_comm]
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
⊢ ∠ c a b + ∠ a b c + ∠ b c a = Real.pi

Tactic:
have ha₃ := angle_add_angle_add_angle_eq_pi b (ne₁₃_of_not_collinear h)
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
⊢ ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi

Tactic:
have ha₃' := angle_add_angle_add_angle_eq_pi b' (ne₁₃_of_not_collinear h')
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
⊢ ∠ c a b = ∠ c' a' b'

Tactic:
simp only [← ha₃', ha₁, ha₂, angle_comm b' c' a', add_right_cancel_iff] at ha₃

Premises used: EuclideanGeometry.angle_comm, add_right_cancel_iff
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
⊢ ¬Collinear ℝ (P := P₁) {b, a, c}

Tactic:
simpa [Set.insert_comm] using h

Premises used: Set.insert_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
⊢ ¬Collinear ℝ (P := P₁) {b, a, c}

Tactic:
have h_bac : ¬Collinear ℝ {b, a, c} := by simpa [Set.insert_comm] using h
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bac : ¬Collinear ℝ (P := P₁) {b, a, c}
⊢ ¬Collinear ℝ (P := P₂) {b', a', c'}

Tactic:
simpa [Set.insert_comm] using h'

Premises used: Set.insert_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bac : ¬Collinear ℝ (P := P₁) {b, a, c}
⊢ ¬Collinear ℝ (P := P₂) {b', a', c'}

Tactic:
have h_bac' : ¬Collinear ℝ {b', a', c'} := by simpa [Set.insert_comm] using h'
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bac : ¬Collinear ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
rw₁ : dist b a = dist b' a'
rw₂ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' a'
rw₃ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₄ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₅ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₆ : dist b' c' * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₇ : dist b' c' * Real.sin (∠ b c a) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₈ :
  dist b' c' * Real.sin (∠ b' c' a') / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₉ :
  dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₁₀ :
  dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ c a b) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₁₁ :
  dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ c' a' b') =
    dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₁₂ rw₁₃ :
  dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ c' a' b') =
    dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ c' a' b')
⊢ dist a b = dist a' b'

Tactic:
rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']

Premises used: EuclideanGeometry.angle_comm, dist_comm, EuclideanGeometry.dist_eq_dist_mul_sin_angle_div_sin_angle
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bac : ¬Collinear ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
⊢ dist a b = dist a' b'

Tactic:
have dist_ab_eq : dist a b = dist a' b' := by
    rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bac : ¬Collinear ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
dist_ab_eq : dist a b = dist a' b'
⊢ ![a, b, c] ≅ ![a', b', c']

Tactic:
side_angle_side ha₁ dist_ab_eq hd

Premises used: EuclideanGeometry.side_angle_side
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bac : ¬Collinear ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
dist_ab_eq : dist a b = dist a' b'
⊢ ![a, b, c] ≅ ![a', b', c']

Tactic:
exact side_angle_side ha₁ dist_ab_eq hd

Premises used: EuclideanGeometry.side_angle_side
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
⊢ ∠ c a b + ∠ a b c + ∠ b c a = Real.pi

Tactic:
have ha₃ := angle_add_angle_add_angle_eq_pi b (ne₁₃_of_not_collinear h)
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
⊢ ¬Collinear ℝ (P := P₂) {a', b', c'}

Tactic:
grind only [collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, angle_self_right,
      angle_self_left, dist_eq_zero, Set.insert_comm, Set.pair_comm]

Premises used: EuclideanGeometry.angle_self_right, Set.insert_comm, EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, dist_eq_zero, EuclideanGeometry.angle_self_left, Set.pair_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
⊢ ¬Collinear ℝ (P := P₂) {a', b', c'}

Tactic:
have h' : ¬Collinear ℝ {a', b', c'} := by
    grind only [collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, angle_self_right,
      angle_self_left, dist_eq_zero, Set.insert_comm, Set.pair_comm]
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
⊢ ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi

Tactic:
have ha₃' := angle_add_angle_add_angle_eq_pi b' (ne₁₃_of_not_collinear h')
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
⊢ ∠ c a b = ∠ c' a' b'

Tactic:
simp only [← ha₃', ha₁, ha₂, angle_comm b' c' a', add_right_cancel_iff] at ha₃

Premises used: EuclideanGeometry.angle_comm, add_right_cancel_iff
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
rwa :
  ∀ (h : ¬Collinear ℝ (P := P₁) {b, a, c}) (ha₁ : ∠ a b c = ∠ a' b' c') (ha₂ : ∠ b c a = ∠ b' c' a')
    (hd : dist c a = dist c' a') (h' : ¬Collinear ℝ (P := P₂) {a', b', c'})
    (ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi) (ha₃ : ∠ c a b = ∠ c' a' b'),
    ¬Collinear ℝ (P := P₁) {b, c, a}
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h : ¬Collinear ℝ (P := P₁) {b, c, a}) (ha₁ : ∠ a b c = ∠ a' b' c') (ha₂ : ∠ b c a = ∠ b' c' a')
    (hd : dist c a = dist c' a') (h' : ¬Collinear ℝ (P := P₂) {a', b', c'})
    (ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi) (ha₃ : ∠ c a b = ∠ c' a' b'),
    ¬Collinear ℝ (P := P₁) {b, c, a}
⊢ ¬Collinear ℝ (P := P₁) {b, c, a}

Tactic:
rwa [Set.insert_comm, Set.pair_comm] at h

Premises used: Set.insert_comm, Set.pair_comm
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
⊢ ¬Collinear ℝ (P := P₁) {b, c, a}

Tactic:
have h_bca : ¬Collinear ℝ {b, c, a} := by rwa [Set.insert_comm, Set.pair_comm] at h
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bca : ¬Collinear ℝ (P := P₁) {b, c, a}
⊢ ![b, c, a] ≅ ![b', c', a']

Tactic:
have h1 := angle_side_angle h_bca ha₂ hd ha₃
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bca : ¬Collinear ℝ (P := P₁) {b, c, a}
h1 : ![b, c, a] ≅ ![b', c', a']
⊢ ![a, b, c] ≅ ![a', b', c']

Tactic:
angle_side_angle h ha₁ (h1.dist_eq 0 1) ha₂

Premises used: EuclideanGeometry.angle_side_angle, OfNat.ofNat, Congruent.dist_eq
-- Module: Mathlib.Geometry.Euclidean.Congruence
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bca : ¬Collinear ℝ (P := P₁) {b, c, a}
h1 : ![b, c, a] ≅ ![b', c', a']
⊢ ![a, b, c] ≅ ![a', b', c']

Tactic:
exact angle_side_angle h ha₁ (h1.dist_eq 0 1) ha₂

Premises used: EuclideanGeometry.angle_side_angle, OfNat.ofNat, Congruent.dist_eq