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

Tactic:
rcases subsingleton_or_nontrivial V with hs | hs

Premises used: subsingleton_or_nontrivial
-- 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
h : dist s.center s.center < s.radius
hs : Subsingleton V
⊢ Subsingleton P

Tactic:
have hs' := (AddTorsor.subsingleton_iff V P).1 hs
-- 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
h : dist s.center s.center < s.radius
hs : Subsingleton V
hs' : Subsingleton P
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius s.center) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V

Tactic:
simp [hs, Metric.sphere_eq_empty_of_subsingleton (dist_nonneg.trans_lt h).ne']

Premises used: dist_nonneg, LT.lt.ne', Metric.sphere_eq_empty_of_subsingleton, LE.le.trans_lt
-- 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
h : dist s.center s.center < s.radius
hs : Nontrivial V
inl : (Metric.sphere s.center s.radius).Nonempty
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius s.center) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V

Tactic:
simp only [orthRadius_center, top_coe, Set.inter_univ, not_true_eq_false, and_false,
          not_subsingleton_iff_nontrivial.2 hs, or_self, iff_false, ← Set.nonempty_iff_ne_empty]

Premises used: Iff.mpr, iff_false, Set.inter_univ, EuclideanGeometry.Sphere.orthRadius_center, not_true_eq_false, AffineSubspace.top_coe, Set.nonempty_iff_ne_empty, or_self, and_false, not_subsingleton_iff_nontrivial
-- 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
h : dist s.center s.center < s.radius
hs : Nontrivial V
inl : ∀ (v : V) (hv : ‖v‖ = s.radius), (Metric.sphere s.center s.radius).Nonempty
⊢ (Metric.sphere s.center s.radius).Nonempty

Tactic:
obtain ⟨v, hv⟩ := exists_norm_eq V (dist_nonneg.trans_lt h).le

Premises used: dist_nonneg, exists_norm_eq, LT.lt.le, LE.le.trans_lt
-- 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
h : dist s.center s.center < s.radius
hs : Nontrivial V
v : V
hv : ‖v‖ = s.radius
⊢ v +ᵥ s.center ∈ Metric.sphere s.center s.radius

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
h : dist s.center s.center < s.radius
hs : Nontrivial V
v : V
hv : ‖v‖ = s.radius
⊢ (Metric.sphere s.center s.radius).Nonempty

Tactic:
exact ⟨v +ᵥ s.center, by 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
h : dist p s.center < s.radius
hp : p ≠ s.center
inl : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬p = s.center ∨ Subsingleton V

Tactic:
simp only [hp, not_false_eq_true, and_true]

Premises used: and_true, not_false_eq_true
-- 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
inl :
  ∀ (hb : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤),
    Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
inl₁ :
  ∀ (hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤),
    Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V

Tactic:
rcases eq_or_ne (ℝ ∙ (p -ᵥ s.center)) ⊤ with hb | hb

Premises used: Real, VSub.vsub, EuclideanGeometry.Sphere.center, Submodule.span, eq_or_ne, Top.top, Singleton.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 : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤

Tactic:
have hb' := hb
-- 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 hb' : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
⊢ ∀ (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v

Tactic:
rw [Submodule.span_singleton_eq_top_iff] at hb'

Premises used: Submodule.span_singleton_eq_top_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
hp : p ≠ s.center
hb : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hb' : ∀ (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
⊢ Module.finrank ℝ V = 1

Tactic:
have hf := finrank_eq_one_iff'.2 ⟨p -ᵥ s.center, vsub_ne_zero.2 hp, hb'⟩
-- 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)) ⊤
hb' : ∀ (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
hf : Module.finrank ℝ V = 1
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V

Tactic:
simpa [hf] using inter_orthRadius_eq_empty_of_finrank_eq_one hp h.ne

Premises used: EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_of_finrank_eq_one, LT.lt.ne
-- 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 : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
rw : ¬Subsingleton P
⊢ ¬Subsingleton V

