-- 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 }
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 }
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 }
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₃]