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

Tactic:
h (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _)
    (InnerProductGeometry.angle_le_pi _ _))

Premises used: InnerProductGeometry.angle_le_pi, InnerProductGeometry.angle_nonneg, Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi
-- 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 : ¬0 ≤ (↑(InnerProductGeometry.angle x y) : Real.Angle).sign
hx : ¬x = 0
hy : ¬y = 0
hxy : o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ False

Tactic:
exact h (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _)
    (InnerProductGeometry.angle_le_pi _ _))

Premises used: InnerProductGeometry.angle_le_pi, InnerProductGeometry.angle_nonneg, Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi
-- 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_left ?_

Premises used: Orientation.oangle_eq_angle_or_eq_neg_angle, Or.resolve_left
-- 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_left ?_

Premises used: Orientation.oangle_eq_angle_or_eq_neg_angle, Or.resolve_left
-- 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, ← SignType.neg_iff, ← not_le] at h

Premises used: not_le, 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, ← SignType.neg_iff, ← not_le] at h

Premises used: not_le, 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, ← SignType.neg_iff, ← not_le] at h

Premises used: not_le, 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, ← SignType.neg_iff, ← not_le] at h

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

Tactic:
h (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _)
    (InnerProductGeometry.angle_le_pi _ _))

Premises used: InnerProductGeometry.angle_le_pi, InnerProductGeometry.angle_nonneg, Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi
-- 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 : ¬0 ≤ (↑(InnerProductGeometry.angle x y) : Real.Angle).sign
hx : ¬x = 0
hy : ¬y = 0
hxy : o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ False

Tactic:
exact h (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _)
    (InnerProductGeometry.angle_le_pi _ _))

Premises used: InnerProductGeometry.angle_le_pi, InnerProductGeometry.angle_nonneg, Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi
-- 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
⊢ o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: 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)
x y : V
hx : x ≠ 0
hy : y ≠ 0
refine_1 : ∀ (h : o.oangle x y = 0), InnerProductGeometry.angle x y = 0
refine_2 : ∀ (h : InnerProductGeometry.angle x y = 0), o.oangle x y = 0
⊢ o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0

Tactic:
refine ⟨fun h => ?_, 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)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : o.oangle x y = 0
⊢ InnerProductGeometry.angle x y = 0

Tactic:
simpa [o.angle_eq_abs_oangle_toReal hx hy]

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)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : InnerProductGeometry.angle x y = 0
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle) ∨
    o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
have ha := o.oangle_eq_angle_or_eq_neg_angle hx hy
-- 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
h : InnerProductGeometry.angle x y = 0
ha :
  o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle) ∨
    o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = (↑0 : Real.Angle) ∨ o.oangle x y = -(↑0 : Real.Angle)

Tactic:
rw [h] at ha
-- 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
h : InnerProductGeometry.angle x y = 0
ha : o.oangle x y = (↑0 : Real.Angle) ∨ o.oangle x y = -(↑0 : Real.Angle)
⊢ o.oangle x y = 0

Tactic:
simpa using ha
-- 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
pos : ∀ (hx : x = 0), o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
neg : ∀ (hx : ¬x = 0), o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π

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
hx : x = 0
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π

Tactic:
simp [hx, Real.Angle.pi_ne_zero.symm, div_eq_mul_inv,
      Real.pi_ne_zero]

Premises used: Ne.symm, div_eq_mul_inv, Real.Angle.pi_ne_zero, Real.pi_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)
x y : V
hx : ¬x = 0
pos : ∀ (hy : y = 0), o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
neg : ∀ (hy : ¬y = 0), o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π

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
hx : ¬x = 0
hy : y = 0
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π

Tactic:
simp [hy, Real.Angle.pi_ne_zero.symm, div_eq_mul_inv,
      Real.pi_ne_zero]

Premises used: Ne.symm, div_eq_mul_inv, Real.Angle.pi_ne_zero, Real.pi_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)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: 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)
x y : V
hx : ¬x = 0
hy : ¬y = 0
neg : ∀ (h : o.oangle x y = (↑π : Real.Angle)), InnerProductGeometry.angle x y = π
neg₁ : ∀ (h : InnerProductGeometry.angle x y = π), o.oangle x y = (↑π : Real.Angle)
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π

Tactic:
refine ⟨fun h => ?_, 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)
x y : V
hx : ¬x = 0
hy : ¬y = 0
h : o.oangle x y = (↑π : Real.Angle)
neg : |(↑π : Real.Angle).toReal| = π
⊢ InnerProductGeometry.angle x y = π

Tactic:
rw [o.angle_eq_abs_oangle_toReal hx hy, 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)
x y : V
hx : ¬x = 0
hy : ¬y = 0
h : o.oangle x y = (↑π : Real.Angle)
⊢ |(↑π : Real.Angle).toReal| = π

Tactic:
simp [Real.pi_pos.le]

Premises used: Real.pi_pos, LT.lt.le
-- 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
h : InnerProductGeometry.angle x y = π
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle) ∨
    o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
have ha := o.oangle_eq_angle_or_eq_neg_angle hx hy
-- 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
h : InnerProductGeometry.angle x y = π
ha :
  o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle) ∨
    o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = (↑π : Real.Angle) ∨ o.oangle x y = -(↑π : Real.Angle)

