awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
simp_rw :
  ‖q -ᵥ s.center‖ * ‖q -ᵥ s.center‖ = ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ + ‖q -ᵥ p‖ * ‖q -ᵥ p‖ ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
⊢ HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q

Tactic:
simp_rw [dist_eq_norm_vsub, pow_two]

Premises used: pow_two, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
rw :
  ‖q -ᵥ p + (p -ᵥ s.center)‖ * ‖q -ᵥ p + (p -ᵥ s.center)‖ = ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ + ‖q -ᵥ p‖ * ‖q -ᵥ p‖ ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
⊢ ‖q -ᵥ s.center‖ * ‖q -ᵥ s.center‖ = ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ + ‖q -ᵥ p‖ * ‖q -ᵥ p‖ ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q

Tactic:
rw [← vsub_add_vsub_cancel q p s.center]

Premises used: vsub_add_vsub_cancel, EuclideanGeometry.Sphere.center
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
nth_rw :
  ‖q -ᵥ p + (p -ᵥ s.center)‖ * ‖q -ᵥ p + (p -ᵥ s.center)‖ = ‖q -ᵥ p‖ * ‖q -ᵥ p‖ + ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
⊢ ‖q -ᵥ p + (p -ᵥ s.center)‖ * ‖q -ᵥ p + (p -ᵥ s.center)‖ = ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ + ‖q -ᵥ p‖ * ‖q -ᵥ p‖ ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q

Tactic:
nth_rw 3 [add_comm]

Premises used: add_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
rw : ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0 ↔ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
rw₁ rw₂ :
  Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
⊢ ‖q -ᵥ p + (p -ᵥ s.center)‖ * ‖q -ᵥ p + (p -ᵥ s.center)‖ = ‖q -ᵥ p‖ * ‖q -ᵥ p‖ + ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q

Tactic:
rw [norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, ← mem_orthRadius_iff_inner_left]

Premises used: norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
simp :
  q ∈ s ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 =
        HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 =
          HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ∧
        HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔
    0 ≤ s.radius ∧
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
simp only [Set.mem_inter_iff, Metric.mem_sphere, mem_coe', SetLike.mem_coe,
    ← dist_sq_eq_iff_mem_orthRadius, ← direction_orthRadius,
    vsub_right_mem_direction_iff_mem (s.self_mem_orthRadius p), ← dist_eq_norm_vsub]

Premises used: Set.mem_inter_iff, EuclideanGeometry.Sphere.dist_sq_eq_iff_mem_orthRadius, Metric.mem_sphere, SetLike.mem_coe, EuclideanGeometry.Sphere.mem_coe', dist_eq_norm_vsub, AffineSubspace.vsub_right_mem_direction_iff_mem, EuclideanGeometry.Sphere.direction_orthRadius, EuclideanGeometry.Sphere.self_mem_orthRadius
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
nth_rw :
  q ∈ s ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 =
        HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ∧
        HPow.hPow (β := ℕ) (dist q s.center) 2 =
          HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2
⊢ q ∈ s ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 =
        HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 =
          HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ∧
        HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
nth_rw 3 [and_comm]

Premises used: and_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
rw :
  HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 →
    (q ∈ s ↔
      0 ≤ s.radius ∧
        HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)
⊢ q ∈ s ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 =
        HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ∧
        HPow.hPow (β := ℕ) (dist q s.center) 2 =
          HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2

Tactic:
rw [← and_assoc, and_congr_left_iff]

Premises used: and_congr_left_iff, and_assoc
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2
⊢ HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2

