awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
rw : ∠ p₃ p₁ p₂ + ∠ p₁ p₃ p₂ + ∠ p₁ p₂ p₃ = π
⊢ ∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ = π

Tactic:
rw [add_assoc, add_comm, add_comm (∠ p₂ p₃ p₁), angle_comm p₂ p₃ p₁]

Premises used: EuclideanGeometry.angle_comm, add_assoc, add_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
h : p₂ ≠ p₁
rw :
  InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) +
      InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) =
    π
⊢ InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃) +
      InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) =
    π

Tactic:
rw [← angle_neg_neg (p₁ -ᵥ p₃), ← angle_neg_neg (p₁ -ᵥ p₂), neg_vsub_eq_vsub_rev,
    neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, ←
    vsub_sub_vsub_cancel_right p₃ p₂ p₁, ← vsub_sub_vsub_cancel_right p₂ p₃ p₁]

Premises used: VSub.vsub, vsub_sub_vsub_cancel_right, 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 : p₂ ≠ p₁
⊢ InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) +
      InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) =
    π

Tactic:
angle_add_angle_sub_add_angle_sub_eq_pi _ fun he => h (vsub_eq_zero_iff_eq.1 he)

Premises used: InnerProductGeometry.angle_add_angle_sub_add_angle_sub_eq_pi, vsub_eq_zero_iff_eq, Iff.mp
-- 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₁
⊢ InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) +
      InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) =
    π

Tactic:
exact angle_add_angle_sub_add_angle_sub_eq_pi _ fun he => h (vsub_eq_zero_iff_eq.1 he)

Premises used: InnerProductGeometry.angle_add_angle_sub_add_angle_sub_eq_pi, vsub_eq_zero_iff_eq, Iff.mp
-- 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
h : Sbtw ℝ p p₁ p₂
linarith :
  ∠ p₃ p₁ p < ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁ →
    ∠ p₃ p₁ p - (∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁) + -(∠ p₃ p₁ p + ∠ p₃ p₁ p₂ - π) + (∠ p₂ p₁ p₃ + ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁ - π) +
        (∠ p₃ p₁ p₂ - ∠ p₂ p₁ p₃) =
      0
linarith₁ :
  ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁ < ∠ p₃ p₁ p →
    ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁ - ∠ p₃ p₁ p + (∠ p₃ p₁ p + ∠ p₃ p₁ p₂ - π) + -(∠ p₂ p₁ p₃ + ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁ - π) +
        -(∠ p₃ p₁ p₂ - ∠ p₂ p₁ p₃) =
      0
⊢ ∠ p₃ p₁ p = ∠ p₁ p₃ p₂ + ∠ p₃ p₂ p₁

Tactic:
linarith [angle_add_angle_eq_pi_of_angle_eq_pi p₃ h.angle₁₂₃_eq_pi,
    angle_add_angle_add_angle_eq_pi p₃ h.right_ne.symm, angle_comm p₃ p₁ p₂]

Premises used: EuclideanGeometry.angle_comm, Sbtw.right_ne, Ne.symm, Sbtw.angle₁₂₃_eq_pi, EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi, EuclideanGeometry.angle_add_angle_add_angle_eq_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
h21 : p₂ ≠ p₁
h32 : p₃ ≠ p₂
h13 : p₁ ≠ p₃
⊢ ∡ p₁ p₂ p₃ + ∡ p₂ p₃ p₁ + ∡ p₃ p₁ p₂ = (↑π : Real.Angle)

Tactic:
simpa only [neg_vsub_eq_vsub_rev] using
    positiveOrientation.oangle_add_cyc3_neg_left (vsub_ne_zero.mpr h21) (vsub_ne_zero.mpr h32)
      (vsub_ne_zero.mpr h13)

Premises used: Iff.mpr, vsub_ne_zero, Orientation.oangle_add_cyc3_neg_left, neg_vsub_eq_vsub_rev, Module.Oriented.positiveOrientation
-- 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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pos : ∀ (pb : p = b), ∠ b a p + ∠ p a c = ∠ b a c
neg : ∀ (pb : ¬p = b), ∠ b a p + ∠ p a c = ∠ b a c
⊢ ∠ b a p + ∠ p a c = ∠ b a c

Tactic:
by_cases pb : p = b
-- 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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : p = b
⊢ ∠ b a p + ∠ p a c = ∠ b a c

