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
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)
rw : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p'
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)

Tactic:
rw [← direction_orthRadius, vsub_right_mem_direction_iff_mem (s.self_mem_orthRadius p)]

Premises used: 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
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)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p'

Tactic:
h.2

Premises used: And.right
-- 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)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p'

Tactic:
exact h.2

Premises used: And.right
-- 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)
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)

Tactic:
have h' : p' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ := by
      rw [← direction_orthRadius, vsub_right_mem_direction_iff_mem (s.self_mem_orthRadius p)]
      exact h.2
-- 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' : 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

Tactic:
rw [← vsub_vadd p' p, vadd_mem_inter_orthRadius_iff_norm_sq hr h'] at h

Premises used: EuclideanGeometry.Sphere.vadd_mem_inter_orthRadius_iff_norm_sq, vsub_vadd
-- 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' : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
h₁ : HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)

Tactic:
rw [← vsub_vadd p' p, vadd_mem_inter_orthRadius_iff_norm_sq hr h'] at h

Premises used: EuclideanGeometry.Sphere.vadd_mem_inter_orthRadius_iff_norm_sq, vsub_vadd
-- 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 : HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
h' : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
h₁ :
  ∀ (c : ℝ) (hc : c • v = p' -ᵥ p),
    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)
⊢ 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)

Tactic:
obtain ⟨c, hc⟩ := hvc _ 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 : HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
h' : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
c : ℝ
hc : c • v = p' -ᵥ p
h₁ :
  ∀ (h : HPow.hPow (β := ℕ) ‖c • v‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)
    (hc : c • v = p' -ᵥ p),
    c • v = √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v ∨
      c • v = -(√(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 ∨
    p' -ᵥ p = -(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v)

Tactic:
rw [← hc] 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
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' : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
c : ℝ
h : HPow.hPow (β := ℕ) ‖c • v‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
hc : c • v = p' -ᵥ p
h₁ :
  c • v = √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v ∨
    c • v = -√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v
⊢ c • v = √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v ∨
    c • v = -(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v)

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
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' : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
c : ℝ
h : HPow.hPow (β := ℕ) ‖c • v‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
hc : c • v = p' -ᵥ p
h₁ : HPow.hPow (β := ℕ) c 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ c • v = √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v ∨
    c • v = -√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v

Tactic:
simp_rw [(smul_left_injective ℝ hv0).eq_iff, ← sq_eq_sq_iff_eq_or_eq_neg, Real.sq_sqrt hvp]

Premises used: Real, Function.Injective.eq_iff, Real.sq_sqrt, smul_left_injective, sq_eq_sq_iff_eq_or_eq_neg
-- 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' : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
c : ℝ
h : HPow.hPow (β := ℕ) ‖c • v‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
hc : c • v = p' -ᵥ p
⊢ HPow.hPow (β := ℕ) c 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
simpa [norm_smul, hv1] using h

Premises used: norm_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
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 :
  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'
⊢ 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 [← neg_smul] at h

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
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 :
  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₁ :
  √(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)
h₂ :
  -√(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)
⊢ p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)

Tactic:
rcases h with rfl | rfl

Premises used: 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
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 :
  HPow.hPow (β := ℕ) ‖√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v‖ 2 =
    HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 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)

Tactic:
rw [vadd_mem_inter_orthRadius_iff_norm_sq hr (Submodule.smul_mem _ _ hv)]

Premises used: EuclideanGeometry.Sphere.vadd_mem_inter_orthRadius_iff_norm_sq, Submodule.smul_mem
-- 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 :
  HPow.hPow (β := ℕ) ‖-√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v‖ 2 =
    HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 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)

Tactic:
rw [vadd_mem_inter_orthRadius_iff_norm_sq hr (Submodule.smul_mem _ _ hv)]

Premises used: EuclideanGeometry.Sphere.vadd_mem_inter_orthRadius_iff_norm_sq, Submodule.smul_mem
-- 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
⊢ HPow.hPow (β := ℕ) ‖√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v‖ 2 =
    HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
simp [norm_smul, hv1, hvp]

Premises used: norm_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
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
⊢ HPow.hPow (β := ℕ) ‖-√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v‖ 2 =
    HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
simp [norm_smul, hv1, hvp]

Premises used: norm_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
hv0 : v ≠ 0
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) =
    {√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • ‖v‖⁻¹ • v +ᵥ p,
      -√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • ‖v‖⁻¹ • v +ᵥ p}

Tactic:
inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one hp hpc (v := ‖v‖⁻¹ • v)
      (Submodule.smul_mem _ _ hv) ?_

Premises used: EuclideanGeometry.Sphere.inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one, Submodule.smul_mem
-- 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
hv0 : v ≠ 0
h :
  (√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • v +ᵥ p =
    √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • ‖v‖⁻¹ • v +ᵥ p
h₁ :
  Eq (α := Set P) {-(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • v +ᵥ p}
    {-√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • ‖v‖⁻¹ • v +ᵥ p}
inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one : ‖‖v‖⁻¹ • v‖ = 1
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) =
    {(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • v +ᵥ p,
      -(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • v +ᵥ p}

Tactic:
convert!
    inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one hp hpc (v := ‖v‖⁻¹ • v)
      (Submodule.smul_mem _ _ hv) ?_ using 2

Premises used: EuclideanGeometry.Sphere.inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one, Submodule.smul_mem
-- 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
hv0 : v ≠ 0
⊢ (√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • v +ᵥ p =
    √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • ‖v‖⁻¹ • v +ᵥ p

Tactic:
simp [div_eq_mul_inv, smul_smul]

Premises used: smul_smul, div_eq_mul_inv