case inl
V : Type ?u.9686
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₂ p : P
⊢ dist p (midpoint ℝ p p₂) = ‖2‖⁻¹ * dist p p₂

case inr.refl
V : Type ?u.9686
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ dist p₂ (midpoint ℝ p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂
V : Type ?u.9686
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ ∀ (p : P), p ∈ {p₁, p₂} → dist p (midpoint ℝ p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂
rintro p (rfl | rfl | _)
no goals
case inl
V : Type ?u.9686
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₂ p : P
⊢ dist p (midpoint ℝ p p₂) = ‖2‖⁻¹ * dist p p₂
rw [dist_comm, dist_midpoint_left (𝕜 := ℝ)]
no goals
case inr.refl
V : Type ?u.9686
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ dist p₂ (midpoint ℝ p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂
rw [dist_comm, dist_midpoint_right (𝕜 := ℝ)]