Tactic:
rw [AddTorsor.subsingleton_iff V P]

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
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hs : Subsingleton P
⊢ False

Tactic:
simp [Subsingleton.elim p s.center] at hp

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
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
⊢ ¬Subsingleton V

Tactic:
have hn : ¬Subsingleton V := by
          rw [AddTorsor.subsingleton_iff V P]
          intro hs
          simp [Subsingleton.elim p s.center] at 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
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
hf : Module.finrank ℝ V = 1
apply : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
⊢ False

Tactic:
apply hb
-- 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 : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
hf : Module.finrank ℝ V = 1
rw : ∀ (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤

Tactic:
rw [Submodule.span_singleton_eq_top_iff]

Premises used: Submodule.span_singleton_eq_top_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
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
hf : Module.finrank ℝ V = 1
⊢ ∃ (v : V), v ≠ 0 ∧ ∀ (w : V), ∃ (c : ℝ), c • v = w

Tactic:
rw [finrank_eq_one_iff'] at hf

Premises used: finrank_eq_one_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
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
hf : ∃ (v : V), v ≠ 0 ∧ ∀ (w : V), ∃ (c : ℝ), c • v = w
obtain : ∀ (v : V) (hv0 : v ≠ 0) (hv : ∀ (w : V), ∃ (c : ℝ), c • v = w) (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
⊢ ∀ (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v

Tactic:
obtain ⟨v, hv0, hv⟩ := 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
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ (c : ℝ), c • v = w
obtain : ∀ (c : ℝ) (hc : c • v = p -ᵥ s.center) (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
⊢ ∀ (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v

Tactic:
obtain ⟨c, hc⟩ := hv (p -ᵥ s.center)

Premises used: VSub.vsub, 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 : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ (c : ℝ), c • v = w
hc : HSMul.hSMul (α := ℝ) 0 v = p -ᵥ s.center
⊢ p = s.center

Tactic:
rw [zero_smul, eq_comm, vsub_eq_zero_iff_eq] at hc

Premises used: vsub_eq_zero_iff_eq, eq_comm, zero_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
s : Sphere P
p : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ (c : ℝ), c • v = w
hc : p = s.center
⊢ False

Tactic:
simp [hc] at 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
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ (c : ℝ), c • v = w
c : ℝ
hc : c • v = p -ᵥ s.center
⊢ c ≠ 0

Tactic:
have hc0 : c ≠ 0 := by
            rintro rfl
            rw [zero_smul, eq_comm, vsub_eq_zero_iff_eq] at hc
            simp [hc] at 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
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ (c : ℝ), c • v = w
c : ℝ
hc : c • v = p -ᵥ s.center
hc0 : c ≠ 0
v' : V
obtain : ∀ (c' : ℝ), ∃ (r : ℝ), r • (p -ᵥ s.center) = c' • v
⊢ ∃ (r : ℝ), r • (p -ᵥ s.center) = v'

Tactic:
obtain ⟨c', rfl⟩ := hv v'

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
s : Sphere P
p : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ (c : ℝ), c • v = w
c : ℝ
hc : c • v = p -ᵥ s.center
hc0 : c ≠ 0
c' : ℝ
⊢ ∃ (r : ℝ), r • (p -ᵥ s.center) = c' • v

Tactic:
⟨c' / c, ?_⟩

Premises used: HDiv.hDiv, Exists.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 : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ (c : ℝ), c • v = w
c : ℝ
hc : c • v = p -ᵥ s.center
hc0 : c ≠ 0
c' : ℝ
refine : (c' / c) • (p -ᵥ s.center) = c' • v
⊢ ∃ (r : ℝ), r • (p -ᵥ s.center) = c' • v

Tactic:
refine ⟨c' / c, ?_⟩
-- 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 : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ (c : ℝ), c • v = w
c : ℝ
hc : c • v = p -ᵥ s.center
hc0 : c ≠ 0
c' : ℝ
⊢ (c' / c) • (p -ᵥ s.center) = c' • v

Tactic:
simp [← hc, smul_smul, hc0]

Premises used: smul_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
s : Sphere P
p : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
⊢ Module.finrank ℝ V ≠ 1

Tactic:
have hnf : Module.finrank ℝ V ≠ 1 := by
          intro hf
          apply hb
          rw [Submodule.span_singleton_eq_top_iff]
          rw [finrank_eq_one_iff'] at hf
          obtain ⟨v, hv0, hv⟩ := hf
          obtain ⟨c, hc⟩ := hv (p -ᵥ s.center)
          have hc0 : c ≠ 0 := by
            rintro rfl
            rw [zero_smul, eq_comm, vsub_eq_zero_iff_eq] at hc
            simp [hc] at hp
          intro v'
          obtain ⟨c', rfl⟩ := hv v'
          refine ⟨c' / c, ?_⟩
          simp [← hc, smul_smul, hc0]
-- 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 : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
inl : (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).Nonempty
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V

Tactic:
simp only [hnf, hn, or_self, iff_false, ← Set.nonempty_iff_ne_empty]

Premises used: iff_false, Set.nonempty_iff_ne_empty, or_self
-- 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 : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
⊢ ¬Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ⊥

Tactic:
rw [ne_eq, ← Submodule.orthogonal_eq_bot_iff] at hb

Premises used: Submodule.orthogonal_eq_bot_iff, ne_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 : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
hb₁ : ¬Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ⊥
⊢ ¬Subsingleton V

Tactic:
rw [ne_eq, ← Submodule.orthogonal_eq_bot_iff] at hb

Premises used: Submodule.orthogonal_eq_bot_iff, ne_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 : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : Ne (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
hb₁ : ¬Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ⊥
hn₁ : ¬Subsingleton V
⊢ Module.finrank ℝ V ≠ 1

Tactic:
rw [ne_eq, ← Submodule.orthogonal_eq_bot_iff] at hb

Premises used: Submodule.orthogonal_eq_bot_iff, ne_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 : 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
inl :
  ∀ (v : V) (hvm : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v) (hv0 : v ≠ 0),
    (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).Nonempty
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).Nonempty

Tactic:
obtain ⟨v, hvm, hv0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hb

Premises used: Submodule.exists_mem_ne_zero_of_ne_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
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
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).Nonempty

Tactic:
⟨(√(s.radius ^ 2 - (dist p s.center) ^ 2) / ‖v‖) • v +ᵥ p, ?_⟩

Premises used: Norm.norm, HSub.hSub, HDiv.hDiv, HVAdd.hVAdd, EuclideanGeometry.Sphere.center, Set.Nonempty, HPow.hPow, Exists.intro, Real.sqrt, HSMul.hSMul, Dist.dist, 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 : 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 :
  (√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • v +ᵥ p ∈
    Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).Nonempty

Tactic:
refine ⟨(√(s.radius ^ 2 - (dist p s.center) ^ 2) / ‖v‖) • v +ᵥ 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
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 :
  HPow.hPow (β := ℕ) ‖(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • 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‖) • v +ᵥ p ∈
    Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)

Tactic:
rw [vadd_mem_inter_orthRadius_iff_norm_sq (dist_nonneg.trans_lt h).le
          (Submodule.smul_mem _ _ hvm)]

Premises used: EuclideanGeometry.Sphere.vadd_mem_inter_orthRadius_iff_norm_sq, dist_nonneg, LT.lt.le, LE.le.trans_lt, 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
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 :
  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
⊢ HPow.hPow (β := ℕ) ‖(√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • v‖ 2 =
    HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2

Tactic:
rw [norm_smul, norm_div, norm_norm, div_mul_cancel₀ _ (norm_ne_zero_iff.2 hv0)]

Premises used: Iff.mpr, div_mul_cancel₀, norm_smul, norm_norm, norm_ne_zero_iff, norm_div
-- 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 :
  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
⊢ 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:
simp only [Real.norm_eq_abs, sq_abs]

Premises used: sq_abs, Real.norm_eq_abs