awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
H : x ≠ 0 ∧ HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0
⊢ (∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) r_1 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
    ∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) (-r_1) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
have neg : ∀ (hr0 : 0 < r),
  (∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) r_1 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
    ∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) (-r_1) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
Tactic: rcases lt_trichotomy 0 r with (hr0 | rfl | hr0)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
H : x ≠ 0 ∧ HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0
neg :
  ∀ (hr0 : 0 < r),
    (∃ (r_1 : ℝ),
        0 < r_1 ∧
          HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
            HSMul.hSMul (β := V) r_1 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
      ∃ (r_1 : ℝ),
        0 < r_1 ∧
          HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
            HSMul.hSMul (β := V) (-r_1) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
⊢ (∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) r_1 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
    ∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) (-r_1) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
have neg₁ : ∀ (H : x ≠ 0 ∧ HSMul.hSMul (α := ℝ) (β := V) 0 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0),
  (∃ (r : ℝ),
      0 < r ∧
        HSMul.hSMul (α := ℝ) (β := V) 0 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
    ∃ (r : ℝ),
      0 < r ∧
        HSMul.hSMul (α := ℝ) (β := V) 0 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
Tactic: rcases lt_trichotomy 0 r with (hr0 | rfl | hr0)
Cleared hypotheses: r, H
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
H : x ≠ 0 ∧ HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0
neg :
  ∀ (hr0 : 0 < r),
    (∃ (r_1 : ℝ),
        0 < r_1 ∧
          HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
            HSMul.hSMul (β := V) r_1 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
      ∃ (r_1 : ℝ),
        0 < r_1 ∧
          HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
            HSMul.hSMul (β := V) (-r_1) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
neg₁ :
  ∀ (H : x ≠ 0 ∧ HSMul.hSMul (α := ℝ) (β := V) 0 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0),
    (∃ (r : ℝ),
        0 < r ∧
          HSMul.hSMul (α := ℝ) (β := V) 0 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
            HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
      ∃ (r : ℝ),
        0 < r ∧
          HSMul.hSMul (α := ℝ) (β := V) 0 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
            HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
⊢ (∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) r_1 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
    ∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) (-r_1) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
have neg₂ : ∀ (hr0 : r < 0),
  (∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) r_1 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
    ∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) (-r_1) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
Tactic: rcases lt_trichotomy 0 r with (hr0 | rfl | hr0)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
H : x ≠ 0 ∧ HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0
hr0 : r < 0
⊢ (∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) r_1 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
    ∃ (r_1 : ℝ),
      0 < r_1 ∧
        HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
          HSMul.hSMul (β := V) (-r_1) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
have neg : ∃ (r_1 : ℝ),
  0 < r_1 ∧
    HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
      HSMul.hSMul (β := V) (-r_1) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
Tactic: right
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
H : x ≠ 0 ∧ HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0
hr0 : r < 0
⊢ ∃ (r_1 : ℝ),
    0 < r_1 ∧
      HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
        HSMul.hSMul (β := V) (-r_1) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
have h : 0 < -r ∧
  HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) =
    HSMul.hSMul (β := V) (- -r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
Tactic: use -r
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x z : V
hxzne : x ≠ z
hxz : ‖x‖ = ‖z‖
hxyne : x ≠ 0
hxy : ‖x‖ = norm.{u_1} (E := V) 0
⊢ False
have hxy₁ : x = 0
Tactic: rw [norm_zero, norm_eq_zero] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
⊢ o.oangle y z = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
have hy : y ≠ 0
Tactic: have hy : y ≠ 0 := by
    rintro rfl
    rw [norm_zero, norm_eq_zero] at hxy
    exact hxyne hxy
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
⊢ o.oangle y z = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := norm_ne_zero_iff.1 (hxy.symm ▸ norm_ne_zero_iff.2 hy)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
⊢ o.oangle y z = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
have hz : z ≠ 0
Tactic: have hz : z ≠ 0 := norm_ne_zero_iff.1 (hxz ▸ norm_ne_zero_iff.2 hx)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ o.oangle x z - o.oangle x y =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
      ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x))
have rw : (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) - o.oangle x y =
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
    ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x))