Tactic:
simpa [pb] using angle_self_of_ne hb.symm

Premises used: EuclideanGeometry.angle_self_of_ne, Ne.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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pos : ∀ (pc : p = c), ∠ b a p + ∠ p a c = ∠ b a c
neg : ∀ (pc : ¬p = c), ∠ b a p + ∠ p a c = ∠ b a c
⊢ ∠ b a p + ∠ p a c = ∠ b a c

Tactic:
by_cases pc : p = c
-- 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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : p = c
⊢ ∠ b a p + ∠ p a c = ∠ b a c

Tactic:
simpa [pc] using angle_self_of_ne hc.symm

Premises used: EuclideanGeometry.angle_self_of_ne, Ne.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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : ¬p = c
⊢ ∠ b a c + ∠ a c b + ∠ c b a = π

Tactic:
have ea := angle_add_angle_add_angle_eq_pi c hb
-- 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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
⊢ ∠ b a p + ∠ a p b + ∠ p b a = π

Tactic:
have eb := angle_add_angle_add_angle_eq_pi p hb
-- 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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
⊢ ∠ b p c = π

Tactic:
replace hp : ∠ b p c = π := angle_eq_pi_iff_sbtw.mpr ⟨hp, pb, pc⟩
-- 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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
rwa rwa₁ rwa₂ rwa₃ : ∀ (hp : ∠ c p b = π), ∠ c p b = π
⊢ ∠ c p b = π

Tactic:
rwa [angle_comm] at hp

Premises used: EuclideanGeometry.angle_comm
-- 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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
⊢ ∠ c p b = π

Tactic:
have hp' : ∠ c p b = π := by rwa [angle_comm] at hp
-- 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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
⊢ ∠ b a p + ∠ a p b + ∠ c b a = π

Tactic:
rw [angle_comm p b a, angle_eq_angle_of_angle_eq_pi a hp, angle_comm a b c] at eb

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_angle_of_angle_eq_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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
eb₁ : ∠ b a p + ∠ a p b + ∠ c b a = π
⊢ ∠ a c p + ∠ c p a + ∠ p a c = π

Tactic:
rw [angle_comm p b a, angle_eq_angle_of_angle_eq_pi a hp, angle_comm a b c] at eb

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_angle_of_angle_eq_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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
eb₁ : ∠ b a p + ∠ a p b + ∠ c b a = π
ec₁ : ∠ a c p + ∠ c p a + ∠ p a c = π
⊢ ∠ b p c = π

Tactic:
rw [angle_comm p b a, angle_eq_angle_of_angle_eq_pi a hp, angle_comm a b c] at eb

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_angle_of_angle_eq_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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
eb₁ : ∠ b a p + ∠ a p b + ∠ c b a = π
ec₁ : ∠ a c p + ∠ c p a + ∠ p a c = π
hp₁ : ∠ b p c = π
⊢ ∠ c p b = π

Tactic:
rw [angle_comm p b a, angle_eq_angle_of_angle_eq_pi a hp, angle_comm a b c] at eb

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_angle_of_angle_eq_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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ c b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
⊢ ∠ a c b + ∠ a p c + ∠ p a c = π

