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
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
hq'' :
  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
⊢ -(q -ᵥ p) +ᵥ p = q

Tactic:
have hqq := (h' _).1 hq''
-- 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
hq'' :
  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
hqq : HSMul.hSMul (α := ℝ) 2 (q -ᵥ p) = 0
⊢ Ne (α := ℝ) 2 0

Tactic:
norm_num
-- 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
hq'' :
  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
hqq : -(q -ᵥ p) +ᵥ p = q
⊢ q = p

Tactic:
rw [eq_comm, eq_vadd_iff_vsub_eq, eq_neg_iff_add_eq_zero, ← two_smul ℝ,
      smul_eq_zero_iff_right (by norm_num), vsub_eq_zero_iff_eq] at hqq

Premises used: Real, vsub_eq_zero_iff_eq, two_smul, eq_comm, smul_eq_zero_iff_right, eq_neg_iff_add_eq_zero, eq_vadd_iff_vsub_eq
-- 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
hq'' :
  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
hqq : q = p
⊢ q = p ∧ dist p s.center = s.radius

Tactic:
⟨hqq, ?_⟩

Premises used: And.intro
-- 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
hq'' :
  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
hqq : q = p
mp : dist p s.center = s.radius
⊢ q = p ∧ dist p s.center = s.radius

Tactic:
refine ⟨hqq, ?_⟩
-- 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
hq'' :
  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
hqq : q = p
mp :
  ∀ (h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius q) : Set P) = {q})
    (hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius q) : Set P))
    (h' :
      ∀ (q' : P),
        Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ (q' -ᵥ q) ∧
            HPow.hPow (β := ℕ) ‖q' -ᵥ q‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2 ↔
          q' = q)
    (hq' :
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ (q -ᵥ q) ∧
        HPow.hPow (β := ℕ) ‖q -ᵥ q‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2)
    (hq'' :
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ ((-(q -ᵥ q) +ᵥ q) -ᵥ q) ∧
        HPow.hPow (β := ℕ) ‖(-(q -ᵥ q) +ᵥ q) -ᵥ q‖ 2 =
          HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2),
    dist q s.center = s.radius
⊢ dist p s.center = s.radius

Tactic:
subst hqq
-- 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
q : P
hr : 0 ≤ s.radius
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius q) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius q) : Set P)
h' :
  ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ (q' -ᵥ q) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ q‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2 ↔
      q' = q
hq' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ (q -ᵥ q) ∧
    HPow.hPow (β := ℕ) ‖q -ᵥ q‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2
hq'' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ ((-(q -ᵥ q) +ᵥ q) -ᵥ q) ∧
    HPow.hPow (β := ℕ) ‖(-(q -ᵥ q) +ᵥ q) -ᵥ q‖ 2 =
      HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2
⊢ dist q s.center = s.radius

Tactic:
hq.1

Premises used: Set.Mem, setOf, And.left, Metric.sphere
-- 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
q : P
hr : 0 ≤ s.radius
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius q) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius q) : Set P)
h' :
  ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ (q' -ᵥ q) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ q‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2 ↔
      q' = q
hq' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ (q -ᵥ q) ∧
    HPow.hPow (β := ℕ) ‖q -ᵥ q‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2
hq'' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ ((-(q -ᵥ q) +ᵥ q) -ᵥ q) ∧
    HPow.hPow (β := ℕ) ‖(-(q -ᵥ q) +ᵥ q) -ᵥ q‖ 2 =
      HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2
⊢ dist q s.center = s.radius

Tactic:
exact hq.1

Premises used: And.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
q : P
h : dist q s.center = s.radius
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius q) : Set P) = {q}

Tactic:
inter_orthRadius_eq_singleton_of_dist_eq_radius h

Premises used: EuclideanGeometry.Sphere.inter_orthRadius_eq_singleton_of_dist_eq_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
q : P
h : dist q s.center = s.radius
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius q) : Set P) = {q}

Tactic:
exact inter_orthRadius_eq_singleton_of_dist_eq_radius h

Premises used: EuclideanGeometry.Sphere.inter_orthRadius_eq_singleton_of_dist_eq_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 : P
hp : s.radius < dist p s.center
h : ∀ (p' : P), p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ Membership.mem (γ := Set P) ∅ p'
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set 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 : s.radius < dist p s.center
p' : P
h :
  0 ≤ s.radius ∧
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
    Membership.mem (γ := Set P) ∅ p'
⊢ p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ Membership.mem (γ := Set P) ∅ p'

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 : P
hp : s.radius < dist p s.center
p' : P
h :
  0 ≤ s.radius →
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) →
      ¬HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ 0 ≤ s.radius ∧
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
    Membership.mem (γ := Set P) ∅ p'

Tactic:
simp only [Set.mem_empty_iff_false, iff_false, not_and]