Tactic: rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxzne.symm hxz.symm,
        o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxyne.symm hxy.symm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
rw :
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) - o.oangle x y =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
      ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x))
⊢ o.oangle x z - o.oangle x y =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
      ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x))
have rw₁ : (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
    ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x)) =
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
    ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x))
Tactic: rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxzne.symm hxz.symm,
        o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxyne.symm hxy.symm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x - o.oangle (x - z) x) = HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z))
have rw : HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z))
Tactic: rw [o.oangle_sub_right (sub_ne_zero_of_ne hxyne) (sub_ne_zero_of_ne hxzne) hx]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
have rw : HSMul.hSMul (α := ℤ) 2 (o.oangle (-(x - y)) (-(x - z))) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
Tactic: rw [← oangle_neg_neg, neg_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
rw : HSMul.hSMul (α := ℤ) 2 (o.oangle (-(x - y)) (-(x - z))) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
have rw₁ : HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (-(x - z))) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
Tactic: rw [← oangle_neg_neg, neg_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
rw : HSMul.hSMul (α := ℤ) 2 (o.oangle (-(x - y)) (-(x - z))) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
rw₁ : HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (-(x - z))) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
have rw₂ : HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
Tactic: rw [← oangle_neg_neg, neg_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ o.oangle y z = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
have y₁ : o.oangle x z - o.oangle x y =
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
    ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x))
Tactic: calc
    o.oangle y z = o.oangle x z - o.oangle x y := (o.oangle_sub_left hx hy hz).symm
    _ = π - (2 : ℤ) • o.oangle (x - z) x - (π - (2 : ℤ) • o.oangle (x - y) x) := by
      rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxzne.symm hxz.symm,
        o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxyne.symm hxy.symm]
    _ = (2 : ℤ) • (o.oangle (x - y) x - o.oangle (x - z) x) := by abel
    _ = (2 : ℤ) • o.oangle (x - y) (x - z) := by
      rw [o.oangle_sub_right (sub_ne_zero_of_ne hxyne) (sub_ne_zero_of_ne hxzne) hx]
    _ = (2 : ℤ) • o.oangle (y - x) (z - x) := by rw [← oangle_neg_neg, neg_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
y₁ :
  o.oangle x z - o.oangle x y =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
      ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x))
⊢ o.oangle y z = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
have y₂ : (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
    ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x)) =
  HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x - o.oangle (x - z) x)
Tactic: calc
    o.oangle y z = o.oangle x z - o.oangle x y := (o.oangle_sub_left hx hy hz).symm
    _ = π - (2 : ℤ) • o.oangle (x - z) x - (π - (2 : ℤ) • o.oangle (x - y) x) := by
      rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxzne.symm hxz.symm,
        o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxyne.symm hxy.symm]
    _ = (2 : ℤ) • (o.oangle (x - y) x - o.oangle (x - z) x) := by abel
    _ = (2 : ℤ) • o.oangle (x - y) (x - z) := by
      rw [o.oangle_sub_right (sub_ne_zero_of_ne hxyne) (sub_ne_zero_of_ne hxzne) hx]
    _ = (2 : ℤ) • o.oangle (y - x) (z - x) := by rw [← oangle_neg_neg, neg_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
y₁ :
  o.oangle x z - o.oangle x y =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
      ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x))
y₂ :
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
      ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x)) =
    HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x - o.oangle (x - z) x)
⊢ o.oangle y z = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
have y₃ : HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x - o.oangle (x - z) x) = HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z))
Tactic: calc
    o.oangle y z = o.oangle x z - o.oangle x y := (o.oangle_sub_left hx hy hz).symm
    _ = π - (2 : ℤ) • o.oangle (x - z) x - (π - (2 : ℤ) • o.oangle (x - y) x) := by
      rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxzne.symm hxz.symm,
        o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxyne.symm hxy.symm]
    _ = (2 : ℤ) • (o.oangle (x - y) x - o.oangle (x - z) x) := by abel
    _ = (2 : ℤ) • o.oangle (x - y) (x - z) := by
      rw [o.oangle_sub_right (sub_ne_zero_of_ne hxyne) (sub_ne_zero_of_ne hxzne) hx]
    _ = (2 : ℤ) • o.oangle (y - x) (z - x) := by rw [← oangle_neg_neg, neg_sub, neg_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
y₁ :
  o.oangle x z - o.oangle x y =
    (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
      ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x))
