awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hs : Subsingleton V
⊢ s.radius = 0
have hs₁ : Subsingleton P
Tactic: rw [AddTorsor.subsingleton_iff V P] at hs
Cleared hypotheses: 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
p : P
h : dist p s.center = s.radius
hs : Subsingleton P
⊢ s.radius = 0
have h₁ : dist s.center s.center = s.radius
Tactic: rw [Subsingleton.elim p s.center] at h
Cleared hypotheses: h, 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
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
⊢ 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}
have hr : 0 ≤ s.radius
Tactic: have hr : 0 ≤ s.radius := dist_nonneg.trans 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
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
have rw : Ne (α := ℝ) 1 0
Tactic: rw [← norm_ne_zero_iff, hv1]
-- 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
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
⊢ 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}
have hv0 : v ≠ 0
Tactic: have hv0 : v ≠ 0 := by rw [← norm_ne_zero_iff, hv1]; simp
-- 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
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
⊢ 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}
have 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}
Tactic: rw [neg_smul]
-- 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
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
⊢ 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}
have hf : Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p)) + 1 = Module.finrank ℝ V
Tactic: have hf := finrank_orthRadius hpc
-- 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
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
⊢ 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}
have hf₁ : Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ + 1 = Module.finrank ℝ V
Tactic: rw [direction_orthRadius] at hf
Cleared hypotheses: hf
-- 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
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
⊢ 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}
have hf₁ : Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ = 1
Tactic: simp only [hf2.out, Nat.reduceEqDiff] at hf
Cleared hypotheses: hf
-- 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
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
⊢ 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}
have hf₁ : ∀ (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
Cleared hypotheses: hf
-- 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
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
⊢ 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}
have hvc : ∀ (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⟩
-- 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
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
have rw : 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 (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
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
⊢ 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}
have hvp : 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)
-- 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
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
⊢ 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}
have 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'
Tactic: ext 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
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'
have 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'
Tactic: refine ⟨fun h ↦ ?_, fun 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
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'
⊢ 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'
have 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)
Tactic: refine ⟨fun h ↦ ?_, fun 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
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 (γ := 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'
have 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)
Tactic: rw [← vsub_vadd p' p, Set.mem_insert_iff, Set.mem_singleton_iff, vadd_right_cancel_iff,
      vadd_right_cancel_iff]
-- 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
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)
have rw : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p'
Tactic: rw [← direction_orthRadius, vsub_right_mem_direction_iff_mem (s.self_mem_orthRadius 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
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)
⊢ 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)
have h' : 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
-- 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
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)
⊢ 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)
have h₁ : 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
Cleared hypotheses: h, 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
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)
⊢ 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)
have 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)
Tactic: obtain ⟨c, hc⟩ := hvc _ 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
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
⊢ 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)
have 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)
Tactic: rw [← hc] at h ⊢
Cleared hypotheses: h, hc