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
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hq : dist a s.center = dist b s.center
rw : dist a p * dist p b = |s.power p|
rw₁ : dist a p * dist b p = |s.power p|
⊢ dist p a * dist p b = |s.power p|
have rw₂ : |HPow.hPow (β := ℕ) (dist b s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = |s.power p|
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
    mem_sphere.mp hb, power, 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
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hq : dist a s.center = dist b s.center
rw : dist a p * dist p b = |s.power p|
rw₁ : dist a p * dist b p = |s.power p|
rw₂ : |HPow.hPow (β := ℕ) (dist b s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = |s.power p|
⊢ dist p a * dist p b = |s.power p|
have rw₃ : |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = |s.power p|
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
    mem_sphere.mp hb, power, 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
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hq : dist a s.center = dist b s.center
rw : dist a p * dist p b = |s.power p|
rw₁ : dist a p * dist b p = |s.power p|
rw₂ : |HPow.hPow (β := ℕ) (dist b s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = |s.power p|
rw₃ : |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = |s.power p|
⊢ dist p a * dist p b = |s.power p|
have rw₄ : |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| =
  |HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2|
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
    mem_sphere.mp hb, power, 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
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hq : dist a s.center = dist b s.center
rw : dist a p * dist p b = |s.power p|
rw₁ : dist a p * dist b p = |s.power p|
rw₂ : |HPow.hPow (β := ℕ) (dist b s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = |s.power p|
rw₃ : |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = |s.power p|
rw₄ :
  |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| =
    |HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2|
⊢ dist p a * dist p b = |s.power p|
have rw₅ : |HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2| =
  |HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2|
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
    mem_sphere.mp hb, power, 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
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
⊢ dist a s.center = dist b s.center
have rw : s.radius = dist b s.center
Tactic: rw [mem_sphere.mp ha, mem_sphere.mp hb]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
rw : s.radius = dist b s.center
⊢ dist a s.center = dist b s.center
have rw₁ : s.radius = s.radius
Tactic: rw [mem_sphere.mp ha, mem_sphere.mp hb]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
⊢ dist p a * dist p b = 0
have hq : dist a s.center = dist b s.center
Tactic: have hq : dist a s.center = dist b s.center := by
    rw [mem_sphere.mp ha, mem_sphere.mp hb]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
hq : dist a s.center = dist b s.center
⊢ dist p a * dist p b = 0
have rw : dist a p * dist p b = 0
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
      mem_sphere.mp hb, mem_sphere.mp hp_on, sub_self, abs_zero]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
hq : dist a s.center = dist b s.center
rw : dist a p * dist p b = 0
⊢ dist p a * dist p b = 0
have rw₁ : dist a p * dist b p = 0
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
      mem_sphere.mp hb, mem_sphere.mp hp_on, sub_self, abs_zero]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
hq : dist a s.center = dist b s.center
rw : dist a p * dist p b = 0
rw₁ : dist a p * dist b p = 0
⊢ dist p a * dist p b = 0
have rw₂ : |HPow.hPow (β := ℕ) (dist b s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = 0
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
      mem_sphere.mp hb, mem_sphere.mp hp_on, sub_self, abs_zero]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
hq : dist a s.center = dist b s.center
rw : dist a p * dist p b = 0
rw₁ : dist a p * dist b p = 0
rw₂ : |HPow.hPow (β := ℕ) (dist b s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = 0
⊢ dist p a * dist p b = 0
have rw₃ : |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = 0
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
      mem_sphere.mp hb, mem_sphere.mp hp_on, sub_self, abs_zero]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
hq : dist a s.center = dist b s.center
rw : dist a p * dist p b = 0
rw₁ : dist a p * dist b p = 0
rw₂ : |HPow.hPow (β := ℕ) (dist b s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = 0
rw₃ : |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = 0
⊢ dist p a * dist p b = 0
have rw₄ : |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) s.radius 2| = 0
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
      mem_sphere.mp hb, mem_sphere.mp hp_on, sub_self, abs_zero]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
hq : dist a s.center = dist b s.center
rw : dist a p * dist p b = 0
rw₁ : dist a p * dist b p = 0
rw₂ : |HPow.hPow (β := ℕ) (dist b s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = 0
rw₃ : |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = 0
rw₄ : |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) s.radius 2| = 0
⊢ dist p a * dist p b = 0
have rw₅ : Eq (α := ℝ) |0| 0
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
      mem_sphere.mp hb, mem_sphere.mp hp_on, sub_self, abs_zero]
-- 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
s : Sphere P
p a b : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
hq : dist a s.center = dist b s.center
rw : dist a p * dist p b = 0
rw₁ : dist a p * dist b p = 0
rw₂ : |HPow.hPow (β := ℕ) (dist b s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = 0
rw₃ : |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2| = 0
rw₄ : |HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) s.radius 2| = 0
rw₅ : Eq (α := ℝ) |0| 0
⊢ dist p a * dist p b = 0
have rw₆ : Eq (α := ℝ) 0 0
Tactic: rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
      mem_sphere.mp hb, mem_sphere.mp hp_on, sub_self, abs_zero]
