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
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)
rw : ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
⊢ ‖a -ᵥ p‖ * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|

Tactic:
rw [dist_eq_norm_vsub V]

Premises used: 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
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)
rw : ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) ‖b -ᵥ q‖ 2 - HPow.hPow (β := ℕ) (dist p q) 2|
⊢ ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|

Tactic:
rw [dist_eq_norm_vsub V]

Premises used: 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
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)
rw : ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) ‖b -ᵥ q‖ 2 - HPow.hPow (β := ℕ) ‖p -ᵥ q‖ 2|
⊢ ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) ‖b -ᵥ q‖ 2 - HPow.hPow (β := ℕ) (dist p q) 2|

Tactic:
rw [dist_eq_norm_vsub V]

Premises used: 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
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)
iterate : ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) ‖b -ᵥ q‖ 2 - HPow.hPow (β := ℕ) ‖p -ᵥ q‖ 2|
⊢ dist a p * dist b p = |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|

Tactic:
iterate 4 rw [dist_eq_norm_vsub V]

Premises used: 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
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)
rw :
  ‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ =
    |HPow.hPow (β := ℕ) ‖m -ᵥ q + (m -ᵥ a)‖ 2 - HPow.hPow (β := ℕ) ‖m -ᵥ q - (m -ᵥ p)‖ 2|
⊢ ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |HPow.hPow (β := ℕ) ‖b -ᵥ q‖ 2 - HPow.hPow (β := ℕ) ‖p -ᵥ q‖ 2|

Tactic:
rw [← h1, ← h2, h, h]
-- 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 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)
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|
⊢ ‖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

Premises used: 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
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|

Tactic:
mul_norm_eq_abs_sub_sq_norm ?_ hq

Premises used: InnerProductGeometry.mul_norm_eq_abs_sub_sq_norm
-- 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 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)
refine : ∃ (k : ℝ), m -ᵥ p = k • (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:
refine mul_norm_eq_abs_sub_sq_norm ?_ hq

Premises used: InnerProductGeometry.mul_norm_eq_abs_sub_sq_norm
-- 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 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)
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)
⊢ ∃ (k : ℝ), m -ᵥ p = k • (m -ᵥ a)

Tactic:
rw [← vsub_vadd p a, vadd_left_mem_affineSpan_pair] at hp

Premises used: vsub_vadd, vadd_left_mem_affineSpan_pair
-- 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 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)
rcases : ∀ (r : ℝ) (hr : r • (b -ᵥ a) = p -ᵥ a), ∃ (k : ℝ), m -ᵥ p = k • (m -ᵥ a)
⊢ ∃ (k : ℝ), m -ᵥ p = k • (m -ᵥ a)

Tactic:
rcases hp with ⟨r, hr⟩
-- 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 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
⊢ 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

Premises used: eq_sub_iff_add_eq', eq_sub_iff_add_eq
-- 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 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 : m -ᵥ p = m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a))
rw : ∃ (k : ℝ), m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a)) = k • (m -ᵥ a)
⊢ ∃ (k : ℝ), m -ᵥ p = k • (m -ᵥ a)

Tactic:
rw [hr]
-- 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 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 : m -ᵥ p = m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a))
h₁ : m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a)) = (1 - r * 2) • (m -ᵥ a)
⊢ ∃ (k : ℝ), m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a)) = k • (m -ᵥ a)

Tactic:
use 1 - r * 2
-- 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 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 : m -ᵥ p = m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a))
match_scalars : 1 - r * HAdd.hAdd (α := ℝ) 1 1 = (1 - r * 2) * 1
⊢ m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a)) = (1 - r * 2) • (m -ᵥ a)

Tactic:
match_scalars
-- 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 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 : m -ᵥ p = m -ᵥ a - r • (m -ᵥ a + (m -ᵥ a))
⊢ 1 - r * HAdd.hAdd (α := ℝ) 1 1 = (1 - r * 2) * 1

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
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
obtain :
  ∀ (q : P) (r : ℝ) (h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r),
    dist a p * dist b p = dist c p * dist d p
⊢ dist a p * dist b p = dist c p * dist d p

Tactic:
obtain ⟨q, r, h'⟩ := (cospherical_def {a, b, c, d}).mp h

