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 : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ¬Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ⊥
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
v : V
hvm : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv0 : v ≠ 0
⊢ HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)) 2 =
    HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
Real.sq_sqrt ?_

Premises used: Real.sq_sqrt
-- 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
hp : p ≠ s.center
hb : ¬Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ⊥
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
v : V
hvm : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv0 : v ≠ 0
inl : 0 ≤ HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)) 2 =
    HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
refine Real.sq_sqrt ?_

Premises used: Real.sq_sqrt
-- 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
hp : p ≠ s.center
hb : ¬Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ⊥
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
v : V
hvm : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv0 : v ≠ 0
inl : dist p s.center ≤ |s.radius|
⊢ 0 ≤ HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
rw [sub_nonneg, sq_le_sq, abs_of_nonneg dist_nonneg]

Premises used: sq_le_sq, dist_nonneg, abs_of_nonneg, sub_nonneg
-- 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
hp : p ≠ s.center
hb : ¬Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ⊥
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
v : V
hvm : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv0 : v ≠ 0
⊢ dist p s.center ≤ |s.radius|

Tactic:
h.le.trans (le_abs_self _)

Premises used: le_abs_self, LT.lt.le, LE.le.trans
-- 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
hp : p ≠ s.center
hb : ¬Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ⊥
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
v : V
hvm : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv0 : v ≠ 0
⊢ dist p s.center ≤ |s.radius|

Tactic:
exact h.le.trans (le_abs_self _)

Premises used: le_abs_self, LT.lt.le, LE.le.trans
-- 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
inr :
  Eq (α := Set P) {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:
rw [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
h : dist p s.center = s.radius
inr : Subsingleton V → s.radius = 0
⊢ Eq (α := Set P) {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 [Set.singleton_ne_empty, h, lt_self_iff_false, ne_eq, false_and, and_false, false_or,
      false_iff, not_and, not_not]

Premises used: Classical.not_not, false_and, false_or, false_iff, ne_eq, lt_self_iff_false, and_false, not_and, Set.singleton_ne_empty
-- 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
hs : Subsingleton V
⊢ Subsingleton P

Tactic:
rw [AddTorsor.subsingleton_iff V P] at hs

Premises used: AddTorsor.subsingleton_iff
-- 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
hs : Subsingleton P
⊢ dist s.center s.center = s.radius

Tactic:
rw [Subsingleton.elim p s.center] at h

Premises used: EuclideanGeometry.Sphere.center, Subsingleton.elim
-- 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
hs : Subsingleton P
h₁ : dist s.center s.center = s.radius
⊢ Subsingleton P

Tactic:
rw [Subsingleton.elim p s.center] at h

Premises used: EuclideanGeometry.Sphere.center, Subsingleton.elim
-- 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 s.center s.center = s.radius
hs : Subsingleton P
⊢ s.radius = 0

Tactic:
simpa using h.symm

Premises used: Eq.symm
-- 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 : 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

Tactic:
simp [h, inter_orthRadius_eq_empty_of_radius_lt_dist]

Premises used: EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_of_radius_lt_dist
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
⊢ 0 ≤ s.radius

Tactic:
have hr : 0 ≤ s.radius := dist_nonneg.trans 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
rw : Ne (α := ℝ) 1 0
⊢ v ≠ 0

Tactic:
rw [← norm_ne_zero_iff, hv1]

Premises used: norm_ne_zero_iff
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
⊢ Ne (α := ℝ) 1 0

Tactic:
simp
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
⊢ v ≠ 0

Tactic:
have hv0 : v ≠ 0 := by rw [← norm_ne_zero_iff, hv1]; simp
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
rw :
  Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) =
    {√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v +ᵥ p,
      -(√(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 (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v +ᵥ p,
      -√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v +ᵥ p}

Tactic:
rw [neg_smul]

Premises used: neg_smul
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
⊢ Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p)) + 1 = Module.finrank ℝ V

Tactic:
have hf := finrank_orthRadius hpc
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p)) + 1 = Module.finrank ℝ V
⊢ Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ + 1 = Module.finrank ℝ V

Tactic:
rw [direction_orthRadius] at hf

Premises used: EuclideanGeometry.Sphere.direction_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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ + 1 = Module.finrank ℝ V
⊢ Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ = 1

Tactic:
simp only [hf2.out, Nat.reduceEqDiff] at hf

Premises used: Nat.reduceEqDiff, Fact.out
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ = 1
⊢ Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv ≠ 0

Tactic:
simpa using hv0
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ = 1
⊢ ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ),
    ∃ (c : ℝ), c • Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv = w

