awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₂
⊢ 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
have 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
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₂)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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
⊢ 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
have 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₂
Tactic: rw [← hr, ← oangle_midpoint_rev_left, oangle, vadd_vsub_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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
⊢ 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₂
have 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₂
Tactic: nth_rw 1 [show p₂ -ᵥ p₁ = (2 : ℝ) • (midpoint ℝ p₁ p₂ -ᵥ p₁) by simp]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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
⊢ 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₂
have h₁ : midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
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' ℝ)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₂ p₃).tan⁻¹ / 2)
        ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (p₃ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₃ =
    s.center
have h : (∡ p₁ p₂ p₃).tan⁻¹ = (∡ p₃ p₁ s.center).tan
Tactic: convert! tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center hp₁ hp₃ hp₁p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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
have h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) + HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) = (↑π : Real.Angle)
Tactic: convert! (Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi _).symm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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 (α := ℤ) 2 (∡ p₁ p₂ p₃) + HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) = (↑π : Real.Angle)
have h : HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) + HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = (↑π : 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₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) + HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₁ s.center) = (↑π : Real.Angle)
have h₁ : (↑π : Real.Angle) = (↑π : 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₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₂
⊢ dist p₁ p₂ / (∡ p₂ p₁ s.center).cos / 2 = s.radius
have 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)‖
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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)‖
⊢ dist p₁ p₂ / (∡ p₂ p₁ s.center).cos / 2 = s.radius
have h₁ : midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₁‖ / (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)‖
have 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₁‖)
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
    ‖(∡ p₂ p₁ s.center).tan‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * (‖(∡ p₂ p₁ s.center).tan‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖)
have 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₁‖
Tactic: rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs,
        abs_mul_abs_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * (‖(∡ p₂ p₁ s.center).tan‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖)
have 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₁‖
Tactic: conv_rhs =>
      rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs,
        abs_mul_abs_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₂
⊢ dist p₁ p₂ / (∡ p₂ p₁ s.center).cos = 2 * s.radius
have rw : dist p₁ p₂ / (∡ p₂ p₁ s.center).cos = 2 * (dist p₁ p₂ / (∡ p₂ p₁ s.center).cos / 2)
Tactic: rw [← dist_div_cos_oangle_center_div_two_eq_radius hp₁ hp₂ h, mul_div_cancel₀ _ (two_ne_zero' ℝ)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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)
⊢ dist p₁ p₂ / (∡ p₂ p₁ s.center).cos = 2 * s.radius
have rw₁ : dist p₁ p₂ / (∡ p₂ p₁ s.center).cos = dist p₁ p₂ / (∡ p₂ p₁ s.center).cos
Tactic: rw [← dist_div_cos_oangle_center_div_two_eq_radius hp₁ hp₂ h, mul_div_cancel₀ _ (two_ne_zero' ℝ)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₂ p₃).sin| / 2 = s.radius
have h : |(∡ p₁ p₂ p₃).sin| = (∡ p₃ p₁ s.center).cos
Tactic: convert! dist_div_cos_oangle_center_div_two_eq_radius hp₁ hp₃ hp₁p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₃).sin| = (∡ p₃ p₁ s.center).cos
have rw : |(∡ p₃ p₁ s.center).toReal| ≤ π / 2
Tactic: rw [← Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi
    (two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₂ hp₃ hp₁p₂.symm hp₂p₃ hp₁p₃),
    abs_of_nonneg (Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two.2 _)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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₂ p₃).sin| = 2 * s.radius
have rw : dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| = 2 * (dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| / 2)
Tactic: rw [← dist_div_sin_oangle_div_two_eq_radius hp₁ hp₂ hp₃ hp₁p₂ hp₁p₃ hp₂p₃,
    mul_div_cancel₀ _ (two_ne_zero' ℝ)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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 : dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| = 2 * (dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| / 2)
⊢ dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| = 2 * s.radius
have rw₁ : dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| = dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin|
Tactic: rw [← dist_div_sin_oangle_div_two_eq_radius hp₁ hp₂ hp₃ hp₁p₂ hp₁p₃ hp₂p₃,
    mul_div_cancel₀ _ (two_ne_zero' ℝ)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁ : t₁.points i₁ = t₂.points i₁
h₃ : t₁.points i₃ = t₂.points i₃
h₂ :
  HSMul.hSMul (α := ℤ) 2 (∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃))
⊢ Simplex.circumsphere t₁ = Simplex.circumsphere t₂
have rw : {
    center :=
      HSMul.hSMul (β := V) ((∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).tan⁻¹ / 2)
          ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (t₁.points i₃ -ᵥ t₁.points i₁) : V) +ᵥ
        midpoint ℝ (t₁.points i₁) (t₁.points i₃),
    radius := dist (t₁.points i₁) (t₁.points i₃) / |(∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).sin| / 2 } =
  Simplex.circumsphere t₂
Tactic: rw [t₁.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
    t₂.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
    Real.Angle.tan_eq_of_two_zsmul_eq h₂, Real.Angle.abs_sin_eq_of_two_zsmul_eq h₂, h₁, h₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁ : t₁.points i₁ = t₂.points i₁
h₃ : t₁.points i₃ = t₂.points i₃
h₂ :
  HSMul.hSMul (α := ℤ) 2 (∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃))
rw :
  {
      center :=
        HSMul.hSMul (β := V) ((∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).tan⁻¹ / 2)
            ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (t₁.points i₃ -ᵥ t₁.points i₁) : V) +ᵥ
          midpoint ℝ (t₁.points i₁) (t₁.points i₃),
      radius := dist (t₁.points i₁) (t₁.points i₃) / |(∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).sin| / 2 } =
    Simplex.circumsphere t₂
⊢ Simplex.circumsphere t₁ = Simplex.circumsphere t₂
have rw₁ : Eq (α := Sphere P)
  {
    center :=
      HSMul.hSMul (β := V) ((∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).tan⁻¹ / 2)
          ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (t₁.points i₃ -ᵥ t₁.points i₁) : V) +ᵥ
        midpoint ℝ (t₁.points i₁) (t₁.points i₃),
    radius := dist (t₁.points i₁) (t₁.points i₃) / |(∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).sin| / 2 }
  {
    center :=
      HSMul.hSMul (β := V) ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2)
          ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (t₂.points i₃ -ᵥ t₂.points i₁) : V) +ᵥ
        midpoint ℝ (t₂.points i₁) (t₂.points i₃),
    radius := dist (t₂.points i₁) (t₂.points i₃) / |(∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).sin| / 2 }
Tactic: rw [t₁.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
    t₂.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
    Real.Angle.tan_eq_of_two_zsmul_eq h₂, Real.Angle.abs_sin_eq_of_two_zsmul_eq h₂, h₁, h₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁ : t₁.points i₁ = t₂.points i₁
h₃ : t₁.points i₃ = t₂.points i₃
h₂ :
  HSMul.hSMul (α := ℤ) 2 (∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)) =
    HSMul.hSMul (α := ℤ) 2 (∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃))
