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 q : P
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
hr : HSMul.hSMul (α := ℝ) 0 (p -ᵥ s.center) = q -ᵥ s.center
⊢ p = q ∨ q = s.center
have hr₁ : q = s.center
Tactic: rw [zero_smul, eq_comm, vsub_eq_zero_iff_eq] at hr
Cleared hypotheses: hr
-- 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 : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : ⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0
⊢ p = q ∨ q = s.center
have hp₁ : p = s.center
Tactic: simp only [inner_self_eq_zero, vsub_eq_zero_iff_eq] at hp
Cleared hypotheses: hp
-- 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 : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : p = s.center
⊢ p = q ∨ q = s.center
have hr₁ : q = s.center
Tactic: rw [hp, vsub_self, smul_zero, eq_comm, vsub_eq_zero_iff_eq] at hr
Cleared hypotheses: hr, 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
s : Sphere P
p q : P
h : p = q ∨ q = s.center
⊢ LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
have refine_2 : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius p)
Tactic: rcases h with rfl | rfl
Cleared hypotheses: q, 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 : p = q ∨ q = s.center
refine_2 : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius p)
⊢ LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
have refine_2₁ : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius s.center)
Tactic: rcases h with rfl | rfl
Cleared hypotheses: q, 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
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q) ↔ p = q
have refine : ∀ (h : Eq (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)), p = q
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h ▸ 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 : Eq (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
⊢ p = q
have hpq : p = q ∨ q = s.center
Tactic: have hpq := orthRadius_le_orthRadius_iff.1 h.le
-- 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 : Eq (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
hpq : p = q ∨ q = s.center
⊢ p = q
have hqp : q = p ∨ p = s.center
Tactic: have hqp := orthRadius_le_orthRadius_iff.1 h.symm.le
-- 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
inst_4 : FiniteDimensional ℝ V
s : Sphere P
p : P
hp : p ≠ s.center
⊢ Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p)) + 1 = Module.finrank ℝ V
have rw : 1 + Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ = Module.finrank ℝ V
Tactic: rw [orthRadius, add_comm, direction_mk']
-- 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
inst_4 : FiniteDimensional ℝ V
s : Sphere P
p : P
hp : p ≠ s.center
⊢ 1 + Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ = Module.finrank ℝ V
have h : 1 = Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))
Tactic: convert! (ℝ ∙ (p -ᵥ s.center)).finrank_add_finrank_orthogonal
-- 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
f : P ≃ᵃⁱ[ℝ] P
h : (f : (a : P) → P) s.center = s.center
⊢ map (↑f.toAffineEquiv : P →ᵃ[ℝ] P) (s.orthRadius p) = s.orthRadius ((f : (a : P) → P) p)
have rw : Eq (α := AffineSubspace ℝ P)
  (mk' (((↑f.toAffineEquiv : P →ᵃ[ℝ] P) : (a : P) → P) p)
      (Submodule.map (↑f.toAffineEquiv : P →ᵃ[ℝ] P).linear (ℝ ∙ (p -ᵥ s.center))ᗮ) :
    AffineSubspace ℝ P)
  (mk' ((f : (a : P) → P) p) (ℝ ∙ ((f : (a : P) → P) p -ᵥ s.center))ᗮ : AffineSubspace ℝ P)
Tactic: rw [orthRadius, map_mk', orthRadius]
-- 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
f : P ≃ᵃⁱ[ℝ] P
h : (f : (a : P) → P) s.center = s.center
⊢ Eq (α := AffineSubspace ℝ P)
    (mk' (((↑f.toAffineEquiv : P →ᵃ[ℝ] P) : (a : P) → P) p)
        (Submodule.map (↑f.toAffineEquiv : P →ᵃ[ℝ] P).linear (ℝ ∙ (p -ᵥ s.center))ᗮ) :
      AffineSubspace ℝ P)
    (mk' ((f : (a : P) → P) p) (ℝ ∙ ((f : (a : P) → P) p -ᵥ s.center))ᗮ : AffineSubspace ℝ P)
have h₁ : Real.instRing = NormedRing.toRing →
  Eq.{u_1 + 1} (α := AddCommGroup V) NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup →
    HEq.{u_1 + 1} (α := Module ℝ V) (NormedSpace.toModule : Module ℝ V) (β := Module ℝ V) NormedSpace.toModule →
      (ℝ ∙ ((f : (a : P) → P) p -ᵥ s.center))ᗮ =
        Submodule.map (↑f.toAffineEquiv : P →ᵃ[ℝ] P).linear (ℝ ∙ (p -ᵥ s.center))ᗮ
Tactic: convert! rfl 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
s : Sphere P
p : P
f : P ≃ᵃⁱ[ℝ] P
h : (f : (a : P) → P) s.center = s.center
e_4 : Real.instRing = NormedRing.toRing
e_5 : Eq.{u_1 + 1} (α := AddCommGroup V) NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup
e_6 : HEq.{u_1 + 1} (α := Module ℝ V) (NormedSpace.toModule : Module ℝ V) (β := Module ℝ V) NormedSpace.toModule
⊢ (ℝ ∙ ((f : (a : P) → P) p -ᵥ s.center))ᗮ = Submodule.map (↑f.toAffineEquiv : P →ᵃ[ℝ] P).linear (ℝ ∙ (p -ᵥ s.center))ᗮ
have h₁ : ℝ ∙ ((f : (a : P) → P) p -ᵥ s.center) =
  Submodule.map (↑f.linearIsometryEquiv.toLinearEquiv : V →ₗ[ℝ] V) (ℝ ∙ (p -ᵥ s.center))
Tactic: convert! (Submodule.map_orthogonal_equiv (ℝ ∙ (p -ᵥ s.center)) f.linearIsometryEquiv).symm
-- 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
⊢ s.orthRadius p ∥ s.orthRadius q ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
have simp_rw : mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ ∥ mk' q (ℝ ∙ (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)
⊢ s.orthRadius p ∥ s.orthRadius q ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
have 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)
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)
⊢ s.orthRadius p ∥ s.orthRadius q ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
have 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)
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)
⊢ s.orthRadius p ∥ s.orthRadius q ↔ ∃ (r : ℝ), r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
have 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)
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)
⊢ 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) ∧
    (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)
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)
⊢ 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) ∧
    ((↑(mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) : Set P) = ∅ ↔ (↑(mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) : Set P) = ∅) ↔
  ∃ (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)
⊢ 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) ∧
    (¬(↑(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)
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)
⊢ 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) ∧ True ↔ ∃ (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]