awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
h : s.IsTangent as
hpar : as ∥ s.orthRadius p
hp : p ∈ s
rcases :
  ∀ (q : P) (hqs : q ∈ s) (hqas : q ∈ as) (hqo : as ≤ s.orthRadius q),
    as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)

Tactic:
rcases h with ⟨q, hqs, hqas, hqo⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
⊢ as.direction ≤ direction (s.orthRadius q)

Tactic:
have hd := direction_le hqo
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
hd : as.direction ≤ direction (s.orthRadius q)
⊢ ∃ (r : ℝ), q -ᵥ s.center = r • (p -ᵥ s.center)

Tactic:
rw [hpar.direction_eq, direction_orthRadius_le_iff] at hd

Premises used: AffineSubspace.Parallel.direction_eq, EuclideanGeometry.Sphere.direction_orthRadius_le_iff
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
hd : ∃ (r : ℝ), q -ᵥ s.center = r • (p -ᵥ s.center)
obtain :
  ∀ (r : ℝ) (hr : q -ᵥ s.center = r • (p -ᵥ s.center)),
    as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)

Tactic:
obtain ⟨r, hr⟩ := hd
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
inl :
  ∀ (hrad : s.radius = 0), as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
inr :
  ∀ (hrad : s.radius ≠ 0), as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)

Tactic:
rcases eq_or_ne s.radius 0 with hrad | hrad

Premises used: eq_or_ne, OfNat.ofNat, EuclideanGeometry.Sphere.radius
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius = 0
inl :
  ∀ (hp : p = s.center) (q : P) (hqs : q = s.center) (hqas : q ∈ as) (hqo : as ≤ s.orthRadius q) (r : ℝ)
    (hr : q -ᵥ s.center = r • (p -ᵥ s.center)) (hrad : s.radius = 0),
    as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)

Tactic:
rw [mem_sphere, hrad, dist_eq_zero] at hp hqs

Premises used: EuclideanGeometry.mem_sphere, dist_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p = s.center
q : P
hqs : q = s.center
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius = 0
inl :
  ∀ (hpar : as ∥ ⊤) (hp : p = s.center) (q : P) (hqs : q = s.center) (hqas : q ∈ as) (hqo : as ≤ s.orthRadius q) (r : ℝ)
    (hr : q -ᵥ s.center = r • (p -ᵥ s.center)) (hrad : s.radius = 0),
    as = ⊤ ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) s.center)
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)

Tactic:
rw [hp, orthRadius_center] at hpar ⊢

Premises used: EuclideanGeometry.Sphere.orthRadius_center
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ ⊤
hp : p = s.center
q : P
hqs : q = s.center
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius = 0
inl :
  ∀ (hqo : as ≤ ⊤) (r : ℝ) (hr : q -ᵥ s.center = r • (p -ᵥ s.center)) (hrad : s.radius = 0),
    as = ⊤ ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) s.center)
⊢ as = ⊤ ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) s.center)

Tactic:
rw [hqs, orthRadius_center] at hqo

Premises used: EuclideanGeometry.Sphere.orthRadius_center
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ ⊤
hp : p = s.center
q : P
hqs : q = s.center
hqas : q ∈ as
hqo : as ≤ ⊤
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius = 0
⊢ as = ⊤ ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) s.center)

Tactic:
.inl (eq_of_direction_eq_of_nonempty_of_le hpar.direction_eq ⟨q, hqas⟩ hqo)

Premises used: AffineSubspace.Parallel.direction_eq, Exists.intro, AffineSubspace.eq_of_direction_eq_of_nonempty_of_le, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ ⊤
hp : p = s.center
q : P
hqs : q = s.center
hqas : q ∈ as
hqo : as ≤ ⊤
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius = 0
⊢ as = ⊤ ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) s.center)

Tactic:
exact .inl (eq_of_direction_eq_of_nonempty_of_le hpar.direction_eq ⟨q, hqas⟩ hqo)
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
⊢ as = s.orthRadius q

Tactic:
eq_of_direction_eq_of_nonempty_of_le ?_ ⟨q, hqas⟩ hqo

Premises used: Exists.intro, AffineSubspace.eq_of_direction_eq_of_nonempty_of_le
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
refine : as.direction = direction (s.orthRadius q)
⊢ as = s.orthRadius q

Tactic:
refine eq_of_direction_eq_of_nonempty_of_le ?_ ⟨q, hqas⟩ hqo

Premises used: Exists.intro, AffineSubspace.eq_of_direction_eq_of_nonempty_of_le
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
rw : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ
⊢ as.direction = direction (s.orthRadius q)

Tactic:
rw [hpar.direction_eq, direction_orthRadius, direction_orthRadius]

Premises used: AffineSubspace.Parallel.direction_eq, EuclideanGeometry.Sphere.direction_orthRadius
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
e_K : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center))ᗮ (ℝ ∙ (q -ᵥ s.center))ᗮ

Tactic:
congr 1
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
e_K :
  ∀ (hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 0 (p -ᵥ s.center)),
    Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))
e_K₁ : ∀ (hr0 : r ≠ 0), Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))

Tactic:
rcases eq_or_ne r 0 with rfl | hr0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
hrad : s.radius ≠ 0
hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 0 (p -ᵥ s.center)
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))