y₂ :
  (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - z) x) -
      ((↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x)) =
    HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x - o.oangle (x - z) x)
y₃ :
  HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x - o.oangle (x - z) x) = HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z))
⊢ o.oangle y z = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
have y₄ : HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x))
Tactic: calc
    o.oangle y z = o.oangle x z - o.oangle x y := (o.oangle_sub_left hx hy hz).symm
    _ = π - (2 : ℤ) • o.oangle (x - z) x - (π - (2 : ℤ) • o.oangle (x - y) x) := by
      rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxzne.symm hxz.symm,
        o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxyne.symm hxy.symm]
    _ = (2 : ℤ) • (o.oangle (x - y) x - o.oangle (x - z) x) := by abel
    _ = (2 : ℤ) • o.oangle (x - y) (x - z) := by
      rw [o.oangle_sub_right (sub_ne_zero_of_ne hxyne) (sub_ne_zero_of_ne hxzne) hx]
    _ = (2 : ℤ) • o.oangle (y - x) (z - x) := by rw [← oangle_neg_neg, neg_sub, neg_sub]
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
⊢ ∠ p₁ p₂ p₃ = π / 2 ↔ p₂ ∈ s
have rw : ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius
Tactic: rw [mem_sphere', EuclideanGeometry.angle,
    ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (hypothesis)
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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
⊢ ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius
have h_center : o = midpoint ℝ p₁ p₃
Tactic: have h_center : o = midpoint ℝ p₁ p₃ := hd.midpoint_eq_center.symm
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
⊢ ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius
have rw : ⟪p₁ -ᵥ o, p₃ -ᵥ o⟫_ℝ + ⟪p₁ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪o -ᵥ p₂, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
  dist s.center p₂ = s.radius
Tactic: rw [← vsub_add_vsub_cancel p₁ o p₂, ← vsub_add_vsub_cancel p₃ o p₂,
    inner_add_left, inner_add_right, inner_add_right]
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
⊢ p₁ -ᵥ o = -(p₃ -ᵥ o)
have rw : p₁ -ᵥ midpoint ℝ p₁ p₃ = -(p₃ -ᵥ midpoint ℝ p₁ p₃)
Tactic: rw [h_center, left_vsub_midpoint, right_vsub_midpoint, ← smul_neg, neg_vsub_eq_vsub_rev]
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
rw : p₁ -ᵥ midpoint ℝ p₁ p₃ = -(p₃ -ᵥ midpoint ℝ p₁ p₃)
⊢ p₁ -ᵥ o = -(p₃ -ᵥ o)
have rw₁ : HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
  -(p₃ -ᵥ midpoint ℝ p₁ p₃)
Tactic: rw [h_center, left_vsub_midpoint, right_vsub_midpoint, ← smul_neg, neg_vsub_eq_vsub_rev]
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
rw : p₁ -ᵥ midpoint ℝ p₁ p₃ = -(p₃ -ᵥ midpoint ℝ p₁ p₃)
rw₁ :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
    -(p₃ -ᵥ midpoint ℝ p₁ p₃)
⊢ p₁ -ᵥ o = -(p₃ -ᵥ o)
have rw₂ : HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
  -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₃ -ᵥ p₁)
Tactic: rw [h_center, left_vsub_midpoint, right_vsub_midpoint, ← smul_neg, neg_vsub_eq_vsub_rev]
-- 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
rw : p₁ -ᵥ midpoint ℝ p₁ p₃ = -(p₃ -ᵥ midpoint ℝ p₁ p₃)
rw₁ :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
    -(p₃ -ᵥ midpoint ℝ p₁ p₃)
rw₂ :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
    -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₃ -ᵥ p₁)
⊢ p₁ -ᵥ o = -(p₃ -ᵥ o)
have rw₃ : HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(p₃ -ᵥ p₁))
Tactic: rw [h_center, left_vsub_midpoint, right_vsub_midpoint, ← smul_neg, neg_vsub_eq_vsub_rev]