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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
⊢ π / 2 ≠ π

Tactic:
have hpi : π / 2 ≠ π := by
      intro hpi
      rw [div_eq_iff, eq_comm, ← sub_eq_zero, mul_two, add_sub_cancel_right] at hpi
      · exact Real.pi_pos.ne.symm hpi
      · exact two_ne_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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
⊢ w = 0 ∨ x = 0 ∨ InnerProductGeometry.angle w x = 0 ∨ InnerProductGeometry.angle w x = π

Tactic:
have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hswx
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0' : w = 0 ∨ x = 0 ∨ InnerProductGeometry.angle w x = 0 ∨ InnerProductGeometry.angle w x = π
⊢ w = 0 ∨ x = 0

Tactic:
simpa [hwx, Real.pi_pos.ne.symm, hpi] using h0'

Premises used: Real.pi_pos, Ne.symm, LT.lt.ne
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
⊢ w = 0 ∨ x = 0

Tactic:
have h0wx : w = 0 ∨ x = 0 := by
      have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hswx
      simpa [hwx, Real.pi_pos.ne.symm, hpi] using 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0wx : w = 0 ∨ x = 0
⊢ y = 0 ∨ z = 0 ∨ InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π

Tactic:
have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hsyz
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0wx : w = 0 ∨ x = 0
h0' : y = 0 ∨ z = 0 ∨ InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
⊢ y = 0 ∨ z = 0

Tactic:
simpa [hyz, Real.pi_pos.ne.symm, hpi] using h0'

Premises used: Real.pi_pos, Ne.symm, LT.lt.ne
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0wx : w = 0 ∨ x = 0
⊢ y = 0 ∨ z = 0

Tactic:
have h0yz : y = 0 ∨ z = 0 := by
      have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hsyz
      simpa [hyz, Real.pi_pos.ne.symm, hpi] using 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0wx : w = 0 ∨ x = 0
h0yz : y = 0 ∨ z = 0
pos : ∀ (h0wx : w = 0), o.oangle w x = o.oangle y z
pos₁ : ∀ (h0wx : x = 0), o.oangle w x = o.oangle y z
⊢ o.oangle w x = o.oangle y z

Tactic:
rcases h0wx with (h0wx | h0wx)
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0yz : y = 0 ∨ z = 0
h0wx : w = 0
pos : ∀ (h0yz : y = 0), o.oangle w x = o.oangle y z
pos₁ : ∀ (h0yz : z = 0), o.oangle w x = o.oangle y z
⊢ o.oangle w x = o.oangle y z

Tactic:
rcases h0yz with (h0yz | h0yz)
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0yz : y = 0 ∨ z = 0
h0wx : x = 0
pos : ∀ (h0yz : y = 0), o.oangle w x = o.oangle y z
pos₁ : ∀ (h0yz : z = 0), o.oangle w x = o.oangle y z
⊢ o.oangle w x = o.oangle y z

Tactic:
rcases h0yz with (h0yz | h0yz)
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0wx : w = 0
h0yz : y = 0
⊢ o.oangle w x = o.oangle y z

Tactic:
simp [h0wx, h0yz]
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0wx : w = 0
h0yz : z = 0
⊢ o.oangle w x = o.oangle y z

Tactic:
simp [h0wx, h0yz]
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0wx : x = 0
h0yz : y = 0
⊢ o.oangle w x = o.oangle y z

Tactic:
simp [h0wx, h0yz]
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0wx : x = 0
h0yz : z = 0
⊢ o.oangle w x = o.oangle y z

Tactic:
simp [h0wx, h0yz]
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w ≠ 0 ∧ x ≠ 0) ∧ y ≠ 0 ∧ z ≠ 0
neg : |(o.oangle w x).toReal| = |(o.oangle y z).toReal|
⊢ o.oangle w x = o.oangle y z

Tactic:
rw [Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq hs]