Premises used: Insert.insert, EuclideanGeometry.cospherical_def, Iff.mp, Singleton.singleton
-- 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
⊢ Membership.mem (γ := Set P) {a, b, c, d} 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
⊢ Membership.mem (γ := Set P) {a, b, c, d} 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
⊢ Membership.mem (γ := Set P) {a, b, c, 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
⊢ Membership.mem (γ := Set P) {a, b, c, 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
⊢ dist a q = r

Tactic:
obtain ⟨ha, hb, hc, hd⟩ := h' a (by simp), h' b (by simp), h' c (by simp), h' d (by 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
⊢ dist b q = r

Tactic:
obtain ⟨ha, hb, hc, hd⟩ := h' a (by simp), h' b (by simp), h' c (by simp), h' d (by 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
⊢ dist c q = r

Tactic:
obtain ⟨ha, hb, hc, hd⟩ := h' a (by simp), h' b (by simp), h' c (by simp), h' d (by 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
hc : dist c q = r
⊢ dist d q = r

Tactic:
obtain ⟨ha, hb, hc, hd⟩ := h' a (by simp), h' b (by simp), h' c (by simp), h' d (by 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
hc : dist c q = r
hd : dist d q = r
⊢ dist c q = dist d q

Tactic:
rw [← hd] at hc
-- 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
hc : dist c q = r
hd : dist d q = r
hc₁ : dist c q = dist d q
⊢ dist d q = r

Tactic:
rw [← hd] at hc
-- 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}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
⊢ dist a q = dist b q

Tactic:
rw [← hb] at 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 c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
ha₁ : dist a q = dist b q
⊢ dist b q = r

Tactic:
rw [← hb] at 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 c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
ha₁ : dist a q = dist b q
hb₁ : dist b q = r
⊢ dist c q = dist d q

Tactic:
rw [← hb] at 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 c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = r
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
ha₁ : dist a q = dist b q
hb₁ : dist b q = r
hc₁ : dist c q = dist d q
⊢ dist d q = r

Tactic:
rw [← hb] at 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 c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapb : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {a, b}) p
hcpd : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {c, d}) p
q : P
r : ℝ
h' : ∀ (p : P), Membership.mem (γ := Set P) {a, b, c, d} p → dist p q = r
ha : dist a q = dist b q
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
rw : |HPow.hPow (β := ℕ) (dist b q) 2 - HPow.hPow (β := ℕ) (dist p q) 2| = dist c p * dist d p
rw₁ : |HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) (dist p q) 2| = dist c p * dist d p
rw₂ :
  |HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) (dist p q) 2| =
    |HPow.hPow (β := ℕ) (dist d q) 2 - HPow.hPow (β := ℕ) (dist p q) 2|
rw₃ rw₄ :
  |HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) (dist p q) 2| =
    |HPow.hPow (β := ℕ) r 2 - HPow.hPow (β := ℕ) (dist p q) 2|
⊢ dist a p * dist b p = dist c p * dist d p

Tactic:
rw [mul_dist_eq_abs_sub_sq_dist hapb ha, hb, mul_dist_eq_abs_sub_sq_dist hcpd hc, hd]

Premises used: EuclideanGeometry.mul_dist_eq_abs_sub_sq_dist
-- 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}
hapb : ∠ a p b = π
hcpd : ∠ c p d = π
⊢ Sbtw ℝ a p b

Tactic:
rw [EuclideanGeometry.angle_eq_pi_iff_sbtw] at hapb hcpd

Premises used: EuclideanGeometry.angle_eq_pi_iff_sbtw
-- 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}
hapb : ∠ a p b = π
hcpd : ∠ c p d = π
hapb₁ : Sbtw ℝ a p b
⊢ Sbtw ℝ c p d

Tactic:
rw [EuclideanGeometry.angle_eq_pi_iff_sbtw] at hapb hcpd

Premises used: EuclideanGeometry.angle_eq_pi_iff_sbtw
-- 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}
hapb : Sbtw ℝ a p b
hcpd : Sbtw ℝ c p d
⊢ dist a p * dist b p = dist c p * dist d p

Tactic:
mul_dist_eq_mul_dist_of_cospherical h hapb.wbtw.mem_affineSpan hcpd.wbtw.mem_affineSpan

Premises used: EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical, Sbtw.wbtw, Wbtw.mem_affineSpan
-- 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}
hapb : Sbtw ℝ a p b
hcpd : Sbtw ℝ 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.wbtw.mem_affineSpan hcpd.wbtw.mem_affineSpan

Premises used: EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical, Sbtw.wbtw, Wbtw.mem_affineSpan
-- 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
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Oriented ℝ V (Fin 2)
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₃}
h_equiv : Cospherical (P := P) {p₁, p₂, p₄, p₃}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄}

Tactic:
grind [Set.pair_comm p₄ p₃]

Premises used: Set.pair_comm