Tactic:
simp_all
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hr0 : r ≠ 0
e_K : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ r • (p -ᵥ s.center))
e_K₁ e_K₂ : Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (p -ᵥ s.center))
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (p -ᵥ s.center)) (ℝ ∙ (q -ᵥ s.center))

Tactic:
rw [hr, Submodule.span_singleton_smul_eq hr0.isUnit]

Premises used: Ne.isUnit, Submodule.span_singleton_smul_eq
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
inr :
  ∀ (hpar : s.orthRadius q ∥ s.orthRadius p) (hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q)
    (hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)),
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
      Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p)

Tactic:
obtain rfl : as = s.orthRadius q := by
    refine eq_of_direction_eq_of_nonempty_of_le ?_ ⟨q, hqas⟩ hqo
    rw [hpar.direction_eq, direction_orthRadius, direction_orthRadius]
    congr 1
    rcases eq_or_ne r 0 with rfl | hr0
    · simp_all
    · rw [hr, Submodule.span_singleton_smul_eq hr0.isUnit]

Premises used: EuclideanGeometry.Sphere.orthRadius, rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
inr :
  ∀ (hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 0 (p -ᵥ s.center)),
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
      Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
inr₁ :
  ∀ (hr0 : r ≠ 0),
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
      Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))

Tactic:
rcases eq_or_ne r 0 with rfl | hr0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 0 (p -ᵥ s.center)
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))

Tactic:
simp_all
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr0 : r ≠ 0
rw rw₁ : ‖r • (p -ᵥ s.center)‖ = ‖r • (p -ᵥ s.center)‖
⊢ ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖

Tactic:
rw [hr]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr0 : r ≠ 0
⊢ ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖

Tactic:
have hr' : ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖ := by
      rw [hr]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr0 : r ≠ 0
hr' : ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖
⊢ |r| = 1

Tactic:
simp_rw [norm_smul, Real.norm_eq_abs, ← dist_eq_norm_vsub, mem_sphere.1 hp,
      mem_sphere.1 hqs, right_eq_mul₀ hrad] at hr'

Premises used: norm_smul, EuclideanGeometry.mem_sphere, Iff.mp, dist_eq_norm_vsub, right_eq_mul₀, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr0 : r ≠ 0
hr' : |r| = 1
inr :
  ∀ (hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 1 (p -ᵥ s.center)) (hr0 : Ne (α := ℝ) 1 0) (hr' : Eq (α := ℝ) |1| 1),
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
      Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
inr₁ :
  ∀ (hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center)) (hr0 : Ne (α := ℝ) (-1) 0)
    (hr' : Eq (α := ℝ) |(-1)| 1),
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
      Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))

Tactic:
rcases eq_or_eq_neg_of_abs_eq hr' with rfl | rfl

Premises used: eq_or_eq_neg_of_abs_eq, rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) 1 (p -ᵥ s.center)
hr0 : Ne (α := ℝ) 1 0
hr' : Eq (α := ℝ) |1| 1
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))

Tactic:
simp_all
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center)
hr0 : Ne (α := ℝ) (-1) 0
hr' : Eq (α := ℝ) |(-1)| 1
inr : Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius p) ∨
    Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))

Tactic:
right
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center)
hr0 : Ne (α := ℝ) (-1) 0
hr' : Eq (α := ℝ) |(-1)| 1
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center)
hr0 : Ne (α := ℝ) (-1) 0
hr' : Eq (α := ℝ) |(-1)| 1
h : (Equiv.pointReflection s.center : (a : P) → P) p = q
⊢ Eq (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius ((Equiv.pointReflection s.center : (a : P) → P) p))

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center)
hr0 : Ne (α := ℝ) (-1) 0
hr' : Eq (α := ℝ) |(-1)| 1
⊢ q = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center) +ᵥ s.center

Tactic:
rw [← eq_vadd_iff_vsub_eq] at hr

Premises used: eq_vadd_iff_vsub_eq
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center)
hr0 : Ne (α := ℝ) (-1) 0
hr' : Eq (α := ℝ) |(-1)| 1
hr₁ : q = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center) +ᵥ s.center
⊢ Ne (α := ℝ) (-1) 0

Tactic:
rw [← eq_vadd_iff_vsub_eq] at hr

Premises used: eq_vadd_iff_vsub_eq
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr : q -ᵥ s.center = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center)
hr0 : Ne (α := ℝ) (-1) 0
hr' : Eq (α := ℝ) |(-1)| 1
hr₁ : q = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center) +ᵥ s.center
hr0₁ : Ne (α := ℝ) (-1) 0
⊢ Eq (α := ℝ) |(-1)| 1

Tactic:
rw [← eq_vadd_iff_vsub_eq] at hr

Premises used: eq_vadd_iff_vsub_eq
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius q) q
hqo : LE.le (α := AffineSubspace ℝ P) (s.orthRadius q) (s.orthRadius q)
hr : q = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center) +ᵥ s.center
hr0 : Ne (α := ℝ) (-1) 0
hr' : Eq (α := ℝ) |(-1)| 1
h : (Equiv.pointReflection s.center : (a : P) → P) p = HSMul.hSMul (α := ℝ) (-1) (p -ᵥ s.center) +ᵥ s.center
⊢ (Equiv.pointReflection s.center : (a : P) → P) p = q

Tactic:
rw [hr]