awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
h'' : LE.le (α := Submodule ℝ V) (ℝ ∙ (q -ᵥ s.center))ᗮᗮ (ℝ ∙ (p -ᵥ s.center))ᗮᗮ
⊢ ∃ (a : ℝ), a • (p -ᵥ s.center) = q -ᵥ s.center

Tactic:
simp only [Submodule.orthogonal_orthogonal, Submodule.span_singleton_le_iff_mem,
      Submodule.mem_span_singleton] at h''

Premises used: Submodule.orthogonal_orthogonal, Submodule.mem_span_singleton, Submodule.span_singleton_le_iff_mem
-- 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
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
h'' : ∃ (a : ℝ), a • (p -ᵥ s.center) = q -ᵥ s.center
refine_1 : ∀ (r : ℝ) (hr : r • (p -ᵥ s.center) = q -ᵥ s.center), p = q ∨ q = s.center
⊢ p = q ∨ q = s.center

Tactic:
rcases h'' with ⟨r, hr⟩
-- 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
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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) p

Tactic:
have hp : p ∈ s.orthRadius q := h (s.self_mem_orthRadius p)
-- 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
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 : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) p
⊢ r - r * r = 0 ∨ ⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0

Tactic:
rw [mem_orthRadius_iff_inner_left, ← vsub_sub_vsub_cancel_right p q s.center, ← hr,
      inner_sub_left, real_inner_smul_left, real_inner_smul_right, ← mul_assoc, ← sub_mul,
      mul_eq_zero] at hp

Premises used: mul_assoc, mul_eq_zero, real_inner_smul_right, sub_mul, inner_sub_left, EuclideanGeometry.Sphere.center, vsub_sub_vsub_cancel_right, real_inner_smul_left, EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left
-- 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
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 : r - r * r = 0 ∨ ⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0
refine_1 : ∀ (hp : r - r * r = 0), p = q ∨ q = s.center
refine_1₁ : ∀ (hp : ⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0), p = q ∨ q = s.center
⊢ p = q ∨ q = s.center

Tactic:
rcases hp with hp | hp
-- 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
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 : r - r * r = 0
⊢ 1 * r - r * r = 0

Tactic:
nth_rw 1 [← one_mul r] at hp

Premises used: one_mul
-- 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
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 : 1 * r - r * r = 0
⊢ 1 - r = 0 ∨ r = 0

Tactic:
rw [← sub_mul, mul_eq_zero] at hp

Premises used: mul_eq_zero, sub_mul
-- 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
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 : 1 - r = 0 ∨ r = 0
refine_1 : ∀ (hp : 1 - r = 0), p = q ∨ q = s.center
refine_1₁ : ∀ (hr : HSMul.hSMul (α := ℝ) 0 (p -ᵥ s.center) = q -ᵥ s.center), p = q ∨ q = s.center
⊢ p = q ∨ q = s.center

Tactic:
rcases hp with hp | rfl

Premises used: rfl
-- 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
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 : 1 - r = 0
⊢ 1 = r

Tactic:
rw [sub_eq_zero] at hp

Premises used: sub_eq_zero
-- 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
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 : 1 = r
⊢ p = q

Tactic:
rw [← hp, one_smul, vsub_left_cancel_iff] at hr

Premises used: one_smul, vsub_left_cancel_iff
-- 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
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 : 1 = r
hr₁ : p = q
⊢ 1 = r

Tactic:
rw [← hp, one_smul, vsub_left_cancel_iff] at hr

Premises used: one_smul, vsub_left_cancel_iff
-- 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
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : p = q
hp : 1 = r
⊢ p = q ∨ q = s.center

Tactic:
.inl hr

Premises used: Or.inl
-- 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
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : p = q
hp : 1 = r
⊢ p = q ∨ q = s.center

Tactic:
exact .inl hr
-- 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
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
⊢ q = s.center

Tactic:
rw [zero_smul, eq_comm, vsub_eq_zero_iff_eq] at hr

Premises used: vsub_eq_zero_iff_eq, eq_comm, zero_smul
-- 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
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
hr : q = s.center
⊢ p = q ∨ q = s.center

Tactic:
.inr hr

