awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
rw : ⟪z, r • y⟫ = 0
rw₁ : r * ⟪z, y⟫ = 0
rw₂ : r * 0 = 0
⊢ ⟪z, x⟫ = 0
have rw₃ : Eq (α := ℝ) 0 0
Tactic: rw [hr, inner_smul_right, hzy, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
have hzx : ⟪z, x⟫ = 0
Tactic: have hzx : ⟪z, x⟫ = 0 := by rw [hr, inner_smul_right, hzy, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
have by : ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖
Tactic: calc
    ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖ := by simp [sub_smul, add_smul, hr]
    _ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) := by simp_rw [norm_smul]
    _ = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 := by ring
    _ = |(r - 1) * (r + 1) * ‖y‖ ^ 2| := by simp [abs_mul]
    _ = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| := by ring_nf
    _ = |‖x‖ ^ 2 - ‖y‖ ^ 2| := by simp [hr, norm_smul, mul_pow, sq_abs]
    _ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| := by
      simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
by : ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
have by₁ : ‖(r - 1) • y‖ * ‖(r + 1) • y‖ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖)
Tactic: calc
    ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖ := by simp [sub_smul, add_smul, hr]
    _ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) := by simp_rw [norm_smul]
    _ = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 := by ring
    _ = |(r - 1) * (r + 1) * ‖y‖ ^ 2| := by simp [abs_mul]
    _ = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| := by ring_nf
    _ = |‖x‖ ^ 2 - ‖y‖ ^ 2| := by simp [hr, norm_smul, mul_pow, sq_abs]
    _ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| := by
      simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
by : ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖
by₁ : ‖(r - 1) • y‖ * ‖(r + 1) • y‖ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖)
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
have by₂ : ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) = ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: calc
    ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖ := by simp [sub_smul, add_smul, hr]
    _ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) := by simp_rw [norm_smul]
    _ = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 := by ring
    _ = |(r - 1) * (r + 1) * ‖y‖ ^ 2| := by simp [abs_mul]
    _ = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| := by ring_nf
    _ = |‖x‖ ^ 2 - ‖y‖ ^ 2| := by simp [hr, norm_smul, mul_pow, sq_abs]
    _ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| := by
      simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
by : ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖
by₁ : ‖(r - 1) • y‖ * ‖(r + 1) • y‖ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖)
by₂ : ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) = ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
have by₃ : ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2 = |(r - 1) * (r + 1) * HPow.hPow (β := ℕ) ‖y‖ 2|
Tactic: calc
    ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖ := by simp [sub_smul, add_smul, hr]
    _ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) := by simp_rw [norm_smul]
    _ = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 := by ring
    _ = |(r - 1) * (r + 1) * ‖y‖ ^ 2| := by simp [abs_mul]
    _ = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| := by ring_nf
    _ = |‖x‖ ^ 2 - ‖y‖ ^ 2| := by simp [hr, norm_smul, mul_pow, sq_abs]
    _ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| := by
      simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
by : ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖
by₁ : ‖(r - 1) • y‖ * ‖(r + 1) • y‖ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖)
by₂ : ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) = ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2
by₃ : ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2 = |(r - 1) * (r + 1) * HPow.hPow (β := ℕ) ‖y‖ 2|
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
have by₄ : |(r - 1) * (r + 1) * HPow.hPow (β := ℕ) ‖y‖ 2| =
  |HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2|
Tactic: calc
    ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖ := by simp [sub_smul, add_smul, hr]
    _ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) := by simp_rw [norm_smul]
    _ = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 := by ring
    _ = |(r - 1) * (r + 1) * ‖y‖ ^ 2| := by simp [abs_mul]
    _ = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| := by ring_nf
    _ = |‖x‖ ^ 2 - ‖y‖ ^ 2| := by simp [hr, norm_smul, mul_pow, sq_abs]
    _ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| := by
      simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
by : ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖
by₁ : ‖(r - 1) • y‖ * ‖(r + 1) • y‖ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖)
by₂ : ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) = ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2
by₃ : ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2 = |(r - 1) * (r + 1) * HPow.hPow (β := ℕ) ‖y‖ 2|
by₄ :
  |(r - 1) * (r + 1) * HPow.hPow (β := ℕ) ‖y‖ 2| =
    |HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2|
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
have by₅ : |HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2| =
  |HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2|
