awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
hnonzero : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0
h₁ :
  angle x z ≠ π →
    angle x z = angle x y + angle y z →
      Real.sin (angle x z) • NormedSpace.normalize y =
        Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
h₂ :
  Real.sin (angle x z) • NormedSpace.normalize y =
    Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
h₃ :
  Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ • y =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle y z) / ‖x‖) hnneg₁ • x +
      Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x y) / ‖z‖) hnneg₂ • z
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y

Tactic:
exact mem_span_of_linear_combination hnonzero h₃

Premises used: _private.0.InnerProductGeometry.mem_span_of_linear_combination
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
mpr : ∀ (h : angle x z = π), angle x z = angle x y + angle y z
mpr₁ : ∀ (h : Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y), angle x z = angle x y + angle y z
⊢ angle x z = angle x y + angle y z

Tactic:
obtain h | h := h
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = π
⊢ angle x z = angle x y + angle y z

Tactic:
grind [angle_add_angle_eq_pi_of_angle_eq_pi, angle_comm]

Premises used: InnerProductGeometry.angle_add_angle_eq_pi_of_angle_eq_pi, InnerProductGeometry.angle_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
⊢ angle x z = angle x y + angle y z

Tactic:
angle_eq_angle_add_add_angle_add_of_mem_span hy h

Premises used: InnerProductGeometry.angle_eq_angle_add_add_angle_add_of_mem_span
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
⊢ angle x z = angle x y + angle y z

Tactic:
exact angle_eq_angle_add_add_angle_add_of_mem_span hy h

Premises used: InnerProductGeometry.angle_eq_angle_add_add_angle_add_of_mem_span
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_2
P : Type u_3
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₃

Tactic:
InnerProductGeometry.angle_le_angle_add_angle _ _ _

Premises used: InnerProductGeometry.angle_le_angle_add_angle, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : Eq (α := ℝ) (∑ i ∈ s₁, w₁ i) 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : Eq (α := ℝ) (∑ i ∈ s₂, w₂ i) 0
rw :
  HDiv.hDiv (α := ℝ)
      (-∑ i₁ ∈ s₁,
          ∑ i₂ ∈ s₂,
            w₁ i₁ * w₂ i₂ *
              (‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖ *
                ‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖))
      2 =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) 2
⊢ inner.{0, u_1} ℝ (E := V) ((s₁.weightedVSub p₁ : (a : ι₁ → ℝ) → V) w₁ : V)
      ((s₂.weightedVSub p₂ : (a : ι₂ → ℝ) → V) w₂ : V) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) 2

Tactic:
rw [Finset.weightedVSub_apply, Finset.weightedVSub_apply,
    inner_sum_smul_sum_smul_of_sum_eq_zero _ h₁ _ h₂]

Premises used: inner_sum_smul_sum_smul_of_sum_eq_zero, Finset.weightedVSub_apply
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : Eq (α := ℝ) (∑ i ∈ s₁, w₁ i) 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : Eq (α := ℝ) (∑ i ∈ s₂, w₂ i) 0
simp_rw :
  HDiv.hDiv (α := ℝ) (-∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * w₂ x_1 * (‖p₁ x -ᵥ p₂ x_1‖ * ‖p₁ x -ᵥ p₂ x_1‖)) 2 =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) 2
⊢ HDiv.hDiv (α := ℝ)
      (-∑ i₁ ∈ s₁,
          ∑ i₂ ∈ s₂,
            w₁ i₁ * w₂ i₂ *
              (‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖ *
                ‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖))
      2 =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) 2

Tactic:
simp_rw [vsub_sub_vsub_cancel_right]

Premises used: vsub_sub_vsub_cancel_right
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : Eq (α := ℝ) (∑ i ∈ s₁, w₁ i) 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : Eq (α := ℝ) (∑ i ∈ s₂, w₂ i) 0
e_a e_a₁ : ∀ (i₁ : ι₁) (i₂ : ι₂), ‖p₁ i₁ -ᵥ p₂ i₂‖ = dist (p₁ i₁) (p₂ i₂)
⊢ HDiv.hDiv (α := ℝ) (-∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * w₂ x_1 * (‖p₁ x -ᵥ p₂ x_1‖ * ‖p₁ x -ᵥ p₂ x_1‖)) 2 =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) 2