Tactic:
rw [finrank_eq_one_iff_of_nonzero' ⟨v, hv⟩ (by simpa using hv0)] at hf

Premises used: finrank_eq_one_iff_of_nonzero'
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf :
  ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ),
    ∃ (c : ℝ), c • Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv = w
w : V
hw : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ w
⊢ ∃ (c : ℝ), c • v = w

Tactic:
simpa using hf ⟨w, hw⟩

Premises used: Subtype.mk
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf :
  ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ),
    ∃ (c : ℝ), c • Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv = w
⊢ ∀ (w : V), Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ w → ∃ (c : ℝ), c • v = w

Tactic:
have hvc : ∀ w ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ, ∃ c : ℝ, c • v = w := by
    intro w hw
    simpa using hf ⟨w, hw⟩
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf :
  ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ),
    ∃ (c : ℝ), c • Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv = w
hvc : ∀ (w : V), Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ w → ∃ (c : ℝ), c • v = w
rw : dist p s.center ≤ |s.radius|
⊢ 0 ≤ HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
rw [sub_nonneg, sq_le_sq, abs_of_nonneg dist_nonneg]

Premises used: sq_le_sq, dist_nonneg, abs_of_nonneg, sub_nonneg
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf :
  ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ),
    ∃ (c : ℝ), c • Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv = w
hvc : ∀ (w : V), Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ w → ∃ (c : ℝ), c • v = w
⊢ dist p s.center ≤ |s.radius|

Tactic:
le_abs.2 (.inl hp)

Premises used: Iff.mpr, le_abs, Or.inl
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf :
  ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ),
    ∃ (c : ℝ), c • Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv = w
hvc : ∀ (w : V), Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ w → ∃ (c : ℝ), c • v = w
⊢ dist p s.center ≤ |s.radius|

Tactic:
exact le_abs.2 (.inl hp)

Premises used: Iff.mpr, le_abs, Or.inl
-- 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf :
  ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ),
    ∃ (c : ℝ), c • Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv = w
hvc : ∀ (w : V), Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ w → ∃ (c : ℝ), c • v = w
⊢ 0 ≤ HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
have hvp : 0 ≤ s.radius ^ 2 - (dist p s.center) ^ 2 := by
    rw [sub_nonneg, sq_le_sq, abs_of_nonneg dist_nonneg]
    exact le_abs.2 (.inl 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf :
  ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ),
    ∃ (c : ℝ), c • Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv = w
hvc : ∀ (w : V), Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ w → ∃ (c : ℝ), c • v = w
hvp : 0 ≤ HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
h :
  ∀ (p' : P),
    p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔
      Membership.mem (γ := Set P)
        {√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v +ᵥ p,
          -(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v) +ᵥ p}
        p'
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) =
    {√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v +ᵥ p,
      -(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v) +ᵥ 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf :
  ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ),
    ∃ (c : ℝ), c • Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv = w
hvc : ∀ (w : V), Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ w → ∃ (c : ℝ), c • v = w
hvp : 0 ≤ HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
p' : P
⊢ p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔
    Membership.mem (γ := Set P)
      {√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v +ᵥ p,
        -(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v) +ᵥ p}
      p'

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf :
  ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ),
    ∃ (c : ℝ), c • Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv = w
hvc : ∀ (w : V), Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ w → ∃ (c : ℝ), c • v = w
hvp : 0 ≤ HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
p' : P
h :
  ∀ (h : p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)),
    Membership.mem (γ := Set P)
      {√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v +ᵥ p,
        -(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v) +ᵥ p}
      p'
h₁ :
  ∀
    (h :
      Membership.mem (γ := Set P)
        {√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v +ᵥ p,
          -(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v) +ᵥ p}
        p'),
    p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
⊢ p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔
    Membership.mem (γ := Set P)
      {√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v +ᵥ p,
        -(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v) +ᵥ p}
      p'

Tactic:
refine ⟨fun h ↦ ?_, fun 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf :
  ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ),
    ∃ (c : ℝ), c • Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ x) v hv = w
hvc : ∀ (w : V), Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ w → ∃ (c : ℝ), c • v = w
hvp : 0 ≤ HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
p' : P
h : p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
h₁ :
  p' -ᵥ p = √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v ∨
    p' -ᵥ p = -(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v)
⊢ Membership.mem (γ := Set P)
    {√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v +ᵥ p,
      -(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v) +ᵥ p}
    p'

Tactic:
rw [← vsub_vadd p' p, Set.mem_insert_iff, Set.mem_singleton_iff, vadd_right_cancel_iff,
      vadd_right_cancel_iff]

Premises used: Set.mem_singleton_iff, vsub_vadd, Set.mem_insert_iff, vadd_right_cancel_iff