Tactic:
rw [angle_eq_angle_of_angle_eq_pi a hp', angle_comm c p a] at ec

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_angle_of_angle_eq_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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ c b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
ec₁ : ∠ a c b + ∠ a p c + ∠ p a c = π
⊢ ∠ b p c = π

Tactic:
rw [angle_eq_angle_of_angle_eq_pi a hp', angle_comm c p a] at ec

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_angle_of_angle_eq_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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ c b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
ec₁ : ∠ a c b + ∠ a p c + ∠ p a c = π
hp₁ : ∠ b p c = π
⊢ ∠ c p b = π

Tactic:
rw [angle_eq_angle_of_angle_eq_pi a hp', angle_comm c p a] at ec

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_angle_of_angle_eq_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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ c b a = π
ec : ∠ a c b + ∠ a p c + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
⊢ ∠ a p b + ∠ a p c = π

Tactic:
have ep := angle_add_angle_eq_pi_of_angle_eq_pi a hp
-- 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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ c b a = π
ec : ∠ a c b + ∠ a p c + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
ep : ∠ a p b + ∠ a p c = π
linarith :
  ∠ b a p + ∠ p a c < ∠ b a c →
    ∠ b a p + ∠ p a c - ∠ b a c + (∠ b a c + ∠ a c b + ∠ c b a - π) + -(∠ b a p + ∠ a p b + ∠ c b a - π) +
          -(∠ a c b + ∠ a p c + ∠ p a c - π) +
        (∠ a p b + ∠ a p c - π) =
      0
linarith₁ :
  ∠ b a c < ∠ b a p + ∠ p a c →
    ∠ b a c - (∠ b a p + ∠ p a c) + -(∠ b a c + ∠ a c b + ∠ c b a - π) + (∠ b a p + ∠ a p b + ∠ c b a - π) +
          (∠ a c b + ∠ a p c + ∠ p a c - π) +
        -(∠ a p b + ∠ a p c - π) =
      0
⊢ ∠ b a p + ∠ p a c = ∠ b a c

Tactic:
linarith only [ea, eb, ec, ep]
-- 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
a b c p : P
h : ∠ b p c = π
rw :
  (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * -Real.cos (∠ a p c)) * dist c p +
      (dist a p * dist a p + dist c p * dist c p - 2 * dist a p * dist c p * Real.cos (∠ a p c)) * dist b p =
    (dist b p + dist c p) * (HPow.hPow (β := ℕ) (dist a p) 2 + dist b p * dist c p)
⊢ HPow.hPow (β := ℕ) (dist a b) 2 * dist c p + HPow.hPow (β := ℕ) (dist a c) 2 * dist b p =
    dist b c * (HPow.hPow (β := ℕ) (dist a p) 2 + dist b p * dist c p)

Tactic:
rw [pow_two, pow_two, law_cos a p b, law_cos a p c,
    eq_sub_of_add_eq (angle_add_angle_eq_pi_of_angle_eq_pi a h), Real.cos_pi_sub,
    dist_eq_add_dist_of_angle_eq_pi h]

Premises used: pow_two, eq_sub_of_add_eq, EuclideanGeometry.dist_eq_add_dist_of_angle_eq_pi, Real.cos_pi_sub, EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi, EuclideanGeometry.law_cos
-- 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
a b c p : P
h : ∠ b p c = π
⊢ (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * -Real.cos (∠ a p c)) * dist c p +
      (dist a p * dist a p + dist c p * dist c p - 2 * dist a p * dist c p * Real.cos (∠ a p c)) * dist b p =
    (dist b p + dist c p) * (HPow.hPow (β := ℕ) (dist a p) 2 + dist b p * dist c p)

Tactic:
ring
-- 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
a b c : P
pos :
  ∀ (hbc : b = c),
    HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
      2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
neg :
  ∀ (hbc : ¬b = c),
    HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
      2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
⊢ HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)

Tactic:
by_cases hbc : b = c
-- 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
a b c : P
hbc : b = c
⊢ HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)

Tactic:
simp [hbc, midpoint_self, dist_self, two_mul]

Premises used: two_mul, midpoint_self, dist_self
-- 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
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
⊢ dist b c ≠ 0

Tactic:
have : dist b c ≠ 0 := (dist_pos.mpr hbc).ne'
-- 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
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
⊢ HPow.hPow (β := ℕ) (dist a b) 2 * dist c m + HPow.hPow (β := ℕ) (dist a c) 2 * dist b m =
    dist b c * (HPow.hPow (β := ℕ) (dist a m) 2 + dist b m * dist c m)

Tactic:
have hm := dist_sq_mul_dist_add_dist_sq_mul_dist a b c m (angle_midpoint_eq_pi b c hbc)
-- 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
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  HPow.hPow (β := ℕ) (dist a b) 2 * dist c m + HPow.hPow (β := ℕ) (dist a c) 2 * dist b m =
    dist b c * (HPow.hPow (β := ℕ) (dist a m) 2 + dist b m * dist c m)
⊢ HPow.hPow (β := ℕ) (dist a b) 2 * (2⁻¹ * dist b c) + HPow.hPow (β := ℕ) (dist a c) 2 * (2⁻¹ * dist b c) =
    dist b c * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))

Tactic:
simp only [m, dist_left_midpoint, dist_right_midpoint, Real.norm_two] at hm