Premises used: Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w ≠ 0 ∧ x ≠ 0) ∧ y ≠ 0 ∧ z ≠ 0
neg :
  ∀ (h : |(o.oangle w x).toReal| = InnerProductGeometry.angle y z) (hs : (o.oangle w x).sign = (o.oangle y z).sign)
    (h0 : (w ≠ 0 ∧ x ≠ 0) ∧ y ≠ 0 ∧ z ≠ 0), |(o.oangle w x).toReal| = |(o.oangle y z).toReal|
neg₁ neg₂ neg₃ neg₄ :
  ∀ (h : |(o.oangle w x).toReal| = |(o.oangle y z).toReal|) (hs : (o.oangle w x).sign = (o.oangle y z).sign)
    (h0 : (w ≠ 0 ∧ x ≠ 0) ∧ y ≠ 0 ∧ z ≠ 0), |(o.oangle w x).toReal| = |(o.oangle y z).toReal|
⊢ |(o.oangle w x).toReal| = |(o.oangle y z).toReal|

Tactic:
rwa [o.angle_eq_abs_oangle_toReal h0.1.1 h0.1.2,
      o.angle_eq_abs_oangle_toReal h0.2.1 h0.2.2] at h

Premises used: And.right, And.left, Orientation.angle_eq_abs_oangle_toReal
-- 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)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle y z).sign
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z

Tactic:
⟨fun h => o.oangle_eq_of_angle_eq_of_sign_eq h hs, fun h => ?_⟩

Premises used: Orientation.oangle_eq_of_angle_eq_of_sign_eq, Iff.intro
-- 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)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle y z).sign
refine : ∀ (h : o.oangle w x = o.oangle y z), InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z

Tactic:
refine ⟨fun h => o.oangle_eq_of_angle_eq_of_sign_eq h hs, fun h => ?_⟩
-- 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)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle y z).sign
h : o.oangle w x = o.oangle y z
rw : |(o.oangle w x).toReal| = InnerProductGeometry.angle y z
rw₁ : |(o.oangle w x).toReal| = |(o.oangle y z).toReal|
rw₂ rw₃ : |(o.oangle y z).toReal| = |(o.oangle y z).toReal|
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z

Tactic:
rw [o.angle_eq_abs_oangle_toReal hw hx, o.angle_eq_abs_oangle_toReal hy hz, h]

Premises used: Orientation.angle_eq_abs_oangle_toReal
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = -(o.oangle y z).sign
rw : o.oangle w x = o.oangle z y
⊢ o.oangle w x = -o.oangle y z

Tactic:
rw [← oangle_rev]

Premises used: Orientation.oangle_rev
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = -(o.oangle y z).sign
⊢ (o.oangle w x).sign = (o.oangle z y).sign

Tactic:
rw [← Real.Angle.sign_neg, ← oangle_rev] at hs

Premises used: Real.Angle.sign_neg, Orientation.oangle_rev
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle z y).sign
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle z y

Tactic:
nth_rw 2 [InnerProductGeometry.angle_comm] at h

Premises used: InnerProductGeometry.angle_comm
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle z y).sign
h₁ : InnerProductGeometry.angle w x = InnerProductGeometry.angle z y
⊢ (o.oangle w x).sign = (o.oangle z y).sign

Tactic:
nth_rw 2 [InnerProductGeometry.angle_comm] at h

Premises used: InnerProductGeometry.angle_comm
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle z y
hs : (o.oangle w x).sign = (o.oangle z y).sign
⊢ o.oangle w x = o.oangle z y

Tactic:
o.oangle_eq_of_angle_eq_of_sign_eq h hs

Premises used: Orientation.oangle_eq_of_angle_eq_of_sign_eq
-- 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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle z y
hs : (o.oangle w x).sign = (o.oangle z y).sign
⊢ o.oangle w x = o.oangle z y

Tactic:
exact o.oangle_eq_of_angle_eq_of_sign_eq h hs

Premises used: Orientation.oangle_eq_of_angle_eq_of_sign_eq
-- 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)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = -(o.oangle y z).sign
rw : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle z y
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = -o.oangle y z

Tactic:
rw [← oangle_rev]

