awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := AffineSubspace.subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S
p₁' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₁ ⋯
p' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p ⋯
p₃' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₃ ⋯
p₂' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₂ hp₂
p₄' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₄ hp₄
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
⊢ ¬Collinear ℝ (P := ↥S) {p₁', p', p₃'}

Tactic:
have hncol : ¬ Collinear ℝ {p₁', p', p₃'} := by
    rw [← affineIndependent_iff_not_collinear_set,
      ← s_isom.toAffineMap.affineIndependent_iff s_isom.injective]
    convert! hindep
    ext i; fin_cases i <;> rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := AffineSubspace.subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S
p₁' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₁ ⋯
p' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p ⋯
p₃' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₃ ⋯
p₂' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₂ hp₂
p₄' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₄ hp₄
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
hncol : ¬Collinear ℝ (P := ↥S) {p₁', p', p₃'}
⊢ Cospherical (P := ↥S) {p₁', p₂', p₃', p₄'}

Tactic:
cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi_aux h_dist' hp₁'p₂' hp₃'p₄' hncol

Premises used: _private.0.EuclideanGeometry.cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi_aux
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ (P := P) {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := AffineSubspace.subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S
p₁' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₁ ⋯
p' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p ⋯
p₃' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₃ ⋯
p₂' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₂ hp₂
p₄' : ↥S := Subtype.mk (p := fun (x : P) ↦ x ∈ S) p₄ hp₄
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank.{0, u_1} ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := Basis.orientation (finBasisOfFinrankEq ℝ ↥S.direction ⋯) }
hncol : ¬Collinear ℝ (P := ↥S) {p₁', p', p₃'}
⊢ Cospherical (P := ↥S) {p₁', p₂', p₃', p₄'}

Tactic:
exact cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi_aux h_dist' hp₁'p₂' hp₃'p₄' hncol

Premises used: _private.0.EuclideanGeometry.cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi_aux
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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}
hab : a ≠ b
hcd : c ≠ d
hapb : ∠ a p b = 0
hcpd : ∠ c p d = 0
⊢ Collinear ℝ (P := P) {a, p, b}

Tactic:
apply collinear_of_angle_eq_zero at hapb

Premises used: EuclideanGeometry.collinear_of_angle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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}
hab : a ≠ b
hcd : c ≠ d
hcpd : ∠ c p d = 0
hapb : Collinear ℝ (P := P) {a, p, b}
⊢ Collinear ℝ (P := P) {c, p, d}

Tactic:
apply collinear_of_angle_eq_zero at hcpd

Premises used: EuclideanGeometry.collinear_of_angle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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}
hab : a ≠ b
hcd : c ≠ d
hapb : Collinear ℝ (P := P) {a, p, b}
hcpd : Collinear ℝ (P := P) {c, p, d}
⊢ Membership.mem (γ := Set P) {a, p, b} a

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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}
hab : a ≠ b
hcd : c ≠ d
hapb : Collinear ℝ (P := P) {a, p, b}
hcpd : Collinear ℝ (P := P) {c, p, d}
⊢ Membership.mem (γ := Set P) {a, p, b} b

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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}
hab : a ≠ b
hcd : c ≠ d
hapb : Collinear ℝ (P := P) {a, p, b}
hcpd : Collinear ℝ (P := P) {c, p, d}
⊢ Membership.mem (γ := Set P) {a, p, b} p

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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}
hab : a ≠ b
hcd : c ≠ d
hapb : Collinear ℝ (P := P) {a, p, b}
hcpd : Collinear ℝ (P := P) {c, p, d}
⊢ Membership.mem (γ := Set P) {c, p, d} c

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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}
hab : a ≠ b
hcd : c ≠ d
hapb : Collinear ℝ (P := P) {a, p, b}
hcpd : Collinear ℝ (P := P) {c, p, d}
⊢ Membership.mem (γ := Set P) {c, p, d} d

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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}
hab : a ≠ b
hcd : c ≠ d
hapb : Collinear ℝ (P := P) {a, p, b}
hcpd : Collinear ℝ (P := P) {c, p, d}
⊢ Membership.mem (γ := Set P) {c, p, d} p

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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}
hab : a ≠ b
hcd : c ≠ d
hapb : Collinear ℝ (P := P) {a, p, b}
hcpd : Collinear ℝ (P := P) {c, p, d}
⊢ dist a p * dist b p = dist c p * dist d p

