-- Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius
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)
simp_rw₁₀ : (∃ (z : ℝˣ), z • (p -ᵥ s.center) = q -ᵥ s.center) ↔ ∃ (u : ℝˣ), (↑u : ℝ) • (p -ᵥ s.center) = q -ᵥ s.center
⊢ s.orthRadius p ∥ s.orthRadius q ↔ ∃ (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]

Premises used: and_true, Set.not_nonempty_iff_eq_empty, AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, eq_comm, AffineSubspace.mk'_nonempty, AffineSubspace.coe_eq_bot_iff, Units.smul_def, Units.exists_iff_ne_zero, EuclideanGeometry.Sphere.orthRadius, AffineSubspace.direction_mk', Submodule.span_singleton_eq_span_singleton, Submodule.orthogonalComplement_eq_orthogonalComplement