Premises used: Or.inr
-- 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
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
hr : q = s.center
⊢ p = q ∨ q = s.center

Tactic:
exact .inr hr
-- 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
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 = s.center

Tactic:
simp only [inner_self_eq_zero, vsub_eq_zero_iff_eq] at hp

Premises used: vsub_eq_zero_iff_eq, inner_self_eq_zero
-- 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
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
⊢ q = s.center

Tactic:
rw [hp, vsub_self, smul_zero, eq_comm, vsub_eq_zero_iff_eq] at hr

Premises used: vsub_eq_zero_iff_eq, smul_zero, eq_comm, vsub_self
-- 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
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
hr₁ : q = s.center
⊢ p = s.center

Tactic:
rw [hp, vsub_self, smul_zero, eq_comm, vsub_eq_zero_iff_eq] at hr

Premises used: vsub_eq_zero_iff_eq, smul_zero, eq_comm, vsub_self
-- 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
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : q = s.center
hp : p = s.center
⊢ p = q ∨ q = s.center

Tactic:
.inr hr

Premises used: Or.inr
-- 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
h : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
h' : LE.le (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : q = s.center
hp : p = s.center
⊢ p = q ∨ q = s.center

Tactic:
exact .inr hr
-- 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
h : p = q ∨ q = s.center
refine_2 : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius p)
refine_2₁ : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius s.center)
⊢ LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)

Tactic:
rcases h with rfl | rfl

Premises used: rfl
-- 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 : P
⊢ LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius p)

Tactic:
simp
-- 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 : P
⊢ LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius s.center)

Tactic:
simp
-- 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
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q) ↔ p = q

Tactic:
⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩

Premises used: Eq.rec, Iff.intro, rfl
-- 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
refine : ∀ (h : Eq (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)), p = q
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q) ↔ p = q

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩
-- 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
h : Eq (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
⊢ p = q ∨ q = s.center

Tactic:
have hpq := orthRadius_le_orthRadius_iff.1 h.le
-- 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
h : Eq (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
hpq : p = q ∨ q = s.center
⊢ q = p ∨ p = s.center

Tactic:
have hqp := orthRadius_le_orthRadius_iff.1 h.symm.le
-- 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
h : Eq (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
hpq : p = q ∨ q = s.center
hqp : q = p ∨ p = s.center
⊢ p = q

Tactic:
grind
-- 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
⊢ Injective (β := AffineSubspace ℝ P) s.orthRadius

Tactic:
fun _ _ ↦ orthRadius_eq_orthRadius_iff.1

Premises used: EuclideanGeometry.Sphere.orthRadius_eq_orthRadius_iff, Iff.mp, Function.Injective
-- 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
inst_4 : FiniteDimensional ℝ V
s : Sphere P
p : P
hp : p ≠ s.center
rw : 1 + Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ = Module.finrank ℝ V
⊢ Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p)) + 1 = Module.finrank ℝ V

Tactic:
rw [orthRadius, add_comm, direction_mk']

Premises used: add_comm, EuclideanGeometry.Sphere.orthRadius, AffineSubspace.direction_mk'
-- 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
inst_4 : FiniteDimensional ℝ V
s : Sphere P
p : P
hp : p ≠ s.center
⊢ Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center)) + Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ =
    Module.finrank ℝ V

Tactic:
(ℝ ∙ (p -ᵥ s.center)).finrank_add_finrank_orthogonal

Premises used: Real, VSub.vsub, EuclideanGeometry.Sphere.center, Submodule.span, Submodule.finrank_add_finrank_orthogonal, Singleton.singleton
-- 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
inst_4 : FiniteDimensional ℝ V
s : Sphere P
p : P
hp : p ≠ s.center
h : 1 = Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))
⊢ 1 + Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ = Module.finrank ℝ V

Tactic:
convert! (ℝ ∙ (p -ᵥ s.center)).finrank_add_finrank_orthogonal

Premises used: Real, VSub.vsub, EuclideanGeometry.Sphere.center, Submodule.span, Submodule.finrank_add_finrank_orthogonal, Singleton.singleton
-- 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
inst_4 : FiniteDimensional ℝ V
s : Sphere P
p : P
hp : p ≠ s.center
⊢ 1 = Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))