Tactic:
rcongr (i₁ i₂)
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : Eq (α := ℝ) (∑ i ∈ s₁, w₁ i) 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : Eq (α := ℝ) (∑ i ∈ s₂, w₂ i) 0
i₁ : ι₁
i₂ : ι₂
e_a e_a₁ : ‖p₁ i₁ -ᵥ p₂ i₂‖ = ‖p₁ i₁ -ᵥ p₂ i₂‖
⊢ ‖p₁ i₁ -ᵥ p₂ i₂‖ = dist (p₁ i₁) (p₂ i₂)

Tactic:
rw [dist_eq_norm_vsub V (p₁ i₁) (p₂ i₂)]

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : Eq (α := ℝ) (∑ i ∈ s, w₁ i) 1
h₂ : Eq (α := ℝ) (∑ i ∈ s, w₂ i) 1
have : (a₁ : P) → Prop
⊢ Prop

Tactic:
have a₁ := s.affineCombination ℝ p w₁
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : Eq (α := ℝ) (∑ i ∈ s, w₁ i) 1
h₂ : Eq (α := ℝ) (∑ i ∈ s, w₂ i) 1
a₁ : P
have : (a₂ : P) → Prop
⊢ Prop

Tactic:
have a₂ := s.affineCombination ℝ p w₂
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : Eq (α := ℝ) (∑ i ∈ s, w₁ i) 1
h₂ : Eq (α := ℝ) (∑ i ∈ s, w₂ i) 1
a₁ a₂ : P
⊢ Prop

Tactic:
exact dist a₁ a₂ * dist a₁ a₂ = (-∑ i₁ ∈ s, ∑ i₂ ∈ s,
        (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2

Premises used: HMul.hMul, HSub.hSub, Dist.dist, Finset.sum, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : Eq (α := ℝ) (∑ i ∈ s, w₁ i) 1
h₂ : Eq (α := ℝ) (∑ i ∈ s, w₂ i) 1
rw :
  (RCLike.re : (a : ℝ) → ℝ)
      (inner.{0, u_1} ℝ (E := V) ((s.weightedVSub p : (a : ι → ℝ) → V) (w₁ - w₂) : V)
        ((s.weightedVSub p : (a : ι → ℝ) → V) (w₁ - w₂) : V)) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) 2
⊢ dist.{u_2} (α := P) ((Finset.affineCombination ℝ s p : (a : ι → ℝ) → P) w₁ : P)
        ((Finset.affineCombination ℝ s p : (a : ι → ℝ) → P) w₂ : P) *
      dist.{u_2} (α := P) ((Finset.affineCombination ℝ s p : (a : ι → ℝ) → P) w₁ : P)
        ((Finset.affineCombination ℝ s p : (a : ι → ℝ) → P) w₂ : P) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) 2

Tactic:
rw [dist_eq_norm_vsub V (s.affineCombination ℝ p w₁) (s.affineCombination ℝ p w₂), ←
    @inner_self_eq_norm_mul_norm ℝ, Finset.affineCombination_vsub]

Premises used: Finset.affineCombination_vsub, Real, inner_self_eq_norm_mul_norm, Finset.affineCombination, dist_eq_norm_vsub, DFunLike.coe
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : Eq (α := ℝ) (∑ i ∈ s, w₁ i) 1
h₂ : Eq (α := ℝ) (∑ i ∈ s, w₂ i) 1
simp_rw : Eq (α := ℝ) (∑ x ∈ s, (w₁ x - w₂ x)) 0
simp_rw₁ : HSub.hSub (α := ℝ) (∑ x ∈ s, w₁ x) (∑ x ∈ s, w₂ x) = 0
simp_rw₂ : HSub.hSub (α := ℝ) 1 (∑ x ∈ s, w₂ x) = 0
simp_rw₃ : HSub.hSub (α := ℝ) 1 1 = 0
⊢ Eq (α := ℝ) (∑ i ∈ s, (w₁ - w₂) i) 0

Tactic:
simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, h₁, h₂, sub_self]