Premises used: dist_left_midpoint, Real.norm_two, dist_right_midpoint
-- 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
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  HPow.hPow (β := ℕ) (dist a b) 2 * (2⁻¹ * dist b c) + HPow.hPow (β := ℕ) (dist a c) 2 * (2⁻¹ * dist b c) =
    dist b c * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))
⊢ HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
    2 / dist b c *
      (HPow.hPow (β := ℕ) (dist a b) 2 * (2⁻¹ * dist b c) + HPow.hPow (β := ℕ) (dist a c) 2 * (2⁻¹ * dist b c))

Tactic:
field
-- 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
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  HPow.hPow (β := ℕ) (dist a b) 2 * (2⁻¹ * dist b c) + HPow.hPow (β := ℕ) (dist a c) 2 * (2⁻¹ * dist b c) =
    dist b c * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))
rw :
  2 / dist b c * (dist b c * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))) =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
⊢ 2 / dist b c *
      (HPow.hPow (β := ℕ) (dist a b) 2 * (2⁻¹ * dist b c) + HPow.hPow (β := ℕ) (dist a c) 2 * (2⁻¹ * dist b c)) =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)

Tactic:
rw [hm]
-- 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
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  HPow.hPow (β := ℕ) (dist a b) 2 * (2⁻¹ * dist b c) + HPow.hPow (β := ℕ) (dist a c) 2 * (2⁻¹ * dist b c) =
    dist b c * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))
⊢ 2 / dist b c * (dist b c * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))) =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)

Tactic:
field
-- 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
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : Dist.dist b c ≠ 0
hm :
  HPow.hPow (β := ℕ) (Dist.dist a b) 2 * (2⁻¹ * Dist.dist b c) +
      HPow.hPow (β := ℕ) (Dist.dist a c) 2 * (2⁻¹ * Dist.dist b c) =
    Dist.dist b c * (HPow.hPow (β := ℕ) (Dist.dist a (midpoint ℝ b c)) 2 + 2⁻¹ * Dist.dist b c * (2⁻¹ * Dist.dist b c))
dist :
  HPow.hPow (β := ℕ) (Dist.dist a b) 2 + HPow.hPow (β := ℕ) (Dist.dist a c) 2 =
    2 / Dist.dist b c *
      (HPow.hPow (β := ℕ) (Dist.dist a b) 2 * (2⁻¹ * Dist.dist b c) +
        HPow.hPow (β := ℕ) (Dist.dist a c) 2 * (2⁻¹ * Dist.dist b c))
dist₁ :
  2 / Dist.dist b c *
      (HPow.hPow (β := ℕ) (Dist.dist a b) 2 * (2⁻¹ * Dist.dist b c) +
        HPow.hPow (β := ℕ) (Dist.dist a c) 2 * (2⁻¹ * Dist.dist b c)) =
    2 * (HPow.hPow (β := ℕ) (Dist.dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (Dist.dist b c / 2) 2)
⊢ HPow.hPow (β := ℕ) (Dist.dist a b) 2 + HPow.hPow (β := ℕ) (Dist.dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (Dist.dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (Dist.dist b c / 2) 2)

Tactic:
calc
      dist a b ^ 2 + dist a c ^ 2 = 2 / dist b c * (dist a b ^ 2 *
        ((2 : ℝ)⁻¹ * dist b c) + dist a c ^ 2 * (2⁻¹ * dist b c)) := by
        field
      _ = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2) := by
        rw [hm]
        field

Premises used: Real, HMul.hMul, HDiv.hDiv, Inv.inv, HPow.hPow, HAdd.hAdd, Dist.dist, midpoint, OfNat.ofNat
-- 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
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c')

Tactic:
simp [pow_two, law_cos a' b' c']

Premises used: pow_two, EuclideanGeometry.law_cos
-- 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
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
rw :
  HPow.hPow (β := ℕ) (r * dist a b) 2 + HPow.hPow (β := ℕ) (r * dist c b) 2 -
      2 * (r * dist a b) * (r * dist c b) * Real.cos (∠ a b c) =
    HPow.hPow (β := ℕ) r 2 *
      (HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist c b) 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c))
⊢ HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c') =
    HPow.hPow (β := ℕ) r 2 *
      (HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist c b) 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c))

Tactic:
rw [h, hab, hcb]