awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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‖
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0
have simp : ¬Real.sin (angle x z) = 0 ∧ ¬y = 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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‖
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have hnonzero : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0
Tactic: have hnonzero : (⟨Real.sin (angle x z) / ‖y‖, hnneg₃⟩ : ℝ≥0) ≠ 0 := by
      simp; grind
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have h₁ : angle (NormedSpace.normalize x) (NormedSpace.normalize z) ≠ π →
  angle (NormedSpace.normalize x) (NormedSpace.normalize z) =
      angle (NormedSpace.normalize x) (NormedSpace.normalize y) +
        angle (NormedSpace.normalize y) (NormedSpace.normalize z) →
    Real.sin (angle (NormedSpace.normalize x) (NormedSpace.normalize z)) • NormedSpace.normalize y =
      Real.sin (angle (NormedSpace.normalize y) (NormedSpace.normalize z)) • NormedSpace.normalize x +
        Real.sin (angle (NormedSpace.normalize x) (NormedSpace.normalize y)) • NormedSpace.normalize z
Tactic: have h₁ := angle_expression_of_angle_eq_angle_sum (norm_normalize_eq_one_iff.mpr hx)
        (norm_normalize_eq_one_iff.mpr hy) (norm_normalize_eq_one_iff.mpr hz)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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 (NormedSpace.normalize x) (NormedSpace.normalize z) ≠ π →
    angle (NormedSpace.normalize x) (NormedSpace.normalize z) =
        angle (NormedSpace.normalize x) (NormedSpace.normalize y) +
          angle (NormedSpace.normalize y) (NormedSpace.normalize z) →
      Real.sin (angle (NormedSpace.normalize x) (NormedSpace.normalize z)) • NormedSpace.normalize y =
        Real.sin (angle (NormedSpace.normalize y) (NormedSpace.normalize z)) • NormedSpace.normalize x +
          Real.sin (angle (NormedSpace.normalize x) (NormedSpace.normalize y)) • NormedSpace.normalize z
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have 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
Tactic: simp only [angle_normalize_right, angle_normalize_left] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have 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
Tactic: have h₂ := h₁ hxz₁ h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ 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
have simp : ∀ (h₂ : (Real.sin (angle x z) * ‖y‖⁻¹) • y = (Real.sin (angle y z) * ‖x‖⁻¹) • x + (Real.sin (angle x y) * ‖z‖⁻¹) • z),
  (Real.sin (angle x z) / ‖y‖) • y = (Real.sin (angle y z) / ‖x‖) • x + (Real.sin (angle x y) / ‖z‖) • z
Tactic: simp only [NormedSpace.normalize, ← smul_assoc, smul_eq_mul, Nonneg.mk_smul] at h₂ ⊢
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have 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
Tactic: have h₃ : (⟨_, hnneg₃⟩ : ℝ≥0) • y = (⟨_, hnneg₁⟩ : ℝ≥0) • x + (⟨_, hnneg₂⟩ : ℝ≥0) • z := by
      simp only [NormedSpace.normalize, ← smul_assoc, smul_eq_mul, Nonneg.mk_smul] at h₂ ⊢
      exact h₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ angle x z = angle x y + angle y z
have mpr : ∀ (h : angle x z = π), angle x z = angle x y + angle y z
Tactic: obtain h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ angle x z = angle x y + angle y z
have mpr₁ : ∀ (h : Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y), angle x z = angle x y + angle y z
Tactic: obtain h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι₁ : 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
⊢ 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
have rw : HDiv.hDiv (α := ℝ)
    (-∑ i₁ ∈ s₁,
        ∑ i₂ ∈ s₂,
          w₁ i₁ * w₂ i₂ *
            (‖p₁ i₁ -ᵥ Classical.choice sorry - (p₂ i₂ -ᵥ Classical.choice sorry)‖ *
              ‖p₁ i₁ -ᵥ Classical.choice sorry - (p₂ i₂ -ᵥ Classical.choice sorry)‖))
    2 =
  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₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι₁ : 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
