awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
rw :
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ s.center p₂ p₁) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ s.center)
rw₁ rw₂ :
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ s.center) =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ s.center)
⊢ ∡ p₁ s.center p₂ = (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₁ s.center)

Tactic:
rw [oangle_eq_pi_sub_two_zsmul_oangle_center_left hp₁ hp₂ h,
    oangle_eq_oangle_of_dist_eq (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)]

Premises used: EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_left, EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere', EuclideanGeometry.oangle_eq_oangle_of_dist_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₁p₃ : p₁ ≠ p₃
rw : HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + ∡ p₁ s.center p₃ = (↑π : Real.Angle)
rw₁ :
  HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center)) =
    (↑π : Real.Angle)
rw₂ rw₃ : (↑π : Real.Angle) = (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = (↑π : Real.Angle)

Tactic:
rw [← oangle_center_eq_two_zsmul_oangle hp₁ hp₂ hp₃ hp₂p₁ hp₂p₃,
    oangle_eq_pi_sub_two_zsmul_oangle_center_right hp₁ hp₃ hp₁p₃, add_sub_cancel]

Premises used: EuclideanGeometry.Sphere.oangle_eq_pi_sub_two_zsmul_oangle_center_right, add_sub_cancel, EuclideanGeometry.Sphere.oangle_center_eq_two_zsmul_oangle
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ |(∡ s.center p₂ p₁).toReal| < π / 2

Tactic:
abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq
    (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)

Premises used: EuclideanGeometry.abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq, EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere'
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ |(∡ p₂ p₁ s.center).toReal| < π / 2

Tactic:
abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq
    (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)

Premises used: EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere', EuclideanGeometry.abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
obtain :
  ∀ (r : ℝ)
    (hr :
      HSMul.hSMul (β := V) r ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
          midpoint ℝ p₁ p₂ =
        s.center),
    HSMul.hSMul (β := V) ((∡ p₂ p₁ s.center).tan / 2)
          ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
        midpoint ℝ p₁ p₂ =
      s.center
⊢ HSMul.hSMul (β := V) ((∡ p₂ p₁ s.center).tan / 2)
        ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂ =
    s.center

Tactic:
obtain ⟨r, hr⟩ := (dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint h).1
    (dist_center_eq_dist_center_of_mem_sphere hp₁ hp₂)

Premises used: EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint, Iff.mp, EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr :
  HSMul.hSMul (β := V) r ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂ =
    s.center
rw :
  HSMul.hSMul (β := V)
        ((Orientation.oangle «o» (midpoint ℝ p₁ p₂ -ᵥ p₁)
              (HSMul.hSMul (β := V) r
                  ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +
                (midpoint ℝ p₁ p₂ -ᵥ p₁))).tan /
          2)
        ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂ =
    HSMul.hSMul (β := V) r ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂
⊢ HSMul.hSMul (β := V) ((∡ p₂ p₁ s.center).tan / 2)
        ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂ =
    s.center

Tactic:
rw [← hr, ← oangle_midpoint_rev_left, oangle, vadd_vsub_assoc]

Premises used: EuclideanGeometry.oangle, vadd_vsub_assoc, EuclideanGeometry.oangle_midpoint_rev_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr :
  HSMul.hSMul (β := V) r ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂ =
    s.center
⊢ p₂ -ᵥ p₁ = HSMul.hSMul (α := ℝ) 2 (midpoint ℝ p₁ p₂ -ᵥ p₁)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr :
  HSMul.hSMul (β := V) r ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂ =
    s.center
nth_rw :
  HSMul.hSMul (β := V)
        ((Orientation.oangle «o» (midpoint ℝ p₁ p₂ -ᵥ p₁)
              (HSMul.hSMul (β := V) r
                  ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V)
                      (HSMul.hSMul (α := ℝ) 2 (midpoint ℝ p₁ p₂ -ᵥ p₁)) :
                    V) +
                (midpoint ℝ p₁ p₂ -ᵥ p₁))).tan /
          2)
        ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂ =
    HSMul.hSMul (β := V) r ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂
⊢ HSMul.hSMul (β := V)
        ((Orientation.oangle «o» (midpoint ℝ p₁ p₂ -ᵥ p₁)
              (HSMul.hSMul (β := V) r
                  ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +
                (midpoint ℝ p₁ p₂ -ᵥ p₁))).tan /
          2)
        ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂ =
    HSMul.hSMul (β := V) r ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂

Tactic:
nth_rw 1 [show p₂ -ᵥ p₁ = (2 : ℝ) • (midpoint ℝ p₁ p₂ -ᵥ p₁) by simp]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr :
  HSMul.hSMul (β := V) r ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂ =
    s.center
h₁ : midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
⊢ HSMul.hSMul (β := V)
        ((Orientation.oangle «o» (midpoint ℝ p₁ p₂ -ᵥ p₁)
              (HSMul.hSMul (β := V) r
                  ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V)
                      (HSMul.hSMul (α := ℝ) 2 (midpoint ℝ p₁ p₂ -ᵥ p₁)) :
                    V) +
                (midpoint ℝ p₁ p₂ -ᵥ p₁))).tan /
          2)
        ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂ =
    HSMul.hSMul (β := V) r ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂

Tactic:
rw [map_smul, smul_smul, add_comm, o.tan_oangle_add_right_smul_rotation_pi_div_two,
    mul_div_cancel_right₀ _ (two_ne_zero' ℝ)]

Premises used: Real, Orientation.tan_oangle_add_right_smul_rotation_pi_div_two, smul_smul, add_comm, mul_div_cancel_right₀, two_ne_zero', EuclideanGeometry.o, map_smul
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr :
  HSMul.hSMul (β := V) r ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂ =
    s.center
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0

Tactic:
simpa using h.symm

Premises used: Ne.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ HSMul.hSMul (β := V) ((∡ p₃ p₁ s.center).tan / 2)
        ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₃ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₃ =
    s.center

Tactic:
tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center hp₁ hp₃ hp₁p₃

Premises used: EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
h : (∡ p₁ p₂ p₃).tan⁻¹ = (∡ p₃ p₁ s.center).tan
⊢ HSMul.hSMul (β := V) ((∡ p₁ p₂ p₃).tan⁻¹ / 2)
        ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₃ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₃ =
    s.center

Tactic:
convert! tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center hp₁ hp₃ hp₁p₃

Premises used: EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ (∡ p₁ p₂ p₃).tan⁻¹ = (∡ p₃ p₁ s.center).tan

Tactic:
(Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi _).symm

Premises used: Eq.symm, Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) + HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) = (↑π : Real.Angle)
⊢ (∡ p₁ p₂ p₃).tan⁻¹ = (∡ p₃ p₁ s.center).tan

Tactic:
convert! (Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi _).symm

Premises used: Eq.symm, Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
h : HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = (↑π : Real.Angle)
h₁ h₂ : (↑π : Real.Angle) = (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) + HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) = (↑π : Real.Angle)

Tactic:
rw [add_comm,
    two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₂ hp₃ hp₁p₂.symm hp₂p₃ hp₁p₃]

Premises used: Ne.symm, add_comm, EuclideanGeometry.Sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ p₂ -ᵥ p₁ = HSMul.hSMul (α := ℝ) 2 (midpoint ℝ p₁ p₂ -ᵥ p₁)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
rw :
  ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (1 / √(1 + HPow.hPow (β := ℕ) (∡ p₂ p₁ s.center).tan 2)) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ +
        HSMul.hSMul (β := V) (∡ p₂ p₁ s.center).tan
          ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (midpoint ℝ p₁ p₂ -ᵥ p₁) : V)‖
h₁ : midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
⊢ 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]