Tactic:
(finrank_span_singleton (vsub_ne_zero.2 hp)).symm

Premises used: Iff.mpr, Set.Mem, vsub_ne_zero, setOf, finrank_span_singleton, Eq.symm
-- 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
inst_4 : FiniteDimensional ℝ V
s : Sphere P
p : P
hp : p ≠ s.center
⊢ 1 = Module.finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.center))

Tactic:
exact (finrank_span_singleton (vsub_ne_zero.2 hp)).symm

Premises used: Iff.mpr, vsub_ne_zero, finrank_span_singleton, Eq.symm
-- 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 : P
f : P ≃ᵃⁱ[ℝ] P
h : (f : (a : P) → P) s.center = s.center
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)
⊢ map (↑f.toAffineEquiv : P →ᵃ[ℝ] P) (s.orthRadius p) = s.orthRadius ((f : (a : P) → P) p)

Tactic:
rw [orthRadius, map_mk', orthRadius]

Premises used: AffineSubspace.map_mk', EuclideanGeometry.Sphere.orthRadius
-- 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 : 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.toAffineEquiv : P →ᵃ[ℝ] P) : (a : P) → P) p)
        (Submodule.map (↑f.toAffineEquiv : P →ᵃ[ℝ] P).linear (ℝ ∙ (p -ᵥ s.center))ᗮ) :
      AffineSubspace ℝ P)

Tactic:
rfl

Premises used: rfl
-- 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 : P
f : P ≃ᵃⁱ[ℝ] P
h : (f : (a : P) → P) s.center = s.center
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))ᗮ
⊢ 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:
convert! rfl using 2

Premises used: rfl
-- 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 : 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
⊢ (Submodule.map (↑f.linearIsometryEquiv.toLinearEquiv : V →ₗ[ℝ] V) (ℝ ∙ (p -ᵥ s.center)))ᗮ =
    Submodule.map (↑f.linearIsometryEquiv.toLinearEquiv : V →ₗ[ℝ] V) (ℝ ∙ (p -ᵥ s.center))ᗮ

Tactic:
(Submodule.map_orthogonal_equiv (ℝ ∙ (p -ᵥ s.center)) f.linearIsometryEquiv).symm

Premises used: Real, AffineIsometryEquiv.linearIsometryEquiv, Submodule.map_orthogonal_equiv, VSub.vsub, EuclideanGeometry.Sphere.center, Submodule.span, Singleton.singleton, Eq.symm
-- 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 : 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
h₁ :
  ℝ ∙ ((f : (a : P) → P) p -ᵥ s.center) =
    Submodule.map (↑f.linearIsometryEquiv.toLinearEquiv : V →ₗ[ℝ] V) (ℝ ∙ (p -ᵥ s.center))
⊢ (ℝ ∙ ((f : (a : P) → P) p -ᵥ s.center))ᗮ = Submodule.map (↑f.toAffineEquiv : P →ᵃ[ℝ] P).linear (ℝ ∙ (p -ᵥ s.center))ᗮ

Tactic:
convert! (Submodule.map_orthogonal_equiv (ℝ ∙ (p -ᵥ s.center)) f.linearIsometryEquiv).symm

Premises used: Real, AffineIsometryEquiv.linearIsometryEquiv, Submodule.map_orthogonal_equiv, VSub.vsub, EuclideanGeometry.Sphere.center, Submodule.span, Singleton.singleton, Eq.symm
-- 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 : 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.linearIsometryEquiv.toLinearEquiv : V →ₗ[ℝ] V) (ℝ ∙ (p -ᵥ s.center))

Tactic:
simp [Submodule.map_span, Set.image_singleton, h]

Premises used: Set.image_singleton, Submodule.map_span
-- 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
⊢ LE.le (α := Submodule ℝ V) (direction (s.orthRadius p)) (direction (s.orthRadius q)) ↔
    ∃ (r : ℝ), q -ᵥ s.center = r • (p -ᵥ s.center)

Tactic:
simp [Submodule.orthogonal_le_orthogonal_iff, Submodule.mem_span_singleton, eq_comm]

Premises used: Submodule.mem_span_singleton, eq_comm, Submodule.orthogonal_le_orthogonal_iff