rw :
  {
      center :=
        HSMul.hSMul (β := V) ((∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).tan⁻¹ / 2)
            ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (t₁.points i₃ -ᵥ t₁.points i₁) : V) +ᵥ
          midpoint ℝ (t₁.points i₁) (t₁.points i₃),
      radius := dist (t₁.points i₁) (t₁.points i₃) / |(∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).sin| / 2 } =
    Simplex.circumsphere t₂
rw₁ :
  Eq (α := Sphere P)
    {
      center :=
        HSMul.hSMul (β := V) ((∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).tan⁻¹ / 2)
            ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (t₁.points i₃ -ᵥ t₁.points i₁) : V) +ᵥ
          midpoint ℝ (t₁.points i₁) (t₁.points i₃),
      radius := dist (t₁.points i₁) (t₁.points i₃) / |(∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).sin| / 2 }
    {
      center :=
        HSMul.hSMul (β := V) ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2)
            ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (t₂.points i₃ -ᵥ t₂.points i₁) : V) +ᵥ
          midpoint ℝ (t₂.points i₁) (t₂.points i₃),
      radius := dist (t₂.points i₁) (t₂.points i₃) / |(∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).sin| / 2 }
⊢ Simplex.circumsphere t₁ = Simplex.circumsphere t₂
have rw₂ : Eq (α := Sphere P)
  {
    center :=
      HSMul.hSMul (β := V) ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2)
          ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (t₁.points i₃ -ᵥ t₁.points i₁) : V) +ᵥ
        midpoint ℝ (t₁.points i₁) (t₁.points i₃),
    radius := dist (t₁.points i₁) (t₁.points i₃) / |(∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).sin| / 2 }
  {
    center :=
      HSMul.hSMul (β := V) ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2)
          ((Orientation.rotation «o» (↑(π / 2) : Real.Angle) : (a : V) → V) (t₂.points i₃ -ᵥ t₂.points i₁) : V) +ᵥ
        midpoint ℝ (t₂.points i₁) (t₂.points i₃),
    radius := dist (t₂.points i₁) (t₂.points i₃) / |(∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).sin| / 2 }
Tactic: rw [t₁.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
    t₂.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
    Real.Angle.tan_eq_of_two_zsmul_eq h₂, Real.Angle.abs_sin_eq_of_two_zsmul_eq h₂, h₁, h₃]