Tactic: calc
    ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖ := by simp [sub_smul, add_smul, hr]
    _ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) := by simp_rw [norm_smul]
    _ = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 := by ring
    _ = |(r - 1) * (r + 1) * ‖y‖ ^ 2| := by simp [abs_mul]
    _ = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| := by ring_nf
    _ = |‖x‖ ^ 2 - ‖y‖ ^ 2| := by simp [hr, norm_smul, mul_pow, sq_abs]
    _ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| := by
      simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
by : ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖
by₁ : ‖(r - 1) • y‖ * ‖(r + 1) • y‖ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖)
by₂ : ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) = ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2
by₃ : ‖r - 1‖ * ‖r + 1‖ * HPow.hPow (β := ℕ) ‖y‖ 2 = |(r - 1) * (r + 1) * HPow.hPow (β := ℕ) ‖y‖ 2|
by₄ :
  |(r - 1) * (r + 1) * HPow.hPow (β := ℕ) ‖y‖ 2| =
    |HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2|
by₅ :
  |HPow.hPow (β := ℕ) r 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2| =
    |HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2|
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
have by₆ : |HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2| = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
Tactic: calc
    ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖ := by simp [sub_smul, add_smul, hr]
    _ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) := by simp_rw [norm_smul]
    _ = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 := by ring
    _ = |(r - 1) * (r + 1) * ‖y‖ ^ 2| := by simp [abs_mul]
    _ = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| := by ring_nf
    _ = |‖x‖ ^ 2 - ‖y‖ ^ 2| := by simp [hr, norm_smul, mul_pow, sq_abs]
    _ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| := by
      simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
⊢ dist a p * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
have h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
Tactic: have h1 := vsub_sub_vsub_cancel_left a p m
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
⊢ dist a p * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
have h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
Tactic: have h1' := vsub_sub_vsub_cancel_left p a m
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
⊢ dist a p * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
have h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
Tactic: have h2 := vsub_sub_vsub_cancel_left p q m
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
⊢ dist a p * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
have h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
Tactic: have h3 := vsub_sub_vsub_cancel_left a q m
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
r : P
⊢ b -ᵥ r = m -ᵥ r + (m -ᵥ a)
have rw : b -ᵥ r = m -ᵥ r + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)
Tactic: rw [midpoint_vsub_left, ← right_vsub_midpoint, add_comm, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
r : P
rw : b -ᵥ r = m -ᵥ r + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)
⊢ b -ᵥ r = m -ᵥ r + (m -ᵥ a)
have rw₁ : b -ᵥ r = m -ᵥ r + (b -ᵥ midpoint ℝ a b)
Tactic: rw [midpoint_vsub_left, ← right_vsub_midpoint, add_comm, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
r : P
rw : b -ᵥ r = m -ᵥ r + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)
rw₁ : b -ᵥ r = m -ᵥ r + (b -ᵥ midpoint ℝ a b)
⊢ b -ᵥ r = m -ᵥ r + (m -ᵥ a)
have rw₂ : b -ᵥ r = b -ᵥ midpoint ℝ a b + (m -ᵥ r)
Tactic: rw [midpoint_vsub_left, ← right_vsub_midpoint, add_comm, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
r : P
rw : b -ᵥ r = m -ᵥ r + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)
rw₁ : b -ᵥ r = m -ᵥ r + (b -ᵥ midpoint ℝ a b)
rw₂ : b -ᵥ r = b -ᵥ midpoint ℝ a b + (m -ᵥ r)
⊢ b -ᵥ r = m -ᵥ r + (m -ᵥ a)
have rw₃ : b -ᵥ r = b -ᵥ r
Tactic: rw [midpoint_vsub_left, ← right_vsub_midpoint, add_comm, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
⊢ dist a p * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
have h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
Tactic: have h : ∀ r, b -ᵥ r = m -ᵥ r + (m -ᵥ a) := fun r => by
    rw [midpoint_vsub_left, ← right_vsub_midpoint, add_comm, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ dist a p * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
have rw : ‖a -ᵥ p‖ * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
Tactic: rw [dist_eq_norm_vsub V]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖a -ᵥ p‖ * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
have rw : ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
Tactic: rw [dist_eq_norm_vsub V]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
have rw : ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) ‖b -ᵥ q‖ 2 - HPow.hPow (β := ℕ) (dist p q) 2|
Tactic: rw [dist_eq_norm_vsub V]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) ‖b -ᵥ q‖ 2 - HPow.hPow (β := ℕ) (dist p q) 2|
have rw : ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) ‖b -ᵥ q‖ 2 - HPow.hPow (β := ℕ) ‖p -ᵥ q‖ 2|
Tactic: rw [dist_eq_norm_vsub V]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ dist a p * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
have iterate : ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) ‖b -ᵥ q‖ 2 - HPow.hPow (β := ℕ) ‖p -ᵥ q‖ 2|
Tactic: iterate 4 rw [dist_eq_norm_vsub V]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) ‖b -ᵥ q‖ 2 - HPow.hPow (β := ℕ) ‖p -ᵥ q‖ 2|
have rw : ‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ =
  |HPow.hPow (β := ℕ) ‖m -ᵥ q + (m -ᵥ a)‖ 2 - HPow.hPow (β := ℕ) ‖m -ᵥ q - (m -ᵥ p)‖ 2|
