awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : o.oangle x y = -o.oangle y z
hs' : (o.oangle x y).sign = -(o.oangle y z).sign
pos : o.oangle x y + o.oangle y z = 0
⊢ SameRay ℝ x z

Tactic:
rw [← o.oangle_eq_zero_iff_sameRay, ← o.oangle_add hx hy hz]

Premises used: Orientation.oangle_add, Orientation.oangle_eq_zero_iff_sameRay
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : o.oangle x y = -o.oangle y z
hs' : (o.oangle x y).sign = -(o.oangle y z).sign
⊢ o.oangle x y + o.oangle y z = 0

Tactic:
simp [he]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
revert :
  ∀ (hs : ¬(o.oangle x y).sign = (o.oangle y z).sign) (hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign),
    (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
⊢ (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0

Tactic:
revert hs hs'
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
generalize :
  ∀ (sxy : SignType) (hs : ¬sxy = (o.oangle y z).sign) (hs' : ¬sxy = -(o.oangle y z).sign),
    sxy = 0 ∨ (o.oangle y z).sign = 0
⊢ ∀ (hs : ¬(o.oangle x y).sign = (o.oangle y z).sign) (hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign),
    (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0

Tactic:
generalize (o.oangle x y).sign = sxy

Premises used: Orientation.oangle, Real.Angle.sign
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
sxy : SignType
generalize : ∀ (syz : SignType) (hs : ¬sxy = syz) (hs' : ¬sxy = -syz), sxy = 0 ∨ syz = 0
⊢ ∀ (hs : ¬sxy = (o.oangle y z).sign) (hs' : ¬sxy = -(o.oangle y z).sign), sxy = 0 ∨ (o.oangle y z).sign = 0

Tactic:
generalize (o.oangle y z).sign = syz

Premises used: Orientation.oangle, Real.Angle.sign
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
sxy syz : SignType
⊢ ∀ (hs : ¬sxy = syz) (hs' : ¬sxy = -syz), sxy = 0 ∨ syz = 0

Tactic:
decide +revert
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
⊢ (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0

Tactic:
have h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0 := by
        revert hs hs'
        generalize (o.oangle x y).sign = sxy
        generalize (o.oangle y z).sign = syz
        decide +revert
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
inl : ∀ (h0 : (o.oangle x y).sign = 0), InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
inr : ∀ (h0 : (o.oangle y z).sign = 0), InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
⊢ InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π

Tactic:
rcases h0 with h0 | h0
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0
⊢ InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π

Tactic:
simpa [*] using o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h0

Premises used: Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle y z).sign = 0
⊢ InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π

Tactic:
simpa [*] using o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h0

Premises used: Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
⊢ InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π

Tactic:
have h0' : InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π := by
        rcases h0 with h0 | h0
          <;> simpa [*] using o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h0
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
neg : ∀ (h0' : InnerProductGeometry.angle y z = 0), SameRay ℝ x z
neg₁ : ∀ (h0' : InnerProductGeometry.angle y z = π), SameRay ℝ x z
⊢ SameRay ℝ x z

Tactic:
rcases h0' with h0' | h0'
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = 0
⊢ InnerProductGeometry.angle x y = 0

Tactic:
rw [h0'] at he
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = 0
he₁ : InnerProductGeometry.angle x y = 0
⊢ ¬(o.oangle x y).sign = -(o.oangle y z).sign

Tactic:
rw [h0'] at he
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = 0
he₁ : InnerProductGeometry.angle x y = 0
hs'₁ : ¬(o.oangle x y).sign = -(o.oangle y z).sign
⊢ (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0

Tactic:
rw [h0'] at he
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = 0
he₁ : InnerProductGeometry.angle x y = 0
hs'₁ : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0₁ : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
⊢ InnerProductGeometry.angle y z = 0

Tactic:
rw [h0'] at he
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = 0
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = 0
neg :
  ∀ (r : ℝ) (hr0 : 0 < r) (hz : r • y ≠ 0) (hr : ¬SameRay ℝ x (r • y))
    (hs : ¬(o.oangle x y).sign = (o.oangle y (r • y)).sign) (hn : o.oangle x y ≠ o.oangle y (r • y))
    (hs' : ¬(o.oangle x y).sign = -(o.oangle y (r • y)).sign)
    (h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y (r • y)).sign = 0) (h0' : InnerProductGeometry.angle y (r • y) = 0),
    SameRay ℝ x (r • y)
⊢ SameRay ℝ x z

Tactic:
obtain ⟨-, r, hr0, rfl⟩ := InnerProductGeometry.angle_eq_zero_iff.1 h0'

Premises used: InnerProductGeometry.angle_eq_zero_iff, Iff.mp, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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 : V
hx : x ≠ 0
hy : ¬y = 0
he : InnerProductGeometry.angle x y = 0
r : ℝ
hr0 : 0 < r
hz : r • y ≠ 0
hr : ¬SameRay ℝ x (r • y)
hs : ¬(o.oangle x y).sign = (o.oangle y (r • y)).sign
hn : o.oangle x y ≠ o.oangle y (r • y)
hs' : ¬(o.oangle x y).sign = -(o.oangle y (r • y)).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y (r • y)).sign = 0
h0' : InnerProductGeometry.angle y (r • y) = 0
neg :
  ∀ (r' : ℝ) (hr'0 : 0 < r') (hy : ¬r' • x = 0) (he : InnerProductGeometry.angle x (r' • x) = 0) (hz : r • r' • x ≠ 0)
    (hr : ¬SameRay ℝ x (r • r' • x)) (hs : ¬(o.oangle x (r' • x)).sign = (o.oangle (r' • x) (r • r' • x)).sign)
    (hn : o.oangle x (r' • x) ≠ o.oangle (r' • x) (r • r' • x))
    (hs' : ¬(o.oangle x (r' • x)).sign = -(o.oangle (r' • x) (r • r' • x)).sign)
    (h0 : (o.oangle x (r' • x)).sign = 0 ∨ (o.oangle (r' • x) (r • r' • x)).sign = 0)
    (h0' : InnerProductGeometry.angle (r' • x) (r • r' • x) = 0), SameRay ℝ x (r • r' • x)
⊢ SameRay ℝ x (r • y)

Tactic:
obtain ⟨-, r', hr'0, rfl⟩ := InnerProductGeometry.angle_eq_zero_iff.1 he

Premises used: InnerProductGeometry.angle_eq_zero_iff, Iff.mp, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
r : ℝ
hr0 : 0 < r
r' : ℝ
hr'0 : 0 < r'
hy : ¬r' • x = 0
he : InnerProductGeometry.angle x (r' • x) = 0
hz : r • r' • x ≠ 0
hr : ¬SameRay ℝ x (r • r' • x)
hs : ¬(o.oangle x (r' • x)).sign = (o.oangle (r' • x) (r • r' • x)).sign
hn : o.oangle x (r' • x) ≠ o.oangle (r' • x) (r • r' • x)
hs' : ¬(o.oangle x (r' • x)).sign = -(o.oangle (r' • x) (r • r' • x)).sign
h0 : (o.oangle x (r' • x)).sign = 0 ∨ (o.oangle (r' • x) (r • r' • x)).sign = 0
h0' : InnerProductGeometry.angle (r' • x) (r • r' • x) = 0
⊢ SameRay ℝ x (r • r' • x)

Tactic:
simp_all
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = π
⊢ InnerProductGeometry.angle x y = π

Tactic:
rw [h0'] at he
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = π
he₁ : InnerProductGeometry.angle x y = π
⊢ ¬(o.oangle x y).sign = -(o.oangle y z).sign

Tactic:
rw [h0'] at he
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = π
he₁ : InnerProductGeometry.angle x y = π
hs'₁ : ¬(o.oangle x y).sign = -(o.oangle y z).sign
⊢ (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0

Tactic:
rw [h0'] at he
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = π
he₁ : InnerProductGeometry.angle x y = π
hs'₁ : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0₁ : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
⊢ InnerProductGeometry.angle y z = π

Tactic:
rw [h0'] at he
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = π
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = π
neg :
  ∀ (r : ℝ) (hr0 : r < 0) (hz : r • y ≠ 0) (hr : ¬SameRay ℝ x (r • y))
    (hs : ¬(o.oangle x y).sign = (o.oangle y (r • y)).sign) (hn : o.oangle x y ≠ o.oangle y (r • y))
    (hs' : ¬(o.oangle x y).sign = -(o.oangle y (r • y)).sign)
    (h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y (r • y)).sign = 0) (h0' : InnerProductGeometry.angle y (r • y) = π),
    SameRay ℝ x (r • y)
⊢ SameRay ℝ x z

Tactic:
obtain ⟨-, r, hr0, rfl⟩ := InnerProductGeometry.angle_eq_pi_iff.1 h0'

Premises used: Iff.mp, InnerProductGeometry.angle_eq_pi_iff, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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 : V
hx : x ≠ 0
hy : ¬y = 0
he : InnerProductGeometry.angle x y = π
r : ℝ
hr0 : r < 0
hz : r • y ≠ 0
hr : ¬SameRay ℝ x (r • y)
hs : ¬(o.oangle x y).sign = (o.oangle y (r • y)).sign
hn : o.oangle x y ≠ o.oangle y (r • y)
hs' : ¬(o.oangle x y).sign = -(o.oangle y (r • y)).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y (r • y)).sign = 0
h0' : InnerProductGeometry.angle y (r • y) = π
neg :
  ∀ (r' : ℝ) (hr'0 : r' < 0) (hy : ¬r' • x = 0) (he : InnerProductGeometry.angle x (r' • x) = π) (hz : r • r' • x ≠ 0)
    (hr : ¬SameRay ℝ x (r • r' • x)) (hs : ¬(o.oangle x (r' • x)).sign = (o.oangle (r' • x) (r • r' • x)).sign)
    (hn : o.oangle x (r' • x) ≠ o.oangle (r' • x) (r • r' • x))
    (hs' : ¬(o.oangle x (r' • x)).sign = -(o.oangle (r' • x) (r • r' • x)).sign)
    (h0 : (o.oangle x (r' • x)).sign = 0 ∨ (o.oangle (r' • x) (r • r' • x)).sign = 0)
    (h0' : InnerProductGeometry.angle (r' • x) (r • r' • x) = π), SameRay ℝ x (r • r' • x)
⊢ SameRay ℝ x (r • y)

Tactic:
obtain ⟨-, r', hr'0, rfl⟩ := InnerProductGeometry.angle_eq_pi_iff.1 he

Premises used: Iff.mp, InnerProductGeometry.angle_eq_pi_iff, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
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
hx : x ≠ 0
r : ℝ
hr0 : r < 0
r' : ℝ
hr'0 : r' < 0
hy : ¬r' • x = 0
he : InnerProductGeometry.angle x (r' • x) = π
hz : r • r' • x ≠ 0
hr : ¬SameRay ℝ x (r • r' • x)
hs : ¬(o.oangle x (r' • x)).sign = (o.oangle (r' • x) (r • r' • x)).sign
hn : o.oangle x (r' • x) ≠ o.oangle (r' • x) (r • r' • x)
hs' : ¬(o.oangle x (r' • x)).sign = -(o.oangle (r' • x) (r • r' • x)).sign
h0 : (o.oangle x (r' • x)).sign = 0 ∨ (o.oangle (r' • x) (r • r' • x)).sign = 0
h0' : InnerProductGeometry.angle (r' • x) (r • r' • x) = π
⊢ SameRay ℝ x (r • r' • x)

Tactic:
simp_all
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Projection
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)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ Nonempty.{u_2 + 1} ↥s

Tactic:
haveI : Nonempty s := ⟨p', h⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Projection
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)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
this : Nonempty.{u_2 + 1} ↥s
⊢ p ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)

Tactic:
have hpne : p ≠ orthogonalProjection s p := Ne.symm (orthogonalProjection_eq_self_iff.not.2 hp)
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Projection
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)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
this : Nonempty.{u_2 + 1} ↥s
hpne : p ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' =
      (↑(∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p') : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' =
      -(↑(∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p') : Real.Angle)

Tactic:
have ha := oangle_eq_angle_or_eq_neg_angle hpne hp'
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Projection
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)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
this : Nonempty.{u_2 + 1} ↥s
hpne : p ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
ha :
  ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' =
      (↑(∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p') : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' =
      -(↑(∠ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p') : Real.Angle)
⊢ ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = -(↑(π / 2) : Real.Angle)

Tactic:
rw [angle_self_orthogonalProjection p h] at ha

Premises used: EuclideanGeometry.angle_self_orthogonalProjection
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Projection
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)
p p' : P
s : AffineSubspace ℝ P
inst_5 : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
this : Nonempty.{u_2 + 1} ↥s
hpne : p ≠ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
ha :
  ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = -(↑(π / 2) : Real.Angle)
rwa rwa₁ rwa₂ rwa₃ :
  ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(-(π / 2)) : Real.Angle)
⊢ ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(π / 2) : Real.Angle) ∨
    ∡ p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p' = (↑(-π / 2) : Real.Angle)

Tactic:
rwa [neg_div]

Premises used: neg_div