case refine'_1
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : secondInter s p v = p
⊢ inner v (p -ᵥ s.center) = 0

case refine'_2
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : inner v (p -ᵥ s.center) = 0
⊢ secondInter s p v = p
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
⊢ secondInter s p v = p ↔ inner v (p -ᵥ s.center) = 0
refine' ⟨fun hp => _, fun hp => _⟩
case pos
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : secondInter s p v = p
hv : v = 0
⊢ inner v (p -ᵥ s.center) = 0

case neg
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : secondInter s p v = p
hv : ¬v = 0
⊢ inner v (p -ᵥ s.center) = 0
case refine'_1
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : secondInter s p v = p
⊢ inner v (p -ᵥ s.center) = 0
by_cases hv : v = 0
no goals
case neg
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : secondInter s p v = p
hv : ¬v = 0
⊢ inner v (p -ᵥ s.center) = 0
rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
  or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
  or_iff_right (by norm_num : (-2 : ℝ) ≠ 0)] at hp
no goals
case pos
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : secondInter s p v = p
hv : v = 0
⊢ inner v (p -ᵥ s.center) = 0
simp [hv]
no goals
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : -2 = 0 ∨ inner v (p -ᵥ s.center) = 0
hv : ¬v = 0
⊢ -2 ≠ 0
norm_num
no goals
case refine'_2
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : inner v (p -ᵥ s.center) = 0
⊢ secondInter s p v = p
rw [Sphere.secondInter, hp, MulZeroClass.mul_zero, zero_div, zero_smul, zero_vadd]