Tactic: rw [← h1, ← h2, h, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ =
    |HPow.hPow (β := ℕ) ‖m -ᵥ q + (m -ᵥ a)‖ 2 - HPow.hPow (β := ℕ) ‖m -ᵥ q - (m -ᵥ p)‖ 2|
have rw : let m := midpoint ℝ a b;
∀ (hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖) (h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p) (h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a)
  (h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q) (h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q) (h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)),
  ‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ =
    |HPow.hPow (β := ℕ) ‖m -ᵥ q + (m -ᵥ a)‖ 2 - HPow.hPow (β := ℕ) ‖m -ᵥ q - (m -ᵥ p)‖ 2|
Tactic: rw [dist_eq_norm_vsub V a q, dist_eq_norm_vsub V b q, ← h3, h] at hq
Cleared hypotheses: hq, m, h1, h1', h2, h3, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
m : P := midpoint ℝ a b
hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ =
    |HPow.hPow (β := ℕ) ‖m -ᵥ q + (m -ᵥ a)‖ 2 - HPow.hPow (β := ℕ) ‖m -ᵥ q - (m -ᵥ p)‖ 2|
have refine : ∃ (k : ℝ), m -ᵥ p = k • (m -ᵥ a)
Tactic: refine mul_norm_eq_abs_sub_sq_norm ?_ hq
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
m : P := midpoint ℝ a b
hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ∃ (k : ℝ), m -ᵥ p = k • (m -ᵥ a)
have rw : ∀ (hp : ∃ (r : ℝ), r • (b -ᵥ a) = p -ᵥ a),
  let m := midpoint ℝ a b;
  ∀ (hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖) (h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p)
    (h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a) (h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q) (h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q)
    (h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)), ∃ (k : ℝ), m -ᵥ p = k • (m -ᵥ a)
Tactic: rw [← vsub_vadd p a, vadd_left_mem_affineSpan_pair] at hp
Cleared hypotheses: hp, m, hq, h1, h1', h2, h3, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
hp : ∃ (r : ℝ), r • (b -ᵥ a) = p -ᵥ a
m : P := midpoint ℝ a b
hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ∃ (k : ℝ), m -ᵥ p = k • (m -ᵥ a)
have rcases : ∀ (r : ℝ) (hr : r • (b -ᵥ a) = p -ᵥ a), ∃ (k : ℝ), m -ᵥ p = k • (m -ᵥ a)
Tactic: rcases hp with ⟨r, hr⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b p q : P
m : P := midpoint ℝ a b
hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
r : ℝ
hr : r • (b -ᵥ a) = p -ᵥ a
⊢ ∃ (k : ℝ), m -ᵥ p = k • (m -ᵥ a)
have hr₁ : m -ᵥ p = m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a))
Tactic: rw [h, ← h1', eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at hr
Cleared hypotheses: hr