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 q : P
mp : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q} → q = p ∧ dist p s.center = s.radius
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q} ↔ q = p ∧ dist p s.center = s.radius
have mpr : q = p ∧ dist p s.center = s.radius → Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
Tactic: constructor
-- 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 q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
⊢ q = p ∧ dist p s.center = s.radius
have hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
Tactic: have hq : q ∈ (s ∩ s.orthRadius p : Set P) := h ▸ Set.mem_singleton _
-- 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 q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
⊢ q = p ∧ dist p s.center = s.radius
have h' : ∀ (q' : P), q' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ q' = q
Tactic: have h' (q' : P) : q' ∈ (s ∩ s.orthRadius p : Set P) ↔ q' = q := by simp [h]
-- 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 q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
h' : ∀ (q' : P), q' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ q' = q
⊢ q = p ∧ dist p s.center = s.radius
have hr : 0 ≤ s.radius
Tactic: have hr : 0 ≤ s.radius := radius_nonneg_of_mem hq.1
-- 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 q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
h' : ∀ (q' : P), q' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ q' = q
hr : 0 ≤ s.radius
⊢ q = p ∧ dist p s.center = s.radius
have h'₁ : ∀ (q' : P),
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q' -ᵥ p) ∧
      HPow.hPow (β := ℕ) ‖q' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
    q' = q
Tactic: simp_rw [mem_inter_orthRadius_iff_vsub_mem_and_norm_sq hr] at h'
Cleared hypotheses: h'
-- 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 q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
hr : 0 ≤ s.radius
h' :
  ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
      q' = q
⊢ q = p ∧ dist p s.center = s.radius
have hq' : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
  HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: have hq' := (h' q).2 rfl
-- 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 q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
hr : 0 ≤ s.radius
h' :
  ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
      q' = q
hq' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ q = p ∧ dist p s.center = s.radius
have hq'' : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ((-(q -ᵥ p) +ᵥ p) -ᵥ p) ∧
  HPow.hPow (β := ℕ) ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: have hq'' : (-(q -ᵥ p) +ᵥ p) -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧
        ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 := by
      simpa [-neg_vsub_eq_vsub_rev] using hq'
-- 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 q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
hr : 0 ≤ s.radius
h' :
  ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
      q' = q