Premises used: sub_self, Finset.sum_sub_distrib, Pi.sub_apply
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : Eq (α := ℝ) (∑ i ∈ s, w₁ i) 1
h₂ : Eq (α := ℝ) (∑ i ∈ s, w₂ i) 1
⊢ Eq (α := ℝ) (∑ i ∈ s, (w₁ - w₂) i) 0

Tactic:
have h : (∑ i ∈ s, (w₁ - w₂) i) = 0 := by
    simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, h₁, h₂, sub_self]
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : Eq (α := ℝ) (∑ i ∈ s, w₁ i) 1
h₂ : Eq (α := ℝ) (∑ i ∈ s, w₂ i) 1
h : Eq (α := ℝ) (∑ i ∈ s, (w₁ - w₂) i) 0
⊢ (RCLike.re : (a : ℝ) → ℝ)
      (inner.{0, u_1} ℝ (E := V) ((s.weightedVSub p : (a : ι → ℝ) → V) (w₁ - w₂) : V)
        ((s.weightedVSub p : (a : ι → ℝ) → V) (w₁ - w₂) : V)) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) 2

Tactic:
inner_weightedVSub p h p h

Premises used: EuclideanGeometry.inner_weightedVSub
-- Module: Mathlib.Geometry.Euclidean.Basic
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
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : Eq (α := ℝ) (∑ i ∈ s, w₁ i) 1
h₂ : Eq (α := ℝ) (∑ i ∈ s, w₂ i) 1
h : Eq (α := ℝ) (∑ i ∈ s, (w₁ - w₂) i) 0
⊢ (RCLike.re : (a : ℝ) → ℝ)
      (inner.{0, u_1} ℝ (E := V) ((s.weightedVSub p : (a : ι → ℝ) → V) (w₁ - w₂) : V)
        ((s.weightedVSub p : (a : ι → ℝ) → V) (w₁ - w₂) : V)) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) 2

Tactic:
exact inner_weightedVSub p h p h

Premises used: EuclideanGeometry.inner_weightedVSub
-- Module: Mathlib.Geometry.Euclidean.Basic
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
r : ℝ
v : V
p₁ p₂ : P
rw :
  r * (r * ⟪v, v⟫) + 2 * (r * ⟪v, p₁ -ᵥ p₂⟫) + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ =
    ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫
⊢ dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ = ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫

Tactic:
rw [dist_eq_norm_vsub V _ p₂, ← real_inner_self_eq_norm_mul_norm, vadd_vsub_assoc,
    real_inner_add_add_self, real_inner_smul_left, real_inner_smul_left, real_inner_smul_right]

Premises used: vadd_vsub_assoc, real_inner_smul_right, real_inner_self_eq_norm_mul_norm, dist_eq_norm_vsub, real_inner_smul_left, real_inner_add_add_self
-- Module: Mathlib.Geometry.Euclidean.Basic
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
r : ℝ
v : V
p₁ p₂ : P
⊢ r * (r * ⟪v, v⟫) + 2 * (r * ⟪v, p₁ -ᵥ p₂⟫) + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ =
    ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Basic
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
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
rw : ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + 0 = 0
| dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂

Tactic:
rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, mul_assoc,
      ← sub_eq_zero, add_sub_assoc, dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm,
      sub_self]

Premises used: EuclideanGeometry.dist_smul_vadd_sq, add_sub_assoc, mul_self_inj_of_nonneg, sub_self, sub_eq_zero, mul_assoc, dist_nonneg, real_inner_self_eq_norm_mul_norm, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Basic
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
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
conv_lhs : ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + 0 = 0 ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫
⊢ dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫

Tactic:
conv_lhs =>
    rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, mul_assoc,
      ← sub_eq_zero, add_sub_assoc, dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm,
      sub_self]

Premises used: EuclideanGeometry.dist_smul_vadd_sq, add_sub_assoc, mul_self_inj_of_nonneg, sub_self, sub_eq_zero, mul_assoc, dist_nonneg, real_inner_self_eq_norm_mul_norm, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Basic
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
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ ⟪v, v⟫ ≠ 0

Tactic:
simpa using hv
-- Module: Mathlib.Geometry.Euclidean.Basic
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
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ ⟪v, v⟫ ≠ 0