Premises used: EuclideanGeometry.oangle, div_mul_cancel₀, Real, vadd_vsub_assoc, div_right_comm, EuclideanGeometry.oangle_midpoint_rev_left, EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, smul_smul, dist_eq_norm_vsub', div_eq_mul_inv, add_comm, two_ne_zero', EuclideanGeometry.mem_sphere, Orientation.oangle_add_right_smul_rotation_pi_div_two, Real.Angle.cos_coe, Iff.mp, mul_comm, OfNat.ofNat, EuclideanGeometry.o, map_smul, Real.cos_arctan
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
norm_cast :
  ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (1 / √(1 + HPow.hPow (β := ℕ) (∡ p₂ p₁ s.center).tan 2)) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ +
        HSMul.hSMul (β := V) (∡ p₂ p₁ s.center).tan
          ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (midpoint ℝ p₁ p₂ -ᵥ p₁) : V)‖
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (1 / √(1 + HPow.hPow (β := ℕ) (∡ p₂ p₁ s.center).tan 2)) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ +
        HSMul.hSMul (β := V) (∡ p₂ p₁ s.center).tan
          ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (midpoint ℝ p₁ p₂ -ᵥ p₁) : V)‖

Tactic:
norm_cast
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ 0 ≤ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * √(1 + HPow.hPow (β := ℕ) (∡ p₂ p₁ s.center).tan 2)

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ 0 ≤
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ +
        HSMul.hSMul (β := V) (∡ p₂ p₁ s.center).tan
          ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (midpoint ℝ p₁ p₂ -ᵥ p₁) : V)‖

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ 0 ≤ 1 + HPow.hPow (β := ℕ) (∡ p₂ p₁ s.center).tan 2

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
rw :
  (1 + HPow.hPow (β := ℕ) (∡ 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₁‖)
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (1 / √(1 + HPow.hPow (β := ℕ) (∡ p₂ p₁ s.center).tan 2)) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ +
        HSMul.hSMul (β := V) (∡ p₂ p₁ s.center).tan
          ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (midpoint ℝ p₁ p₂ -ᵥ p₁) : V)‖

Tactic:
rw [one_div, div_inv_eq_mul, ← mul_self_inj (by positivity) (by positivity),
      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 (by positivity), norm_smul, LinearIsometryEquiv.norm_map]

Premises used: norm_smul, LinearIsometryEquiv.norm_map, mul_assoc, Real.mul_self_sqrt, Orientation.inner_smul_rotation_pi_div_two_right, one_div, mul_comm, Real.sqrt, div_inv_eq_mul, EuclideanGeometry.o, norm_add_sq_eq_norm_sq_add_norm_sq_real, mul_self_inj
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
rw :
  ‖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₁‖
| ‖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:
rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs,
        abs_mul_abs_self]

Premises used: Norm.norm, mul_assoc, Real.Angle.tan, mul_comm, abs_mul_abs_self, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
conv_rhs :
  (1 + HPow.hPow (β := ℕ) (∡ 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₁‖
⊢ (1 + HPow.hPow (β := ℕ) (∡ 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]

Premises used: Norm.norm, mul_assoc, Real.Angle.tan, mul_comm, abs_mul_abs_self, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ (1 + HPow.hPow (β := ℕ) (∡ 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
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : 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

Premises used: Ne.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
rw : dist p₁ p₂ / (∡ p₂ p₁ s.center).cos = 2 * (dist p₁ p₂ / (∡ p₂ p₁ s.center).cos / 2)
rw₁ rw₂ : dist p₁ p₂ / (∡ p₂ p₁ s.center).cos = dist p₁ p₂ / (∡ p₂ p₁ s.center).cos
⊢ dist p₁ p₂ / (∡ p₂ p₁ s.center).cos = 2 * s.radius

Tactic:
rw [← dist_div_cos_oangle_center_div_two_eq_radius hp₁ hp₂ h, mul_div_cancel₀ _ (two_ne_zero' ℝ)]

Premises used: Real, EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radius, mul_div_cancel₀, two_ne_zero'
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₁ p₃ / (∡ p₃ p₁ s.center).cos / 2 = s.radius

Tactic:
dist_div_cos_oangle_center_div_two_eq_radius hp₁ hp₃ hp₁p₃

Premises used: EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radius