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
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
⊢ 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)
have 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
Tactic: rw [← neg_smul]
-- 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' : 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
⊢ 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
have h₁ : HPow.hPow (β := ℕ) c 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: simp_rw [(smul_left_injective ℝ hv0).eq_iff, ← sq_eq_sq_iff_eq_or_eq_neg, Real.sq_sqrt hvp]
-- 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 :
  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)
have 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'
Tactic: rw [← neg_smul] at h
Cleared hypotheses: 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 :
  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)
have 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)
Tactic: rcases h with rfl | rfl
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
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)
⊢ p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
have 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)
Tactic: rcases h with rfl | rfl
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
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 (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) • v +ᵥ p ∈
    Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
have 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
Tactic: rw [vadd_mem_inter_orthRadius_iff_norm_sq hr (Submodule.smul_mem _ _ hv)]
-- 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
⊢ -√(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)
have 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
Tactic: rw [vadd_mem_inter_orthRadius_iff_norm_sq hr (Submodule.smul_mem _ _ hv)]
-- 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
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}
have 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
Tactic: convert!
    inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one hp hpc (v := ‖v‖⁻¹ • v)
      (Submodule.smul_mem _ _ hv) ?_ using 2
-- 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
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
⊢ 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}
have 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}
Tactic: convert!
    inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one hp hpc (v := ‖v‖⁻¹ • v)
      (Submodule.smul_mem _ _ hv) ?_ using 2
-- 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
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}
⊢ 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}
have inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one : ‖‖v‖⁻¹ • v‖ = 1
Tactic: convert!
    inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one hp hpc (v := ‖v‖⁻¹ • v)
      (Submodule.smul_mem _ _ hv) ?_ using 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
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard = 2
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
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)).ncard = 2
have hf₁ : ∃ (v : ↥(direction (s.orthRadius p))), v ≠ 0 ∧ ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
Tactic: simp only [hf2.out, Nat.reduceEqDiff, 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
hf : ∃ (v : ↥(direction (s.orthRadius p))), v ≠ 0 ∧ ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard = 2
have obtain : ∀ (v : ↥(direction (s.orthRadius p))) (hv0 : v ≠ 0) (hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w),
  (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard = 2
Tactic: obtain ⟨v, hv0, hv⟩ := 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 : ↥(direction (s.orthRadius p))
hv0 : v ≠ 0
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard = 2
have hv0₁ : (↑v : V) ≠ 0
Tactic: replace hv0 : (v : V) ≠ 0 := by simpa using hv0
Cleared hypotheses: 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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard = 2
have rw : (√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • (↑v : V) +ᵥ p ≠
  -((√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • (↑v : V)) +ᵥ p
Tactic: rw [inter_orthRadius_eq_of_dist_le_radius hp.le hpc (by simpa using v.property) hv0,
    Submodule.norm_coe, neg_smul, Set.ncard_pair]
-- 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 : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
⊢ (√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • (↑v : V) +ᵥ p ≠
    -((√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • (↑v : V)) +ᵥ p
have rw : ¬√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) = 0
Tactic: rw [ne_eq, vadd_right_cancel_iff, ← add_eq_zero_iff_eq_neg, ← two_smul ℝ,
    smul_eq_zero_iff_right two_ne_zero, smul_eq_zero_iff_left hv0, div_eq_iff, zero_mul]
-- 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 : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
rw : ¬√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) = 0
⊢ (√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • (↑v : V) +ᵥ p ≠
    -((√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) / ‖v‖) • (↑v : V)) +ᵥ p
have rw₁ : ‖v‖ ≠ 0
Tactic: rw [ne_eq, vadd_right_cancel_iff, ← add_eq_zero_iff_eq_neg, ← two_smul ℝ,
    smul_eq_zero_iff_right two_ne_zero, smul_eq_zero_iff_left hv0, div_eq_iff, zero_mul]
-- 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 : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
⊢ 0 < √(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)
have rw : dist p s.center < |s.radius|
Tactic: rw [Real.sqrt_pos, sub_pos, sq_lt_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 : ↥(direction (s.orthRadius p))
hv : ∀ (w : ↥(direction (s.orthRadius p))), ∃ (c : ℝ), c • v = w
hv0 : (↑v : V) ≠ 0
⊢ ¬√(HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2) = 0
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 [Real.sqrt_pos, sub_pos, sq_lt_sq, abs_of_nonneg dist_nonneg]
      exact lt_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
hpc : p ≠ s.center
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
have inl : ∀ (h : dist p s.center < s.radius), (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
Tactic: rcases lt_trichotomy (dist p s.center) s.radius with h | 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
hpc : p ≠ s.center
inl : ∀ (h : dist p s.center < s.radius), (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
have inr : ∀ (h : dist p s.center = s.radius), (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
Tactic: rcases lt_trichotomy (dist p s.center) s.radius with h | 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
hpc : p ≠ s.center
inl : ∀ (h : dist p s.center < s.radius), (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
inr : ∀ (h : dist p s.center = s.radius), (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
⊢ (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
have inr₁ : ∀ (h : s.radius < dist p s.center), (Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)).ncard ≤ 2
Tactic: rcases lt_trichotomy (dist p s.center) s.radius with h | h | h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₁ : ∃ (k : ℝ), x = k • y
h₃ : ‖z - y‖ = ‖z + y‖
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
have obtain : ∀ (r : ℝ) (hr : x = r • y), ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
Tactic: obtain ⟨r, hr⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
⊢ ⟪z, y⟫ = 0
have rwa : angle z y = π / 2
Tactic: rwa [inner_eq_zero_iff_angle_eq_pi_div_two, ← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two,
      eq_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
rwa : angle z y = π / 2
⊢ ⟪z, y⟫ = 0
have rwa₁ : ‖z + y‖ = ‖z - y‖
Tactic: rwa [inner_eq_zero_iff_angle_eq_pi_div_two, ← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two,
      eq_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
⊢ ‖x - y‖ * ‖x + y‖ = |HPow.hPow (β := ℕ) ‖z + y‖ 2 - HPow.hPow (β := ℕ) ‖z - x‖ 2|
have hzy : ⟪z, y⟫ = 0
Tactic: have hzy : ⟪z, y⟫ = 0 := by
    rwa [inner_eq_zero_iff_angle_eq_pi_div_two, ← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two,
      eq_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
⊢ ⟪z, x⟫ = 0
have rw : ⟪z, r • y⟫ = 0
Tactic: rw [hr, inner_smul_right, hzy, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
rw : ⟪z, r • y⟫ = 0
⊢ ⟪z, x⟫ = 0
have rw₁ : r * ⟪z, y⟫ = 0
Tactic: rw [hr, inner_smul_right, hzy, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Power (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
rw : ⟪z, r • y⟫ = 0
rw₁ : r * ⟪z, y⟫ = 0
⊢ ⟪z, x⟫ = 0
have rw₂ : r * 0 = 0
Tactic: rw [hr, inner_smul_right, hzy, mul_zero]