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
simp_rw :
  mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ ∥ mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₁ :
  Eq (α := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ)) (direction (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ)) ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₂ :
  Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₃ :
  Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center)) ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₄ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₅ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧
      ((↑(mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) : Set P) = ∅ ↔ (↑(mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) : Set P) = ∅) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₆ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧
      (¬(↑(mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) : Set P).Nonempty ↔ ¬(↑(mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) : Set P).Nonempty) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₇ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧ True ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
⊢ s.orthRadius p ∥ s.orthRadius q ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
have simp_rw₈ : (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
Tactic: simp_rw [orthRadius, parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, direction_mk',
    Submodule.orthogonalComplement_eq_orthogonalComplement,
    Submodule.span_singleton_eq_span_singleton, ← coe_eq_bot_iff,
    ← Set.not_nonempty_iff_eq_empty, mk'_nonempty, and_true, ← Units.exists_iff_ne_zero, eq_comm,
    Units.smul_def]
-- 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
simp_rw :
  mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ ∥ mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₁ :
  Eq (α := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ)) (direction (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ)) ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₂ :
  Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₃ :
  Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center)) ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₄ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₅ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧
      ((↑(mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) : Set P) = ∅ ↔ (↑(mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) : Set P) = ∅) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₆ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧
      (¬(↑(mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) : Set P).Nonempty ↔ ¬(↑(mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) : Set P).Nonempty) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₇ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧ True ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₈ : (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
⊢ s.orthRadius p ∥ s.orthRadius q ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
have simp_rw₉ : (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ↔ ∃ (u : ℝˣ), q -ᵥ s.center = (↑u : ℝ) • (p -ᵥ s.center)
Tactic: simp_rw [orthRadius, parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, direction_mk',
    Submodule.orthogonalComplement_eq_orthogonalComplement,
    Submodule.span_singleton_eq_span_singleton, ← coe_eq_bot_iff,
    ← Set.not_nonempty_iff_eq_empty, mk'_nonempty, and_true, ← Units.exists_iff_ne_zero, eq_comm,
    Units.smul_def]
-- 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
simp_rw :
  mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ ∥ mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₁ :
  Eq (α := Submodule ℝ V) (direction (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ)) (direction (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ)) ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₂ :
  Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₃ :
  Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center)) ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₄ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧
      (Eq (α := AffineSubspace ℝ P) (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) ⊥ ↔
        Eq (α := AffineSubspace ℝ P) (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) ⊥) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₅ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧
      ((↑(mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) : Set P) = ∅ ↔ (↑(mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) : Set P) = ∅) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₆ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧
      (¬(↑(mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) : Set P).Nonempty ↔ ¬(↑(mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) : Set P).Nonempty) ↔
    ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₇ :
  (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ∧ True ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₈ : (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
simp_rw₉ : (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ↔ ∃ (u : ℝˣ), q -ᵥ s.center = (↑u : ℝ) • (p -ᵥ s.center)
⊢ s.orthRadius p ∥ s.orthRadius q ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
have simp_rw₁₀ : (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ↔ ∃ (u : ℝˣ), (↑u : ℝ) • (p -ᵥ s.center) = q -ᵥ s.center
Tactic: simp_rw [orthRadius, parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, direction_mk',
    Submodule.orthogonalComplement_eq_orthogonalComplement,
    Submodule.span_singleton_eq_span_singleton, ← coe_eq_bot_iff,
    ← Set.not_nonempty_iff_eq_empty, mk'_nonempty, and_true, ← Units.exists_iff_ne_zero, eq_comm,
    Units.smul_def]
-- 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
⊢ HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
have simp_rw : ‖q -ᵥ s.center‖ * ‖q -ᵥ s.center‖ = ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ + ‖q -ᵥ p‖ * ‖q -ᵥ p‖ ↔
  Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
Tactic: simp_rw [dist_eq_norm_vsub, pow_two]
-- 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
⊢ ‖q -ᵥ s.center‖ * ‖q -ᵥ s.center‖ = ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ + ‖q -ᵥ p‖ * ‖q -ᵥ p‖ ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
have rw : ‖q -ᵥ p + (p -ᵥ s.center)‖ * ‖q -ᵥ p + (p -ᵥ s.center)‖ = ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ + ‖q -ᵥ p‖ * ‖q -ᵥ p‖ ↔
  Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
Tactic: rw [← vsub_add_vsub_cancel q 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
p q : P
⊢ ‖q -ᵥ p + (p -ᵥ s.center)‖ * ‖q -ᵥ p + (p -ᵥ s.center)‖ = ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ + ‖q -ᵥ p‖ * ‖q -ᵥ p‖ ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
have nth_rw : ‖q -ᵥ p + (p -ᵥ s.center)‖ * ‖q -ᵥ p + (p -ᵥ s.center)‖ = ‖q -ᵥ p‖ * ‖q -ᵥ p‖ + ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ ↔
  Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
Tactic: nth_rw 3 [add_comm]
-- 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
⊢ ‖q -ᵥ p + (p -ᵥ s.center)‖ * ‖q -ᵥ p + (p -ᵥ s.center)‖ = ‖q -ᵥ p‖ * ‖q -ᵥ p‖ + ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
have rw : ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0 ↔ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
Tactic: rw [norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, ← mem_orthRadius_iff_inner_left]
-- 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
rw : ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0 ↔ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
⊢ ‖q -ᵥ p + (p -ᵥ s.center)‖ * ‖q -ᵥ p + (p -ᵥ s.center)‖ = ‖q -ᵥ p‖ * ‖q -ᵥ p‖ + ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ ↔
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
have rw₁ : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q ↔
  Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
Tactic: rw [norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, ← mem_orthRadius_iff_inner_left]
-- 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
⊢ q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔
    0 ≤ s.radius ∧
      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
have simp : q ∈ s ∧
    HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ↔
  0 ≤ s.radius ∧
    HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ∧
      HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: simp only [Set.mem_inter_iff, Metric.mem_sphere, mem_coe', SetLike.mem_coe,
    ← dist_sq_eq_iff_mem_orthRadius, ← direction_orthRadius,
    vsub_right_mem_direction_iff_mem (s.self_mem_orthRadius p), ← dist_eq_norm_vsub]
-- 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
⊢ q ∈ s ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 =
        HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 =
          HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ∧
        HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have nth_rw : q ∈ s ∧
    HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ↔
  0 ≤ s.radius ∧
    HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2
Tactic: nth_rw 3 [and_comm]
-- 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
⊢ q ∈ s ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 =
        HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ∧
        HPow.hPow (β := ℕ) (dist q s.center) 2 =
          HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2
have rw : HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2 →
  (q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2)
Tactic: rw [← and_assoc, and_congr_left_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 q : P
h : HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2
⊢ q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have h₁ : HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2
Tactic: rw [← sub_eq_iff_eq_add'] 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
s : Sphere P
p q : P
h : HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2
⊢ q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q p) 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have rw : q ∈ s ↔
  0 ≤ s.radius ∧
    HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
      HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: rw [← 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 q : P
h : HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2
⊢ q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
        HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have inl : ∀ (h0 : 0 ≤ s.radius),
  q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
        HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: rcases le_or_gt 0 s.radius with h0 | h0
-- 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 : HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2
inl :
  ∀ (h0 : 0 ≤ s.radius),
    q ∈ s ↔
      0 ≤ s.radius ∧
        HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
          HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
⊢ q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
        HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have inr : ∀ (h0 : s.radius < 0),
  q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
        HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: rcases le_or_gt 0 s.radius with h0 | h0
-- 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 : HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 = HPow.hPow (β := ℕ) (dist q p) 2
h0 : s.radius < 0
⊢ q ∈ s ↔
    0 ≤ s.radius ∧
      HPow.hPow (β := ℕ) (dist q s.center) 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 =
        HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have inr : q ∉ s
Tactic: simp only [h0.not_ge, sub_left_inj, false_and, iff_false]
-- 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 : 0 ≤ s.radius
⊢ q ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set 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
have rw : 0 ≤ s.radius ∧
    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 ↔
  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: 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
v : V
h : 0 ≤ s.radius
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ v
⊢ v +ᵥ p ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔
    HPow.hPow (β := ℕ) ‖v‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
have rw : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ ((v +ᵥ p) -ᵥ p) ∧
    HPow.hPow (β := ℕ) ‖(v +ᵥ p) -ᵥ p‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2 ↔
  HPow.hPow (β := ℕ) ‖v‖ 2 = HPow.hPow (β := ℕ) s.radius 2 - HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: rw [mem_inter_orthRadius_iff_vsub_mem_and_norm_sq 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
hp : dist p s.center = s.radius
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {p}
have h : ∀ (p' : P), p' ∈ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) ↔ Membership.mem (γ := Set P) {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 : dist p s.center = s.radius
p' : P
⊢ p' ∈ s ∧ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p' ↔ p' = p
have h : p' ∈ s ∧ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p' → p' = p
Tactic: constructor
-- 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 : dist p s.center = s.radius
p' : P
h : p' ∈ s ∧ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p' → p' = p
⊢ p' ∈ s ∧ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p' ↔ p' = p
have h₁ : p' = p → p' ∈ s ∧ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p'
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 : P
hp : dist p s.center = s.radius
p' : P
hp's : p' ∈ s
hp'i : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p'
⊢ p' = p
have h' : HPow.hPow (β := ℕ) (dist p' s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist p' p) 2
Tactic: have h' := dist_sq_eq_of_mem_orthRadius hp'i
-- 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
hp : dist p s.center = s.radius
p' : P
hp's : p' ∈ s
hp'i : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p'
h' : HPow.hPow (β := ℕ) (dist p' s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist p' p) 2
⊢ p' = p
have h'₁ : HPow.hPow (β := ℕ) s.radius 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist p' p) 2
Tactic: rw [hp's, hp] 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
s : Sphere P
p q : P
⊢ Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q} ↔ q = p ∧ dist p s.center = s.radius
have mp : Metric.sphere s.center s.radius ∩ (↑(s.orthRadius p) : Set P) = {q} → q = p ∧ dist p s.center = s.radius
Tactic: constructor