awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)
hs₁ : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)
⊢ o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)

Tactic:
rw [h, Real.Angle.sign_add_pi, SignType.neg_eq_self_iff, oangle_sign_sub_left_swap,
      o.oangle_rev, Real.Angle.sign_neg, SignType.neg_eq_zero_iff,
      Real.Angle.sign_eq_zero_iff] at hs

Premises used: Orientation.oangle_sign_sub_left_swap, Real.Angle.sign_neg, SignType.neg_eq_zero_iff, SignType.neg_eq_self_iff, Real.Angle.sign_eq_zero_iff, Real.Angle.sign_add_pi, Orientation.oangle_rev
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)
h : o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)
⊢ ‖x‖ = ‖y‖

Tactic:
simp [h0, hpi] at hs
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
rw :
  ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ - 2 * ‖p₁ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ * Real.cos (∠ p₁ p₂ p₃)
⊢ dist p₁ p₃ * dist p₁ p₃ =
    dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ - 2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (∠ p₁ p₂ p₃)

Tactic:
rw [dist_eq_norm_vsub V p₁ p₃, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₃ p₂]

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
⊢ ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ * ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ -
      2 * ‖p₁ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ * Real.cos (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))

Tactic:
norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle (p₁ -ᵥ p₂ : V)
      (p₃ -ᵥ p₂ : V)

Premises used: VSub.vsub, InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h h₁ : p₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)
⊢ ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ -
      2 * ‖p₁ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ * Real.cos (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))

Tactic:
convert!
    norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle (p₁ -ᵥ p₂ : V)
      (p₃ -ᵥ p₂ : V)

Premises used: VSub.vsub, InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)

Tactic:
(vsub_sub_vsub_cancel_right p₁ p₃ p₂).symm

Premises used: vsub_sub_vsub_cancel_right, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)

Tactic:
exact (vsub_sub_vsub_cancel_right p₁ p₃ p₂).symm

Premises used: vsub_sub_vsub_cancel_right, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
simp :
  Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) * dist p₃ p₂ =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁)) * dist p₃ p₁
⊢ Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁

Tactic:
simp only [dist_comm p₂ p₃, angle]

Premises used: dist_comm, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
rw :
  Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₁)) =
      Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁)) ∨
    ‖p₃ -ᵥ p₁‖ = 0
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) * dist p₃ p₂ =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁)) * dist p₃ p₁

Tactic:
rw [dist_eq_norm_vsub V p₃ p₂, dist_eq_norm_vsub V p₃ p₁, InnerProductGeometry.angle_comm,
    sin_angle_mul_norm_eq_sin_angle_mul_norm, vsub_sub_vsub_cancel_right, mul_eq_mul_right_iff]

Premises used: InnerProductGeometry.sin_angle_mul_norm_eq_sin_angle_mul_norm, mul_eq_mul_right_iff, InnerProductGeometry.angle_comm, vsub_sub_vsub_cancel_right, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h :
  Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₁)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₁)) =
      Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁)) ∨
    ‖p₃ -ᵥ p₁‖ = 0

Tactic:
left
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h :
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))
h₁ :
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (-(p₁ -ᵥ p₂)))
h₂ :
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (π - InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂))
h₃ h₄ :
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂))
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₁)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))

Tactic:
rw [InnerProductGeometry.angle_comm, ← neg_vsub_eq_vsub_rev p₁ p₂, angle_neg_right,
    Real.sin_pi_sub]

Premises used: Real.sin_pi_sub, InnerProductGeometry.angle_neg_right, InnerProductGeometry.angle_comm, neg_vsub_eq_vsub_rev
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h23 : p₂ ≠ p₃
h31 : p₃ ≠ p₁
simp : Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁
⊢ Real.sin (∠ p₁ p₂ p₃) / dist p₃ p₁ = Real.sin (∠ p₃ p₁ p₂) / dist p₂ p₃

Tactic:
simp [field, dist_ne_zero.mpr h23, dist_ne_zero.mpr h31, mul_comm (dist ..)]

Premises used: Iff.mpr, dist_ne_zero, mul_comm, Dist.dist
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h23 : p₂ ≠ p₃
h31 : p₃ ≠ p₁
⊢ Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁

Tactic:
law_sin _ _ _

Premises used: EuclideanGeometry.law_sin
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h23 : p₂ ≠ p₃
h31 : p₃ ≠ p₁
⊢ Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁

Tactic:
exact law_sin _ _ _

Premises used: EuclideanGeometry.law_sin
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ 0 < Real.sin (∠ p₁ p₂ p₃)

Tactic:
have sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃) := sin_pos_of_not_collinear h
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃)
field_simp : dist p₁ p₂ * Real.sin (∠ p₁ p₂ p₃) = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)
⊢ dist p₁ p₂ = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁) / Real.sin (∠ p₁ p₂ p₃)

Tactic:
field_simp
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃)
rw : Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)
rw₁ : Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = Real.sin (∠ p₂ p₃ p₁) * dist p₃ p₁
rw₂ rw₃ : Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂
⊢ dist p₁ p₂ * Real.sin (∠ p₁ p₂ p₃) = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)

Tactic:
rw [mul_comm, mul_comm (dist p₃ p₁), law_sin]

Premises used: EuclideanGeometry.law_sin, mul_comm, Dist.dist
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : dist p₁ p₂ = dist p₁ p₃
⊢ ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖

Tactic:
rw [dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃] at h

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) =
    InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂))