-- 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
s : Sphere P
p a b : P
hr : 0 ≤ s.radius
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hle : s.radius ≤ dist p s.center
⊢ dist p a * dist p b = s.power p
have rw : |s.power p| = s.power p
Tactic: rw [mul_dist_eq_abs_power hp ha hb,
    abs_of_nonneg <| (power_nonneg_iff_radius_le_dist_center hr).mpr hle]
-- 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
s : Sphere P
p a b : P
hr : 0 ≤ s.radius
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hle : s.radius ≤ dist p s.center
rw : |s.power p| = s.power p
⊢ dist p a * dist p b = s.power p
have rw₁ : s.power p = s.power p
Tactic: rw [mul_dist_eq_abs_power hp ha hb,
    abs_of_nonneg <| (power_nonneg_iff_radius_le_dist_center hr).mpr hle]
-- 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
s : Sphere P
p a b : P
hr : 0 ≤ s.radius
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hle : dist p s.center ≤ s.radius
⊢ dist p a * dist p b = -s.power p
have rw : |s.power p| = -s.power p
Tactic: rw [mul_dist_eq_abs_power hp ha hb,
    abs_of_nonpos <| (power_nonpos_iff_dist_center_le_radius hr).mpr hle]
-- 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
s : Sphere P
p a b : P
hr : 0 ≤ s.radius
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
ha : a ∈ s
hb : b ∈ s
hle : dist p s.center ≤ s.radius
rw : |s.power p| = -s.power p
⊢ dist p a * dist p b = -s.power p
have rw₁ : -s.power p = -s.power p
Tactic: rw [mul_dist_eq_abs_power hp ha hb,
    abs_of_nonpos <| (power_nonpos_iff_dist_center_le_radius hr).mpr hle]
-- 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 t p : P
s : Sphere P
ha : a ∈ s
hb : b ∈ s
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
h_tangent : s.IsTangentAt t (affineSpan ℝ {p, t})
⊢ HPow.hPow (β := ℕ) (dist p t) 2 = dist p a * dist p b
have hr : 0 ≤ s.radius
Tactic: have hr := radius_nonneg_of_mem ha
-- 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 t p : P
s : Sphere P
ha : a ∈ s
hb : b ∈ s
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
h_tangent : s.IsTangentAt t (affineSpan ℝ {p, t})
hr : 0 ≤ s.radius
⊢ HPow.hPow (β := ℕ) (dist p t) 2 = dist p a * dist p b
have radius_le_dist : s.radius ≤ dist p s.center
Tactic: have radius_le_dist := h_tangent.isTangent.radius_le_dist_center (left_mem_affineSpan_pair ℝ p t)
-- 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 t p : P
s : Sphere P
ha : a ∈ s
hb : b ∈ s
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
h_tangent : s.IsTangentAt t (affineSpan ℝ {p, t})
hr : 0 ≤ s.radius
radius_le_dist : s.radius ≤ dist p s.center
⊢ HPow.hPow (β := ℕ) (dist p t) 2 = dist p a * dist p b
have rw : HPow.hPow (β := ℕ) (dist p t) 2 =
  HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist p t) 2 - HPow.hPow (β := ℕ) s.radius 2
Tactic: rw [mul_dist_eq_power_of_radius_le_dist_center hr hp ha hb radius_le_dist,
    Sphere.power, h_tangent.dist_sq_eq_of_mem (left_mem_affineSpan_pair ℝ p t)]
-- 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
s : Sphere P
t p : P
h_tangent : s.IsTangentAt t (affineSpan ℝ {p, t})
⊢ s.power p = HPow.hPow (β := ℕ) (dist p t) 2
have rw : HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist p t) 2 - HPow.hPow (β := ℕ) s.radius 2 =
  HPow.hPow (β := ℕ) (dist p t) 2
Tactic: rw [Sphere.power, h_tangent.dist_sq_eq_of_mem (left_mem_affineSpan_pair ℝ p t)]
-- 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
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
⊢ ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
have h_dist_eq₁ : ‖p -ᵥ t‖ * ‖p -ᵥ t‖ = ‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ - ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖
Tactic: simp only [Sphere.power, ← mem_sphere.mp ht, dist_eq_norm_vsub V, sq,
                 ← vsub_add_vsub_cancel p t s.center] at h_dist_eq
Cleared hypotheses: h_dist_eq
-- 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
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq :
  ‖p -ᵥ t‖ * ‖p -ᵥ t‖ = ‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ - ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖
