-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem dist_div_cos_oangle_center_div_two_eq_radius {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) :
    dist p₁ p₂ / Real.Angle.cos (∡ p₂ p₁ s.center) / 2 = s.radius

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ 2⁻¹ * dist p₁ p₂ = dist p₁ (midpoint ℝ p₁ p₂)

Tactic:
simp

Result:
no goals

Proof state:
case h
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0

Tactic:
simpa using h.symm

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ dist p₁ p₂ / (∡ p₂ p₁ s.center).cos / 2 = s.radius

Tactic:
rw [div_right_comm, div_eq_mul_inv _ (2 : ℝ), mul_comm,
  show (2 : ℝ)⁻¹ * dist p₁ p₂ = dist p₁ (midpoint ℝ p₁ p₂) by simp, ← mem_sphere.1 hp₁, ←
  tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center hp₁ hp₂ h, ←
  oangle_midpoint_rev_left, oangle, vadd_vsub_assoc,
  show p₂ -ᵥ p₁ = (2 : ℝ) • (midpoint ℝ p₁ p₂ -ᵥ p₁) by simp, map_smul, smul_smul,
  div_mul_cancel₀ _ (two_ne_zero' ℝ), @dist_eq_norm_vsub' V, @dist_eq_norm_vsub' V,
  vadd_vsub_assoc, add_comm, o.oangle_add_right_smul_rotation_pi_div_two, Real.Angle.cos_coe,
  Real.cos_arctan]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (1 / √(1 + (∡ p₂ p₁ s.center).tan ^ 2)) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖

case h
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ (1 + (∡ p₂ p₁ s.center).tan ^ 2) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
      ‖(∡ p₂ p₁ s.center).tan‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * (‖(∡ p₂ p₁ s.center).tan‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖)

Tactic:
conv_rhs =>
  rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs,
    abs_mul_abs_self]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ (1 + (∡ p₂ p₁ s.center).tan ^ 2) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
      (∡ p₂ p₁ s.center).tan * (∡ p₂ p₁ s.center).tan * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ p₂ -ᵥ p₁ = 2 • (midpoint ℝ p₁ p₂ -ᵥ p₁)

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (1 / √(1 + (∡ p₂ p₁ s.center).tan ^ 2)) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖

Tactic:
rw [one_div, div_inv_eq_mul, ←
  mul_self_inj (mul_nonneg (norm_nonneg _) (Real.sqrt_nonneg _)) (norm_nonneg _),
  norm_add_sq_eq_norm_sq_add_norm_sq_real (o.inner_smul_rotation_pi_div_two_right _ _), ←
  mul_assoc, mul_comm, mul_comm _ (√_), ← mul_assoc, ← mul_assoc,
  Real.mul_self_sqrt (add_nonneg zero_le_one (sq_nonneg _)), norm_smul,
  LinearIsometryEquiv.norm_map]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ (1 + (∡ p₂ p₁ s.center).tan ^ 2) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
      ‖(∡ p₂ p₁ s.center).tan‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * (‖(∡ p₂ p₁ s.center).tan‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ (1 + (∡ p₂ p₁ s.center).tan ^ 2) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
      (∡ p₂ p₁ s.center).tan * (∡ p₂ p₁ s.center).tan * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖

Tactic:
ring

Result:
no goals