Tactic:
exact mul_dist_eq_mul_dist_of_cospherical h
    (hapb.mem_affineSpan_of_mem_of_ne (by simp) (by simp) (by simp) hab)
    (hcpd.mem_affineSpan_of_mem_of_ne (by simp) (by simp) (by simp) hcd)

Premises used: Collinear.mem_affineSpan_of_mem_of_ne, EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 = 0 ↔ p ∈ s
rw₁ : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 = 0 ↔ dist p s.center = s.radius
rw₂ : HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) s.radius 2 ↔ dist p s.center = s.radius
rw₃ rw₄ : dist p s.center = s.radius ↔ dist p s.center = s.radius
⊢ s.power p = 0 ↔ p ∈ s

Tactic:
rw [power, mem_sphere, sub_eq_zero, pow_left_inj₀ dist_nonneg hr two_ne_zero]

Premises used: sub_eq_zero, dist_nonneg, pow_left_inj₀, EuclideanGeometry.Sphere.power, two_ne_zero, EuclideanGeometry.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : 0 < HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ↔ s.radius < dist p s.center
rw₁ : HPow.hPow (β := ℕ) s.radius 2 < HPow.hPow (β := ℕ) (dist p s.center) 2 ↔ s.radius < dist p s.center
rw₂ rw₃ : s.radius < dist p s.center ↔ s.radius < dist p s.center
⊢ 0 < s.power p ↔ s.radius < dist p s.center

Tactic:
rw [power, sub_pos, pow_lt_pow_iff_left₀ hr dist_nonneg two_ne_zero]

Premises used: sub_pos, dist_nonneg, EuclideanGeometry.Sphere.power, two_ne_zero, pow_lt_pow_iff_left₀
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 < 0 ↔ dist p s.center < s.radius
rw₁ : HPow.hPow (β := ℕ) (dist p s.center) 2 < HPow.hPow (β := ℕ) s.radius 2 ↔ dist p s.center < s.radius
rw₂ rw₃ : dist p s.center < s.radius ↔ dist p s.center < s.radius
⊢ s.power p < 0 ↔ dist p s.center < s.radius

Tactic:
rw [power, sub_neg, pow_lt_pow_iff_left₀ dist_nonneg hr two_ne_zero]

Premises used: sub_neg, dist_nonneg, EuclideanGeometry.Sphere.power, two_ne_zero, pow_lt_pow_iff_left₀
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : 0 ≤ HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ↔ s.radius ≤ dist p s.center
rw₁ : HPow.hPow (β := ℕ) s.radius 2 ≤ HPow.hPow (β := ℕ) (dist p s.center) 2 ↔ s.radius ≤ dist p s.center
rw₂ rw₃ : s.radius ≤ dist p s.center ↔ s.radius ≤ dist p s.center
⊢ 0 ≤ s.power p ↔ s.radius ≤ dist p s.center

Tactic:
rw [power, sub_nonneg, pow_le_pow_iff_left₀ hr dist_nonneg two_ne_zero]

Premises used: dist_nonneg, pow_le_pow_iff_left₀, EuclideanGeometry.Sphere.power, two_ne_zero, sub_nonneg
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
P : Type u_2
inst : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
rw : HPow.hPow (β := ℕ) (dist p s.center) 2 - HPow.hPow (β := ℕ) s.radius 2 ≤ 0 ↔ dist p s.center ≤ s.radius
rw₁ : HPow.hPow (β := ℕ) (dist p s.center) 2 ≤ HPow.hPow (β := ℕ) s.radius 2 ↔ dist p s.center ≤ s.radius
rw₂ rw₃ : dist p s.center ≤ s.radius ↔ dist p s.center ≤ s.radius
⊢ s.power p ≤ 0 ↔ dist p s.center ≤ s.radius

Tactic:
rw [power, sub_nonpos, pow_le_pow_iff_left₀ dist_nonneg hr two_ne_zero]

Premises used: dist_nonneg, pow_le_pow_iff_left₀, EuclideanGeometry.Sphere.power, two_ne_zero, sub_nonpos
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
rw : s.radius = dist b s.center
rw₁ rw₂ : s.radius = s.radius
⊢ dist a s.center = dist b s.center