Tactic:
rw [h] at ha
-- 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
h : InnerProductGeometry.angle x y = π
ha : o.oangle x y = (↑π : Real.Angle) ∨ o.oangle x y = -(↑π : Real.Angle)
⊢ o.oangle x y = (↑π : Real.Angle)

Tactic:
simpa using ha
-- 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
pos :
  ∀ (hx : x = 0),
    x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
neg :
  ∀ (hx : ¬x = 0),
    x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0

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
hx : x = 0
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0

Tactic:
simp [hx]
-- 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
pos :
  ∀ (hy : y = 0),
    x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
neg :
  ∀ (hy : ¬y = 0),
    x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0

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
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0

Tactic:
simp [hy]
-- 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
neg :
  o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔
    InnerProductGeometry.angle x y = π / 2
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0

Tactic:
rw [InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, or_iff_right hx, or_iff_right hy]

Premises used: or_iff_right, InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two
-- 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
⊢ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔
    InnerProductGeometry.angle x y = π / 2

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: 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)
x y : V
hx : ¬x = 0
hy : ¬y = 0
neg :
  ∀ (h : o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle)),
    InnerProductGeometry.angle x y = π / 2
neg₁ :
  ∀ (h : InnerProductGeometry.angle x y = π / 2),
    o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle)
⊢ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔
    InnerProductGeometry.angle x y = π / 2

Tactic:
refine ⟨fun h => ?_, 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)
x y : V
hx : ¬x = 0
hy : ¬y = 0
h : o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle)
neg : |(o.oangle x y).toReal| = π / 2
neg₁ neg₂ neg₃ neg₄ : o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle)
⊢ InnerProductGeometry.angle x y = π / 2

Tactic:
rwa [o.angle_eq_abs_oangle_toReal hx hy, Real.Angle.abs_toReal_eq_pi_div_two_iff]

Premises used: Real.Angle.abs_toReal_eq_pi_div_two_iff, 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)
x y : V
hx : ¬x = 0
hy : ¬y = 0
h : InnerProductGeometry.angle x y = π / 2
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle) ∨
    o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
o.oangle_eq_angle_or_eq_neg_angle hx hy

Premises used: Orientation.oangle_eq_angle_or_eq_neg_angle
-- 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
h : InnerProductGeometry.angle x y = π / 2
h₁ : (↑(π / 2) : Real.Angle) = (↑(InnerProductGeometry.angle x y) : Real.Angle)
h₂ : (↑(-π / 2) : Real.Angle) = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle)

Tactic:
convert! o.oangle_eq_angle_or_eq_neg_angle hx hy using 2

Premises used: Orientation.oangle_eq_angle_or_eq_neg_angle
-- 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
h : InnerProductGeometry.angle x y = π / 2
h₁ h₂ : (↑(π / 2) : Real.Angle) = (↑(π / 2) : Real.Angle)
⊢ (↑(π / 2) : Real.Angle) = (↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
rw [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
hx : ¬x = 0
hy : ¬y = 0
h : InnerProductGeometry.angle x y = π / 2
h₁ : (↑(-π / 2) : Real.Angle) = -(↑(π / 2) : Real.Angle)
⊢ (↑(-π / 2) : Real.Angle) = -(↑(InnerProductGeometry.angle x y) : Real.Angle)

Tactic:
rw [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
hx : ¬x = 0
hy : ¬y = 0
h : InnerProductGeometry.angle x y = π / 2
⊢ (↑(-π / 2) : Real.Angle) = -(↑(π / 2) : Real.Angle)

Tactic:
simp only [neg_div, Real.Angle.coe_neg]

Premises used: neg_div, Real.Angle.coe_neg
-- 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 = (↑(π / 2) : Real.Angle)
⊢ ⟪x, y⟫ = 0

Tactic:
o.eq_zero_or_oangle_eq_iff_inner_eq_zero.1 <| Or.inr <| Or.inr <| Or.inl h

Premises used: Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero, Iff.mp, Or.inl, Or.inr
-- 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 = (↑(π / 2) : Real.Angle)
rw : ⟪x, y⟫ = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ⟪y, x⟫ = 0

Tactic:
rw [real_inner_comm, o.inner_eq_zero_of_oangle_eq_pi_div_two h]

Premises used: Orientation.inner_eq_zero_of_oangle_eq_pi_div_two, real_inner_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)
x y : V
h : o.oangle x y = (↑(-π / 2) : Real.Angle)
⊢ ⟪x, y⟫ = 0

Tactic:
o.eq_zero_or_oangle_eq_iff_inner_eq_zero.1 <| Or.inr <| Or.inr <| Or.inr h

Premises used: Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero, Iff.mp, Or.inr
-- 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 = (↑(-π / 2) : Real.Angle)
rw : ⟪x, y⟫ = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ⟪y, x⟫ = 0

Tactic:
rw [real_inner_comm, o.inner_eq_zero_of_oangle_eq_neg_pi_div_two h]

Premises used: Orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two, real_inner_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)
x y : V
pos : ∀ (hx : x = 0), (o.oangle (-x) y).sign = -(o.oangle x y).sign
neg : ∀ (hx : ¬x = 0), (o.oangle (-x) y).sign = -(o.oangle x y).sign
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

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
hx : x = 0
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

Tactic:
simp [hx]