Premises used: Orientation.oangle_rev
-- 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)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = -(o.oangle y z).sign
⊢ (o.oangle w x).sign = (o.oangle z y).sign

Tactic:
rw [← Real.Angle.sign_neg, ← oangle_rev] at hs

Premises used: Real.Angle.sign_neg, Orientation.oangle_rev
-- 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)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle z y).sign
nth_rw : InnerProductGeometry.angle w x = InnerProductGeometry.angle z y ↔ o.oangle w x = o.oangle z y
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle z y

Tactic:
nth_rw 2 [InnerProductGeometry.angle_comm]

Premises used: InnerProductGeometry.angle_comm
-- 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)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle z y).sign
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle z y ↔ o.oangle w x = o.oangle z y

Tactic:
o.angle_eq_iff_oangle_eq_of_sign_eq hw hx hz hy hs

Premises used: Orientation.angle_eq_iff_oangle_eq_of_sign_eq
-- 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)
w x y z : V
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle z y).sign
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle z y ↔ o.oangle w x = o.oangle z y

Tactic:
exact o.angle_eq_iff_oangle_eq_of_sign_eq hw hx hz hy hs

Premises used: Orientation.angle_eq_iff_oangle_eq_of_sign_eq
-- 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
h : (o.oangle x y).sign = 1
pos : ∀ (hx : x = 0), o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
neg : ∀ (hx : ¬x = 0), o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
by_cases hx : x = 0
-- 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
h : (o.oangle x y).sign = 1
hx : x = 0
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
simp [hx] at h
-- 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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
pos : ∀ (hy : y = 0), o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
neg : ∀ (hy : ¬y = 0), o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
by_cases hy : y = 0
-- 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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : y = 0
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
simp [hy] at h
-- 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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
(o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_right ?_

Premises used: Orientation.oangle_eq_angle_or_eq_neg_angle, Or.resolve_right
-- 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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : ¬y = 0
neg : ¬o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
refine (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_right ?_

Premises used: Orientation.oangle_eq_angle_or_eq_neg_angle, Or.resolve_right
-- 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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : ¬y = 0
hxy : o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ ¬0 ≤ (↑(InnerProductGeometry.angle x y) : Real.Angle).sign

Tactic:
rw [hxy, Real.Angle.sign_neg, neg_eq_iff_eq_neg, ← SignType.neg_iff, ← not_le] at h

Premises used: not_le, Real.Angle.sign_neg, neg_eq_iff_eq_neg, SignType.neg_iff
-- 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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : ¬y = 0
hxy : o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
h₁ : ¬0 ≤ (↑(InnerProductGeometry.angle x y) : Real.Angle).sign
⊢ ¬x = 0

Tactic:
rw [hxy, Real.Angle.sign_neg, neg_eq_iff_eq_neg, ← SignType.neg_iff, ← not_le] at h

Premises used: not_le, Real.Angle.sign_neg, neg_eq_iff_eq_neg, SignType.neg_iff
-- 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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : ¬y = 0
hxy : o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
h₁ : ¬0 ≤ (↑(InnerProductGeometry.angle x y) : Real.Angle).sign
hx₁ : ¬x = 0
⊢ ¬y = 0

Tactic:
rw [hxy, Real.Angle.sign_neg, neg_eq_iff_eq_neg, ← SignType.neg_iff, ← not_le] at h

Premises used: not_le, Real.Angle.sign_neg, neg_eq_iff_eq_neg, SignType.neg_iff
-- 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
h : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : ¬y = 0
hxy : o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
h₁ : ¬0 ≤ (↑(InnerProductGeometry.angle x y) : Real.Angle).sign
hx₁ : ¬x = 0
hy₁ : ¬y = 0
⊢ o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
rw [hxy, Real.Angle.sign_neg, neg_eq_iff_eq_neg, ← SignType.neg_iff, ← not_le] at h

Premises used: not_le, Real.Angle.sign_neg, neg_eq_iff_eq_neg, SignType.neg_iff