Tactic:
rw [mem_sphere.mp ha, mem_sphere.mp hb]

Premises used: EuclideanGeometry.mem_sphere, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
⊢ 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]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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|
rw₅ 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|
⊢ dist p a * dist p b = |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]

Premises used: EuclideanGeometry.Sphere.power, dist_comm, EuclideanGeometry.mem_sphere, EuclideanGeometry.mul_dist_eq_abs_sub_sq_dist, Iff.mp, abs_sub_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
rw₁ rw₂ : s.radius = s.radius
⊢ dist a s.center = dist b s.center

Tactic:
rw [mem_sphere.mp ha, mem_sphere.mp hb]

Premises used: EuclideanGeometry.mem_sphere, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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

Tactic:
have hq : dist a s.center = dist b s.center := by
    rw [mem_sphere.mp ha, mem_sphere.mp hb]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
rw₆ rw₇ : Eq (α := ℝ) 0 0
⊢ dist p a * 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]

Premises used: sub_self, dist_comm, EuclideanGeometry.mem_sphere, EuclideanGeometry.mul_dist_eq_abs_sub_sq_dist, abs_zero, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
rw₁ rw₂ : s.power p = s.power p
⊢ dist p a * dist p b = 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]

Premises used: EuclideanGeometry.Sphere.mul_dist_eq_abs_power, Iff.mpr, EuclideanGeometry.Sphere.power_nonneg_iff_radius_le_dist_center, abs_of_nonneg
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
rw₁ rw₂ : -s.power p = -s.power p
⊢ dist p a * dist p b = -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]

Premises used: EuclideanGeometry.Sphere.mul_dist_eq_abs_power, Iff.mpr, abs_of_nonpos, EuclideanGeometry.Sphere.power_nonpos_iff_dist_center_le_radius
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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})
⊢ 0 ≤ s.radius

Tactic:
have hr := radius_nonneg_of_mem ha
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
⊢ s.radius ≤ dist p s.center

Tactic:
have radius_le_dist := h_tangent.isTangent.radius_le_dist_center (left_mem_affineSpan_pair ℝ p t)
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
rw :
  HPow.hPow (β := ℕ) (dist p t) 2 =
    HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist p t) 2 - HPow.hPow (β := ℕ) s.radius 2
⊢ HPow.hPow (β := ℕ) (dist p t) 2 = dist p a * dist p b

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)]

Premises used: Real, EuclideanGeometry.Sphere.power, EuclideanGeometry.Sphere.mul_dist_eq_power_of_radius_le_dist_center, left_mem_affineSpan_pair, EuclideanGeometry.Sphere.IsTangentAt.dist_sq_eq_of_mem
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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 =
    HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist p t) 2 - HPow.hPow (β := ℕ) s.radius 2

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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})
rw :
  HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist p t) 2 - HPow.hPow (β := ℕ) s.radius 2 =
    HPow.hPow (β := ℕ) (dist p t) 2
⊢ s.power p = HPow.hPow (β := ℕ) (dist p t) 2

Tactic:
rw [Sphere.power, h_tangent.dist_sq_eq_of_mem (left_mem_affineSpan_pair ℝ p t)]

Premises used: Real, EuclideanGeometry.Sphere.power, left_mem_affineSpan_pair, EuclideanGeometry.Sphere.IsTangentAt.dist_sq_eq_of_mem
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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})
⊢ HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist p t) 2 - HPow.hPow (β := ℕ) s.radius 2 =
    HPow.hPow (β := ℕ) (dist p t) 2

Tactic:
ring_nf
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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‖ * ‖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

Premises used: vsub_add_vsub_cancel, EuclideanGeometry.Sphere.power, sq, EuclideanGeometry.Sphere.center, EuclideanGeometry.mem_sphere, Iff.mp, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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
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
⊢ ‖p -ᵥ t + (t -ᵥ s.center)‖ * ‖p -ᵥ t + (t -ᵥ s.center)‖ = ‖p -ᵥ t‖ * ‖p -ᵥ t‖ + ‖t -ᵥ s.center‖ * ‖t -ᵥ s.center‖

Tactic:
linarith
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
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⟫ = 0

Tactic:
exact (norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero _ _).mp (by linarith)

Premises used: norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, Iff.mp