⊢ 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
have 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
Tactic: simp_rw [vsub_sub_vsub_cancel_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι₁ : 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
⊢ 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
have e_a : ∀ (i₁ : ι₁) (i₂ : ι₂), ‖p₁ i₁ -ᵥ p₂ i₂‖ = dist (p₁ i₁) (p₂ i₂)
Tactic: rcongr (i₁ i₂)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι₁ : 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₂ : ι₂
⊢ ‖p₁ i₁ -ᵥ p₂ i₂‖ = dist (p₁ i₁) (p₂ i₂)
have e_a : ‖p₁ i₁ -ᵥ p₂ i₂‖ = ‖p₁ i₁ -ᵥ p₂ i₂‖
Tactic: rw [dist_eq_norm_vsub V (p₁ i₁) (p₂ i₂)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : Eq (α := ℝ) (∑ i ∈ s, w₁ i) 1
h₂ : Eq (α := ℝ) (∑ i ∈ s, w₂ i) 1
⊢ Prop
have have : (a₁ : P) → Prop
Tactic: have a₁ := s.affineCombination ℝ p w₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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
⊢ Prop
have have : (a₂ : P) → Prop
Tactic: have a₂ := s.affineCombination ℝ p w₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : Eq (α := ℝ) (∑ i ∈ s, w₁ i) 1
h₂ : Eq (α := ℝ) (∑ i ∈ s, w₂ i) 1
⊢ 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
have 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
Tactic: rw [dist_eq_norm_vsub V (s.affineCombination ℝ p w₁) (s.affineCombination ℝ p w₂), ←
    @inner_self_eq_norm_mul_norm ℝ, Finset.affineCombination_vsub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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
have simp_rw : Eq (α := ℝ) (∑ x ∈ s, (w₁ x - w₂ x)) 0
Tactic: simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, h₁, h₂, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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
⊢ Eq (α := ℝ) (∑ i ∈ s, (w₁ - w₂) i) 0
have simp_rw₁ : HSub.hSub (α := ℝ) (∑ x ∈ s, w₁ x) (∑ x ∈ s, w₂ x) = 0
Tactic: simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, h₁, h₂, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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
⊢ Eq (α := ℝ) (∑ i ∈ s, (w₁ - w₂) i) 0
have simp_rw₂ : HSub.hSub (α := ℝ) 1 (∑ x ∈ s, w₂ x) = 0
Tactic: simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, h₁, h₂, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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
⊢ Eq (α := ℝ) (∑ i ∈ s, (w₁ - w₂) i) 0
have simp_rw₃ : HSub.hSub (α := ℝ) 1 1 = 0
Tactic: simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, h₁, h₂, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : Type u_3
s : Finset ι
w₁ w₂ : ι → ℝ
p : ι → P
h₁ : Eq (α := ℝ) (∑ i ∈ s, w₁ i) 1
h₂ : Eq (α := ℝ) (∑ i ∈ s, w₂ i) 1
⊢ (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
have h : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
r : ℝ
v : V
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₂⟫
have 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₂⟫
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
| dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂
have rw : ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + 0 = 0
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫
have conv_lhs : ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + 0 = 0 ↔ 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + 0 = 0 ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫
have hvi : ⟪v, v⟫ ≠ 0
Tactic: have hvi : ⟪v, v⟫ ≠ 0 := by simpa using hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : ⟪v, v⟫ ≠ 0
⊢ ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + 0 = 0 ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫
have hd : 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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₂⟫)
⊢ ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + 0 = 0 ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫
have hc : Ne (α := ℝ) 2 0
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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₂
⊢ p = p₁ ∨ p = p₂
have ho : ⟪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)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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
⊢ p = p₁ ∨ p = p₂
have hop : ⟪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)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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
have refine_1 : ∀ (i : Fin 2), b i ≠ 0
Tactic: refine linearIndependent_of_ne_zero_of_inner_eq_zero ?_ ?_