⊢ ‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ = ‖p -ᵥ t‖ * ‖p -ᵥ t‖ + ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖
have linarith : ‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ < ‖p -ᵥ t‖ * ‖p -ᵥ t‖ + ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖ →
  ‖p -ᵥ t‖ * ‖p -ᵥ t‖ - (‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ - ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖) +
      (‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ -
        (‖p -ᵥ t‖ * ‖p -ᵥ t‖ + ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖)) =
    0
Tactic: linarith
-- 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
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq :
  ‖p -ᵥ t‖ * ‖p -ᵥ t‖ = ‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ - ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖
linarith :
  ‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ < ‖p -ᵥ t‖ * ‖p -ᵥ t‖ + ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖ →
    ‖p -ᵥ t‖ * ‖p -ᵥ t‖ -
          (‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ - ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖) +
        (‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ -
          (‖p -ᵥ t‖ * ‖p -ᵥ t‖ + ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖)) =
      0
⊢ ‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ = ‖p -ᵥ t‖ * ‖p -ᵥ t‖ + ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖
have linarith₁ : ‖p -ᵥ t‖ * ‖p -ᵥ t‖ + ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖ < ‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ →
  -(‖p -ᵥ t‖ * ‖p -ᵥ t‖ -
          (‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ - ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖)) +
      (‖p -ᵥ t‖ * ‖p -ᵥ t‖ + ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖ -
        ‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖) =
    0
Tactic: linarith
-- 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
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
⊢ s.IsTangentAt t (affineSpan ℝ {p, t})
have h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
Tactic: have h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0 := by
      simp only [Sphere.power, ← mem_sphere.mp ht, dist_eq_norm_vsub V, sq,
                 ← vsub_add_vsub_cancel p t s.center] at h_dist_eq
      exact (norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero _ _).mp (by linarith)
-- 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
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
⊢ s.IsTangentAt t (affineSpan ℝ {p, t})
have refine : ∀ (x : P) (hx : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, t}) x),
  Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius t) x
Tactic: refine ⟨ht, right_mem_affineSpan_pair ℝ p t, fun x hx ↦ ?_⟩
-- 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
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, t}) x
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius t) x
have rw : ⟪x -ᵥ t, t -ᵥ s.center⟫ = 0
Tactic: rw [mem_orthRadius_iff_inner_left]
-- 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
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, t}) x
⊢ ⟪x -ᵥ t, t -ᵥ s.center⟫ = 0
have obtain : ∀ (r : ℝ) (hr : r • (p -ᵥ t) = x -ᵥ t), ⟪x -ᵥ t, t -ᵥ s.center⟫ = 0
Tactic: obtain ⟨r, hr⟩ := (vadd_right_mem_affineSpan_pair (k := ℝ)).mp (vsub_vadd x t ▸ hx)
-- 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
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, t}) x
r : ℝ
hr : r • (p -ᵥ t) = x -ᵥ t
⊢ ⟪x -ᵥ t, t -ᵥ s.center⟫ = 0
have rw : ⟪r • (p -ᵥ t), t -ᵥ s.center⟫ = 0
Tactic: rw [← hr, inner_smul_left, h_orth, 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
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, t}) x
r : ℝ
hr : r • (p -ᵥ t) = x -ᵥ t
rw : ⟪r • (p -ᵥ t), t -ᵥ s.center⟫ = 0
⊢ ⟪x -ᵥ t, t -ᵥ s.center⟫ = 0
have rw₁ : HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
Tactic: rw [← hr, inner_smul_left, h_orth, 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
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, t}) x
r : ℝ
hr : r • (p -ᵥ t) = x -ᵥ t
rw : ⟪r • (p -ᵥ t), t -ᵥ s.center⟫ = 0
rw₁ : HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
⊢ ⟪x -ᵥ t, t -ᵥ s.center⟫ = 0
have rw₂ : HMul.hMul (α := ℝ) (β := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) (0 : ℝ) = 0
Tactic: rw [← hr, inner_smul_left, h_orth, 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
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, t}) x
r : ℝ
hr : r • (p -ᵥ t) = x -ᵥ t
rw : ⟪r • (p -ᵥ t), t -ᵥ s.center⟫ = 0
rw₁ : HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
rw₂ : HMul.hMul (α := ℝ) (β := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) (0 : ℝ) = 0
⊢ ⟪x -ᵥ t, t -ᵥ s.center⟫ = 0
have rw₃ : Eq (α := ℝ) 0 0
Tactic: rw [← hr, inner_smul_left, h_orth, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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 c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
⊢ dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
have h' : Cospherical (P := P) {a, c, b, d}
Tactic: have h' : Cospherical ({a, c, b, d} : Set P) := by rwa [Set.insert_comm c b {d}]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Ptolemy (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 c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
⊢ dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
have hmul : dist a p * dist c p = dist b p * dist d p
Tactic: have hmul := mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi h' hapc hbpd