Tactic:
angle_sub_eq_angle_sub_rev_of_norm_eq h

Premises used: InnerProductGeometry.angle_sub_eq_angle_sub_rev_of_norm_eq
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
h₁ : p₃ -ᵥ p₂ = p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)
h₂ : p₂ -ᵥ p₃ = p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)

Tactic:
convert! angle_sub_eq_angle_sub_rev_of_norm_eq h

Premises used: InnerProductGeometry.angle_sub_eq_angle_sub_rev_of_norm_eq
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₃ -ᵥ p₂ = p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)

Tactic:
(vsub_sub_vsub_cancel_left p₃ p₂ p₁).symm

Premises used: vsub_sub_vsub_cancel_left, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₃ -ᵥ p₂ = p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)

Tactic:
exact (vsub_sub_vsub_cancel_left p₃ p₂ p₁).symm

Premises used: vsub_sub_vsub_cancel_left, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₂ -ᵥ p₃ = p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)

Tactic:
(vsub_sub_vsub_cancel_left p₂ p₃ p₁).symm

Premises used: vsub_sub_vsub_cancel_left, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₂ -ᵥ p₃ = p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)

Tactic:
exact (vsub_sub_vsub_cancel_left p₂ p₃ p₁).symm

Premises used: vsub_sub_vsub_cancel_left, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
hpi : InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁) ≠ π
rw : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ dist p₁ p₂ = dist p₁ p₃

Tactic:
rw [dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃]

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
hpi : InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁) ≠ π
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) ≠ π

Tactic:
rw [← angle_neg_neg, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev] at hpi

Premises used: neg_vsub_eq_vsub_rev, InnerProductGeometry.angle_neg_neg
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
hpi : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) ≠ π
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) =
    InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂))

Tactic:
rw [← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁] at h

Premises used: vsub_sub_vsub_cancel_left
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
hpi : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) ≠ π
h₁ :
  InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) =
    InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂))
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) ≠ π

Tactic:
rw [← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁] at h

Premises used: vsub_sub_vsub_cancel_left
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h :
  InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) =
    InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂))
hpi : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) ≠ π
⊢ ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖

Tactic:
norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi h hpi

Premises used: InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
p₁ p₂ p₃ : P
h :
  InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) =
    InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂))
hpi : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) ≠ π
⊢ ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖

Tactic:
exact norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi h hpi

Premises used: InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ ‖p₂ -ᵥ p₁‖ = ‖p₃ -ᵥ p₁‖

Tactic:
(Orientation.norm_eq_of_two_zsmul_oangle_sub_eq (x := p₃ -ᵥ p₁) (y := p₂ -ᵥ p₁) ?_ ?_ h0
        hpi).symm

Premises used: Orientation.norm_eq_of_two_zsmul_oangle_sub_eq, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
h₁ h₂ : ‖p₂ -ᵥ p₁‖ = ‖p₂ -ᵥ p₁‖
⊢ dist p₁ p₂ = ‖p₂ -ᵥ p₁‖

Tactic:
rw [dist_eq_norm_vsub']

Premises used: dist_eq_norm_vsub'
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
h₁ h₂ : ‖p₃ -ᵥ p₁‖ = ‖p₃ -ᵥ p₁‖
⊢ dist p₁ p₃ = ‖p₃ -ᵥ p₁‖

Tactic:
rw [dist_eq_norm_vsub']

Premises used: dist_eq_norm_vsub'
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
rw :
  HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)))
⊢ HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) (p₂ -ᵥ p₁))

Tactic:
rw [eq_comm, o.oangle_rev, ← o.oangle_neg_neg]

Premises used: eq_comm, Orientation.oangle_rev, EuclideanGeometry.o, Orientation.oangle_neg_neg
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
nth_rw :
  HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁)))
⊢ HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)))

Tactic:
nth_rw 2 [o.oangle_rev, ← o.oangle_neg_neg]

Premises used: Orientation.oangle_rev, EuclideanGeometry.o, Orientation.oangle_neg_neg
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁)
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
simp_rw :
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁)))
⊢ HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (-Orientation.oangle o (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁)))

Tactic:
simp_rw [smul_neg, neg_inj]

Premises used: smul_neg, neg_inj
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h :
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃))
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃))

Tactic:
h
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h :
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃))
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
h₁ : -(p₂ -ᵥ p₁) = p₁ -ᵥ p₂
h₂ : -(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) = p₃ -ᵥ p₂
h₃ : -(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) = p₂ -ᵥ p₃
h₄ : -(p₃ -ᵥ p₁) = p₁ -ᵥ p₃
⊢ HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₂ -ᵥ p₁)) (-(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)))) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (-(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))) (-(p₃ -ᵥ p₁)))

Tactic:
convert! h
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h :
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃))
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ -(p₂ -ᵥ p₁) = p₁ -ᵥ p₂

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h :
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃))
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ -(p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) = p₃ -ᵥ p₂

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h :
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃))
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ -(p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) = p₂ -ᵥ p₃

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inst_4 : Module.Oriented ℝ V (Fin 2)
inst_5 : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h :
  HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) =
    HSMul.hSMul (α := ℤ) 2 (Orientation.oangle o (p₂ -ᵥ p₃) (p₁ -ᵥ p₃))
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ (↑π : Real.Angle)
⊢ -(p₃ -ᵥ p₁) = p₁ -ᵥ p₃

Tactic:
simp