awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ 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
have inl : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
  Module.finrank ℝ V = 1 ∧ ¬p = s.center ∨ Subsingleton V
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬p = s.center ∨ Subsingleton V
have 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
Tactic: obtain rfl | hp := eq_or_ne p s.center
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬p = s.center ∨ Subsingleton V
have 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
Tactic: obtain rfl | hp := eq_or_ne p s.center
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius s.center) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V
have 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
Tactic: rcases subsingleton_or_nontrivial V with hs | hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius s.center) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V
have 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
Tactic: rcases subsingleton_or_nontrivial V with hs | hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (hypothesis)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius s.center) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V
have hs' : Subsingleton P
Tactic: have hs' := (AddTorsor.subsingleton_iff V P).1 hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius s.center) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V
have inl : (Metric.sphere s.center s.radius).Nonempty
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ (Metric.sphere s.center s.radius).Nonempty
have inl : ∀ (v : V) (hv : ‖v‖ = s.radius), (Metric.sphere s.center s.radius).Nonempty
Tactic: obtain ⟨v, hv⟩ := exists_norm_eq V (dist_nonneg.trans_lt h).le
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬p = s.center ∨ Subsingleton V
have inl : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
Tactic: simp only [hp, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
have 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
Tactic: rcases eq_or_ne (ℝ ∙ (p -ᵥ s.center)) ⊤ with hb | hb
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
have 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
Tactic: rcases eq_or_ne (ℝ ∙ (p -ᵥ s.center)) ⊤ with hb | hb
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (hypothesis)
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)) ⊤
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
have hb'₁ : ∀ (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
Tactic: rw [Submodule.span_singleton_eq_top_iff] at hb'
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (hypothesis)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
have hf : Module.finrank ℝ V = 1
Tactic: have hf := finrank_eq_one_iff'.2 ⟨p -ᵥ s.center, vsub_ne_zero.2 hp, hb'⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
have rw : ¬Subsingleton P
Tactic: rw [AddTorsor.subsingleton_iff V P]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (hypothesis)
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)) ⊤
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
have hn : ¬Subsingleton V
Tactic: have hn : ¬Subsingleton V := by
          rw [AddTorsor.subsingleton_iff V P]
          intro hs
          simp [Subsingleton.elim p s.center] at hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ False
have apply : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
Tactic: apply hb
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
have rw : ∀ (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
Tactic: rw [Submodule.span_singleton_eq_top_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (hypothesis)
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), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
have hf₁ : ∃ (v : V), v ≠ 0 ∧ ∀ (w : V), ∃ (c : ℝ), c • v = w
Tactic: rw [finrank_eq_one_iff'] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ ∀ (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
have obtain : ∀ (v : V) (hv0 : v ≠ 0) (hv : ∀ (w : V), ∃ (c : ℝ), c • v = w) (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
Tactic: obtain ⟨v, hv0, hv⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ ∀ (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
have obtain : ∀ (c : ℝ) (hc : c • v = p -ᵥ s.center) (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
Tactic: obtain ⟨c, hc⟩ := hv (p -ᵥ s.center)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (hypothesis)
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
⊢ False
have hc₁ : p = s.center
Tactic: rw [zero_smul, eq_comm, vsub_eq_zero_iff_eq] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (hypothesis)
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
⊢ ∀ (v : V), ∃ (r : ℝ), r • (p -ᵥ s.center) = v
have hc0 : 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ ∃ (r : ℝ), r • (p -ᵥ s.center) = v'
have obtain : ∀ (c' : ℝ), ∃ (r : ℝ), r • (p -ᵥ s.center) = c' • v
Tactic: obtain ⟨c', rfl⟩ := hv v'
Cleared hypotheses: v'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
have refine : (c' / c) • (p -ᵥ s.center) = c' • v
Tactic: refine ⟨c' / c, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (hypothesis)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
have hnf : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
have inl : (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).Nonempty
Tactic: simp only [hnf, hn, or_self, iff_false, ← Set.nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (hypothesis)
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
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).Nonempty
have hb₁ : ¬Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ⊥
Tactic: rw [ne_eq, ← Submodule.orthogonal_eq_bot_iff] at hb
Cleared hypotheses: hb, hn, hnf
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).Nonempty
have 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
Tactic: obtain ⟨v, hvm, hv0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hb
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
have 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)
Tactic: refine ⟨(√(s.radius ^ 2 - (dist p s.center) ^ 2) / ‖v‖) • v +ᵥ p, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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 (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • v +ᵥ p ∈
    Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
have 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
Tactic: rw [vadd_mem_inter_orthRadius_iff_norm_sq (dist_nonneg.trans_lt h).le
          (Submodule.smul_mem _ _ hvm)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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) / ‖v‖) • v‖ 2 =
    HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have 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
Tactic: rw [norm_smul, norm_div, norm_norm, div_mul_cancel₀ _ (norm_ne_zero_iff.2 hv0)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
have 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
Tactic: simp only [Real.norm_eq_abs, sq_abs]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
have inl : 0 ≤ HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: refine Real.sq_sqrt ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ 0 ≤ HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have inl : dist p s.center ≤ |s.radius|
Tactic: rw [sub_nonneg, sq_le_sq, abs_of_nonneg dist_nonneg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ 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
have 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
Tactic: rw [inter_orthRadius_eq_singleton_of_dist_eq_radius h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.OrthRadius (goal)
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
⊢ 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
have inr : 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]