Tactic:
rw [← sub_eq_iff_eq_add'] at h

Premises used: sub_eq_iff_eq_add'
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2
rw :
  q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
        HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
rw [← h]
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2
inl :
  ∀ (h0 : 0 ≤ s.radius),
    q ∈ s ↔
      0 ≤ s.radius ∧
        HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
          HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
inr :
  ∀ (h0 : s.radius < 0),
    q ∈ s ↔
      0 ≤ s.radius ∧
        HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
          HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
        HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
rcases le_or_gt 0 s.radius with h0 | h0

Premises used: le_or_gt, OfNat.ofNat, EuclideanGeometry.Sphere.radius
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2
h0 : 0 ≤ s.radius
⊢ q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
        HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
simp [h0]
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2
h0 : s.radius < 0
inr : q ∉ s
⊢ q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
        HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
simp only [h0.not_ge, sub_left_inj, false_and, iff_false]

Premises used: iff_false, false_and, sub_left_inj, LT.lt.not_ge
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2
h0 : s.radius < 0
hm : q ∈ s
⊢ False

Tactic:
h0.not_ge (radius_nonneg_of_mem hm)

Premises used: EuclideanGeometry.Sphere.radius_nonneg_of_mem, LT.lt.not_ge
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2
h0 : s.radius < 0
hm : q ∈ s
⊢ False

Tactic:
exact h0.not_ge (radius_nonneg_of_mem hm)

Premises used: EuclideanGeometry.Sphere.radius_nonneg_of_mem, LT.lt.not_ge
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : 0 ≤ s.radius
rw :
  0 ≤ s.radius ∧
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
      HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
      HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
rw [mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq]

Premises used: EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : 0 ≤ s.radius
⊢ 0 ≤ s.radius ∧
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
      HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
simp [h]
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
h : 0 ≤ s.radius
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
rw :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ((v +ᵥ p) -ᵥ p) ∧
      HPow.hPow (β := ℕ) ‖(v +ᵥ p) -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
    HPow.hPow (β := ℕ) ‖v‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ v +ᵥ p ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔
    HPow.hPow (β := ℕ) ‖v‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
rw [mem_inter_orthRadius_iff_vsub_mem_and_norm_sq h]

Premises used: EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_vsub_mem_and_norm_sq
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
h : 0 ≤ s.radius
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ((v +ᵥ p) -ᵥ p) ∧
      HPow.hPow (β := ℕ) ‖(v +ᵥ p) -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
    HPow.hPow (β := ℕ) ‖v‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
simp [hv]
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
hp : dist p s.center = s.radius
h : ∀ (p' : P), p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ Membership.mem (γ := Set P) {p} p'
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {p}

Tactic:
ext p'
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
hp : dist p s.center = s.radius
p' : P
h : p' ∈ s ∧ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p' → p' = p
h₁ : p' = p → p' ∈ s ∧ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p'
⊢ p' ∈ s ∧ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p' ↔ p' = p

Tactic:
constructor
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
hp : dist p s.center = s.radius
p' : P
hp's : p' ∈ s
hp'i : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p'
⊢ HPow.hPow (β := ℕ) (dist p' s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist p' p) 2

Tactic:
have h' := dist_sq_eq_of_mem_orthRadius hp'i
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
hp : dist p s.center = s.radius
p' : P
hp's : p' ∈ s
hp'i : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p'
h' : HPow.hPow (β := ℕ) (dist p' s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist p' p) 2
⊢ HPow.hPow (β := ℕ) s.radius 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist p' p) 2

Tactic:
rw [hp's, hp] at h'
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
hp : dist p s.center = s.radius
p' : P
hp's : p' ∈ s
hp'i : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p'
h' : HPow.hPow (β := ℕ) s.radius 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist p' p) 2
⊢ p' = p

Tactic:
simpa using h'
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p' : P
hp : dist p' s.center = s.radius
⊢ p' ∈ s ∧ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p') p'

Tactic:
simpa using hp
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
mp : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q} → q = p ∧ dist p s.center = s.radius
mpr : q = p ∧ dist p s.center = s.radius → Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q} ↔ q = p ∧ dist p s.center = s.radius

Tactic:
constructor
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
⊢ q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)

Tactic:
have hq : q ∈ (s ∩ s.orthRadius p : Set P) := h ▸ Set.mem_singleton _
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
q' : P
⊢ q' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ q' = q

Tactic:
simp [h]
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
⊢ ∀ (q' : P), q' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ q' = q

Tactic:
have h' (q' : P) : q' ∈ (s ∩ s.orthRadius p : Set P) ↔ q' = q := by simp [h]
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
h' : ∀ (q' : P), q' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ q' = q
⊢ 0 ≤ s.radius

Tactic:
have hr : 0 ≤ s.radius := radius_nonneg_of_mem hq.1
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
h' : ∀ (q' : P), q' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ q' = q
hr : 0 ≤ s.radius
⊢ ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
      q' = q

Tactic:
simp_rw [mem_inter_orthRadius_iff_vsub_mem_and_norm_sq hr] at h'

Premises used: EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_vsub_mem_and_norm_sq
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
hr : 0 ≤ s.radius
h' :
  ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
      q' = q
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
have hq' := (h' q).2 rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
hr : 0 ≤ s.radius
h' :
  ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
      q' = q
hq' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ((-(q -ᵥ p) +ᵥ p) -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ 2 =
      HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
simpa [-neg_vsub_eq_vsub_rev] using hq'

Premises used: neg_vsub_eq_vsub_rev
-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
hr : 0 ≤ s.radius
h' :
  ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
      q' = q
hq' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ((-(q -ᵥ p) +ᵥ p) -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ 2 =
      HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
have hq'' : (-(q -ᵥ p) +ᵥ p) -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧
        ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 := by
      simpa [-neg_vsub_eq_vsub_rev] using hq'