Tactic:
have hvi : ⟪v, v⟫ ≠ 0 := by simpa using hv
-- Module: Mathlib.Geometry.Euclidean.Basic
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
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : ⟪v, v⟫ ≠ 0
⊢ HPow.hPow (β := ℕ) (2 * ⟪v, p₁ -ᵥ p₂⟫) 2 - 4 * ⟪v, v⟫ * 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫)

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Basic
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
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : ⟪v, v⟫ ≠ 0
⊢ discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫)

Tactic:
have hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫) := by
    rw [discrim]
    ring
-- Module: Mathlib.Geometry.Euclidean.Basic
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
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : ⟪v, v⟫ ≠ 0
hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫)
hc : Ne (α := ℝ) 2 0
⊢ ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + 0 = 0 ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫

Tactic:
rw [quadratic_eq_zero_iff hvi hd, neg_add_cancel, zero_div, neg_mul_eq_neg_mul, ←
    mul_sub_right_distrib, sub_eq_add_neg, ← mul_two, mul_assoc, mul_div_assoc, mul_div_mul_left,
    mul_div_assoc]

Premises used: mul_assoc, mul_div_assoc, sub_eq_add_neg, zero_div, mul_sub_right_distrib, quadratic_eq_zero_iff, neg_add_cancel, mul_div_mul_left, neg_mul_eq_neg_mul, mul_two
-- Module: Mathlib.Geometry.Euclidean.Basic
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
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : ⟪v, v⟫ ≠ 0
hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫)
⊢ Ne (α := ℝ) 2 0

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Basic
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
s : AffineSubspace ℝ P
inst_4 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
⊢ ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0

Tactic:
have ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0 :=
    inner_vsub_vsub_of_dist_eq_of_dist_eq (hp₁c₁.trans hp₂c₁.symm) (hp₁c₂.trans hp₂c₂.symm)
-- Module: Mathlib.Geometry.Euclidean.Basic
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
s : AffineSubspace ℝ P
inst_4 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
⊢ ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0

Tactic:
have hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0 :=
    inner_vsub_vsub_of_dist_eq_of_dist_eq (hp₁c₁.trans hpc₁.symm) (hp₁c₂.trans hpc₂.symm)
-- Module: Mathlib.Geometry.Euclidean.Basic
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
s : AffineSubspace ℝ P
inst_4 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ LinearIndependent ℝ b

Tactic:
linearIndependent_of_ne_zero_of_inner_eq_zero ?_ ?_

Premises used: linearIndependent_of_ne_zero_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Basic
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
s : AffineSubspace ℝ P
inst_4 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
refine_1 : ∀ (i : Fin 2), b i ≠ 0
refine_2 : Pairwise fun (i j : Fin 2) ↦ ⟪b i, b j⟫ = 0
⊢ LinearIndependent ℝ b

Tactic:
refine linearIndependent_of_ne_zero_of_inner_eq_zero ?_ ?_

Premises used: linearIndependent_of_ne_zero_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Basic
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
s : AffineSubspace ℝ P
inst_4 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
i : Fin 2
refine_1 : b ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ≠ 0
refine_1₁ : b ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ≠ 0
⊢ b i ≠ 0

Tactic:
fin_cases i
-- Module: Mathlib.Geometry.Euclidean.Basic
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
s : AffineSubspace ℝ P
inst_4 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ b ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ≠ 0

Tactic:
simp [b, hc.symm, hp.symm]

Premises used: Ne.symm
-- Module: Mathlib.Geometry.Euclidean.Basic
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
s : AffineSubspace ℝ P
inst_4 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ b ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ≠ 0

Tactic:
simp [b, hc.symm, hp.symm]

Premises used: Ne.symm
-- Module: Mathlib.Geometry.Euclidean.Basic
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
s : AffineSubspace ℝ P
inst_4 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
i j : Fin 2
hij : i ≠ j
refine_2 : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j), ⟪b ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)), b j⟫ = 0
refine_2₁ : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j), ⟪b ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)), b j⟫ = 0
⊢ ⟪b i, b j⟫ = 0

Tactic:
fin_cases i