Premises used: iff_false, Set.mem_empty_iff_false, not_and
-- 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 : s.radius < dist p s.center
p' : P
hle : 0 ≤ s.radius
h : HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
nlinarith :
  0 - HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 +
          (HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 - (HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)) +
        (0 - (s.radius - dist p s.center) * (s.radius - dist p s.center)) +
      2 * (0 - (s.radius - dist p s.center) * (0 - s.radius)) =
    0
nlinarith₁ : GT.gt (α := ℝ) 2 0
⊢ False

Tactic:
nlinarith
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
h : ∀ (p' : P), p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ Membership.mem (γ := Set P) ∅ p'
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
h :
  0 ≤ s.radius ∧
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
    Membership.mem (γ := Set P) ∅ p'
⊢ p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ Membership.mem (γ := Set P) ∅ p'

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 : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
h :
  0 ≤ s.radius →
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) →
      ¬HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ 0 ≤ s.radius ∧
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
    Membership.mem (γ := Set P) ∅ p'

Tactic:
simp only [Set.mem_empty_iff_false, iff_false, not_and]

Premises used: iff_false, Set.mem_empty_iff_false, not_and
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
hpo : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
⊢ FiniteDimensional ℝ V

Tactic:
have : FiniteDimensional ℝ V := Module.finite_of_finrank_eq_succ hf
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
hpo : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
this : FiniteDimensional ℝ V
⊢ Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center)) + Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ =
    Module.finrank ℝ V

Tactic:
have ha := (ℝ ∙ (p -ᵥ s.center)).finrank_add_finrank_orthogonal
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
hpo : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
this : FiniteDimensional ℝ V
ha :
  Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center)) + Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ =
    Module.finrank ℝ V
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤

Tactic:
simp only [finrank_span_singleton (vsub_ne_zero.2 hpc), hf, Nat.add_eq_left,
    Submodule.finrank_eq_zero, Submodule.orthogonal_eq_bot_iff] at ha

Premises used: Iff.mpr, Submodule.orthogonal_eq_bot_iff, vsub_ne_zero, Submodule.finrank_eq_zero, finrank_span_singleton, Nat.add_eq_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 : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
hpo : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
this : FiniteDimensional ℝ V
ha : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
⊢ p' = p

Tactic:
simp only [ha, Submodule.top_orthogonal_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hpo

Premises used: Submodule.mem_bot, vsub_eq_zero_iff_eq, Submodule.top_orthogonal_eq_bot
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hpo : p' = p
h : ¬0 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ ¬HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
simp only [hpo, vsub_self, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]

Premises used: OfNat.ofNat_ne_zero, norm_zero, ne_eq, not_false_eq_true, vsub_self, zero_pow
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hpo : p' = p
h : ¬dist p s.center = s.radius
⊢ ¬0 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
rw [eq_comm, sub_eq_zero, eq_comm, sq_eq_sq₀ dist_nonneg hr]

Premises used: sub_eq_zero, dist_nonneg, eq_comm, sq_eq_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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hpo : p' = p
⊢ ¬dist p s.center = s.radius

Tactic:
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 : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hpo : p' = p
⊢ ¬dist p s.center = s.radius

Tactic:
exact 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 : P
inl :
  ∀ (h : dist p s.center < s.radius),
    Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
      s.radius < dist p s.center ∨
        Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0
inr :
  ∀ (h : dist p s.center = s.radius),
    Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
      s.radius < dist p s.center ∨
        Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0
inr₁ :
  ∀ (h : s.radius < dist p s.center),
    Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
      s.radius < dist p s.center ∨
        Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0

Tactic:
rcases lt_trichotomy (dist p s.center) s.radius with h | h | h

Premises used: EuclideanGeometry.Sphere.center, Dist.dist, lt_trichotomy, 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 : P
h : dist p s.center < s.radius
inl :
  Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬p = s.center ∨ Subsingleton V
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0

Tactic:
simp only [h.not_gt, h, ne_eq, true_and, (dist_nonneg.trans_lt h).ne', not_false_eq_true,
      and_true, false_or]

Premises used: and_true, dist_nonneg, false_or, ne_eq, LT.lt.ne', LT.lt.not_gt, not_false_eq_true, LE.le.trans_lt, true_and
-- 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
h : dist p s.center < s.radius
inl :
  ∀ (h : dist s.center s.center < s.radius),
    Metric.sphere s.center s.radius ∩ (↑(s.orthRadius s.center) : Set P) = ∅ ↔
      Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V
inl₁ :
  ∀ (hp : p ≠ s.center),
    Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
      Module.finrank ℝ V = 1 ∧ ¬p = s.center ∨ Subsingleton V
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬p = s.center ∨ Subsingleton V

Tactic:
obtain rfl | hp := eq_or_ne p s.center

Premises used: EuclideanGeometry.Sphere.center, eq_or_ne, rfl