hq' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
hq'' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ((-(q -ᵥ p) +ᵥ p) -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ 2 =
      HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ q = p ∧ dist p s.center = s.radius
have hqq : -(q -ᵥ p) +ᵥ p = q
Tactic: have hqq := (h' _).1 hq''
-- 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 q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
hr : 0 ≤ s.radius
h' :
  ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
      q' = q
hq' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
hq'' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ((-(q -ᵥ p) +ᵥ p) -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ 2 =
      HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
hqq : -(q -ᵥ p) +ᵥ p = q
⊢ q = p ∧ dist p s.center = s.radius
have hqq₁ : q = p
Tactic: rw [eq_comm, eq_vadd_iff_vsub_eq, eq_neg_iff_add_eq_zero, ← two_smul ℝ,
      smul_eq_zero_iff_right (by norm_num), vsub_eq_zero_iff_eq] at hqq
Cleared hypotheses: hqq
-- 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 q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
hr : 0 ≤ s.radius
h' :
  ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
      q' = q
hq' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
hq'' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ((-(q -ᵥ p) +ᵥ p) -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ 2 =
      HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
hqq : q = p
⊢ q = p ∧ dist p s.center = s.radius
have mp : dist p s.center = s.radius
Tactic: refine ⟨hqq, ?_⟩
-- 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 q : P
h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P)
hr : 0 ≤ s.radius
h' :
  ∀ (q' : P),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖q' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
      q' = q
hq' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (q -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖q -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
hq'' :
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ((-(q -ᵥ p) +ᵥ p) -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ 2 =
      HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
hqq : q = p
⊢ dist p s.center = s.radius
have mp : ∀ (h : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius q) : Set P) = {q})
  (hq : q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius q) : Set P))
  (h' :
    ∀ (q' : P),
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ (q' -ᵥ q) ∧
          HPow.hPow (β := ℕ) ‖q' -ᵥ q‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2 ↔
        q' = q)
  (hq' :
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ (q -ᵥ q) ∧
      HPow.hPow (β := ℕ) ‖q -ᵥ q‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2)
  (hq'' :
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮ ((-(q -ᵥ q) +ᵥ q) -ᵥ q) ∧
      HPow.hPow (β := ℕ) ‖(-(q -ᵥ q) +ᵥ q) -ᵥ q‖ 2 =
        HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist q s.center) 2),
  dist q s.center = s.radius
Tactic: subst hqq
Cleared hypotheses: p, h, hq, h', hq', hq'', hqq
-- 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
hp : s.radius < dist p s.center
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅
have h : ∀ (p' : P), p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ Membership.mem (γ := Set 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
s : Sphere P
p : P
hp : s.radius < dist p s.center
p' : P
⊢ p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ Membership.mem (γ := Set P) ∅ p'
have h : 0 ≤ s.radius ∧
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) ∧
      HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
  Membership.mem (γ := Set P) ∅ p'
Tactic: rw [mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq]
-- 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
hp : s.radius < dist p s.center
p' : P
⊢ 0 ≤ s.radius ∧
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
    Membership.mem (γ := Set P) ∅ p'
have h : 0 ≤ s.radius →
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) →
    ¬HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: simp only [Set.mem_empty_iff_false, iff_false, not_and]
-- 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
hp : s.radius < dist p s.center
p' : P
hle : 0 ≤ s.radius
h : HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ False
have nlinarith : 0 - HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 +
        (HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 - (HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)) +
      (0 - (s.radius - dist p s.center) * (s.radius - dist p s.center)) +
    2 * (0 - (s.radius - dist p s.center) * (0 - s.radius)) =
  0
Tactic: nlinarith
-- 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
hp : s.radius < dist p s.center
p' : P
hle : 0 ≤ s.radius
h : HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
nlinarith :
  0 - HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 +
          (HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 - (HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)) +
        (0 - (s.radius - dist p s.center) * (s.radius - dist p s.center)) +
      2 * (0 - (s.radius - dist p s.center) * (0 - s.radius)) =
    0
⊢ False
have nlinarith₁ : GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = ∅
have h : ∀ (p' : P), p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ Membership.mem (γ := Set 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
s : Sphere P
p : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
⊢ p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ Membership.mem (γ := Set P) ∅ p'
have h : 0 ≤ s.radius ∧
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) ∧
      HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
  Membership.mem (γ := Set P) ∅ p'
Tactic: rw [mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq]
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
⊢ 0 ≤ s.radius ∧
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) ∧
        HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
    Membership.mem (γ := Set P) ∅ p'
have h : 0 ≤ s.radius →
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p) →
    ¬HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: simp only [Set.mem_empty_iff_false, iff_false, not_and]
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
hpo : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
⊢ ¬HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have this : FiniteDimensional ℝ V
Tactic: have : FiniteDimensional ℝ V := Module.finite_of_finrank_eq_succ 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
s : Sphere P
p : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
hpo : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
this : FiniteDimensional ℝ V
⊢ ¬HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have ha : Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center)) + Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ =
  Module.finrank ℝ V
Tactic: have ha := (ℝ ∙ (p -ᵥ s.center)).finrank_add_finrank_orthogonal
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
hpo : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
this : FiniteDimensional ℝ V
ha :
  Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center)) + Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ =
    Module.finrank ℝ V
⊢ ¬HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have ha₁ : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
Tactic: simp only [finrank_span_singleton (vsub_ne_zero.2 hpc), hf, Nat.add_eq_left,
    Submodule.finrank_eq_zero, Submodule.orthogonal_eq_bot_iff] at ha
Cleared hypotheses: ha
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
hpo : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (p' -ᵥ p)
this : FiniteDimensional ℝ V
ha : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
⊢ ¬HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have hpo₁ : p' = p
Tactic: simp only [ha, Submodule.top_orthogonal_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hpo
Cleared hypotheses: hpo
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hpo : p' = p
⊢ ¬HPow.hPow (β := ℕ) ‖p' -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have h : ¬0 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: simp only [hpo, vsub_self, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
-- 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
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) ⊤
hpo : p' = p
⊢ ¬0 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have h : ¬dist p s.center = s.radius
Tactic: rw [eq_comm, sub_eq_zero, eq_comm, sq_eq_sq₀ dist_nonneg hr]
-- 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
⊢ 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 : ∀ (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
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
s : Sphere P
p : P
inl :
  ∀ (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
⊢ 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 : ∀ (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
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
s : Sphere P
p : P
inl :
  ∀ (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
inr :
  ∀ (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
⊢ 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₁ : ∀ (h : s.radius < dist p s.center),
  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
Tactic: rcases lt_trichotomy (dist p s.center) s.radius with h | h | h