awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
f : V ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ V (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ V (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x : V
rw :
  Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
    ((Complex.orientation.rotation θ : (a : ℂ) → ℂ) ((f : (a : V) → ℂ) x : ℂ) : ℂ)
rw₁ :
  Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
    ((rotation
            (((map (Fin 2) f.toLinearEquiv : Orientation ℝ V (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
                (a : Orientation ℝ V (Fin 2)) → Orientation ℝ ℂ (Fin 2))
              o)
            θ :
          (a : ℂ) → ℂ)
        ((f : (a : V) → ℂ) x : ℂ) :
      ℂ)
rw₂ :
  Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
    ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) x : ℂ) : V) : V) : ℂ)
rw₃ rw₄ :
  Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
    ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
⊢ (f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) =
    HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ) ((f : (a : V) → ℂ) x : ℂ)

Tactic:
rw [← Complex.rotation, ← hf, o.rotation_map, LinearIsometryEquiv.symm_apply_apply]

Premises used: Orientation.rotation_map, LinearIsometryEquiv.symm_apply_apply, Complex.rotation
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ ∀ (x : V), Eq (α := V) (((-o).rotation θ : (a : V) → V) x : V) ((o.rotation (-θ) : (a : V) → V) x : V)

Tactic:
simp [rotation_apply]

Premises used: Orientation.rotation_apply
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
rw : ⟪(o.rightAngleRotation : (a : V) → V) x, x⟫ = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0

Tactic:
rw [rotation_pi_div_two, inner_rightAngleRotation_self]

Premises used: Orientation.rotation_pi_div_two, Orientation.inner_rightAngleRotation_self
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
rw : ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ⟪x, (o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x⟫ = 0

Tactic:
rw [real_inner_comm, inner_rotation_pi_div_two_left]

Premises used: Orientation.inner_rotation_pi_div_two_left, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 : ℝ
rw :
  HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
rw₁ : HMul.hMul (α := ℝ) (β := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) (0 : ℝ) = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ ⟪HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), x⟫ = 0

Tactic:
rw [inner_smul_left, inner_rotation_pi_div_two_left, mul_zero]

Premises used: Orientation.inner_rotation_pi_div_two_left, MulZeroClass.mul_zero, inner_smul_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 : ℝ
rw : ⟪HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), x⟫ = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ⟪x, HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)⟫ = 0

Tactic:
rw [real_inner_comm, inner_smul_rotation_pi_div_two_left]

Premises used: Orientation.inner_smul_rotation_pi_div_two_left, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 : ℝ
rw : r * ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
rw₁ : r * 0 = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, r • x⟫ = 0

Tactic:
rw [inner_smul_right, inner_rotation_pi_div_two_left, mul_zero]

Premises used: Orientation.inner_rotation_pi_div_two_left, MulZeroClass.mul_zero, inner_smul_right
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 : ℝ
rw : ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, r • x⟫ = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ⟪r • x, (o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x⟫ = 0

Tactic:
rw [real_inner_comm, inner_rotation_pi_div_two_left_smul]

Premises used: Orientation.inner_rotation_pi_div_two_left_smul, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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₁ r₂ : ℝ
rw : r₂ * ⟪HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), x⟫ = 0
rw₁ : r₂ * 0 = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ ⟪HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), r₂ • x⟫ = 0

Tactic:
rw [inner_smul_right, inner_smul_rotation_pi_div_two_left, mul_zero]

Premises used: MulZeroClass.mul_zero, Orientation.inner_smul_rotation_pi_div_two_left, inner_smul_right
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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₁ r₂ : ℝ
rw : ⟪HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), r₂ • x⟫ = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ⟪r₂ • x, HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)⟫ = 0

Tactic:
rw [real_inner_comm, inner_smul_rotation_pi_div_two_smul_left]

Premises used: Orientation.inner_smul_rotation_pi_div_two_smul_left, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 :
  ∀ (H : x = 0 ∨ y = 0),
    ⟪x, y⟫ = 0 ↔
      x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
neg :
  ∀ (H : x ≠ 0 ∧ y ≠ 0),
    ⟪x, y⟫ = 0 ↔
      x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
⊢ ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y

Tactic:
by_cases! +distrib H : x = 0 ∨ y = 0
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 : x = 0 ∨ y = 0
pos :
  ⟪0, y⟫ = 0 ↔
    Eq.{u_1 + 1} (α := V) 0 0 ∨
      ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) 0 : V) = y
pos₁ :
  ⟪x, 0⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = 0
⊢ ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y

Tactic:
rcases H with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
y : V
⊢ ⟪0, y⟫ = 0 ↔
    Eq.{u_1 + 1} (α := V) 0 0 ∨
      ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) 0 : V) = y

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
⊢ ⟪x, 0⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = 0

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 : x ≠ 0 ∧ y ≠ 0
neg :
  ((∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
      ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ↔
    ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
⊢ ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y

Tactic:
simp only [← o.eq_zero_or_oangle_eq_iff_inner_eq_zero, H, ← neg_smul, false_or,
    o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero H.1 H.2, ← o.neg_rotation_pi_div_two, smul_neg]

Premises used: neg_smul, smul_neg, Orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero, false_or, Orientation.neg_rotation_pi_div_two, And.right, And.left, Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 : x ≠ 0 ∧ y ≠ 0
neg :
  ((∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
      ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) →
    ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
neg₁ :
  (∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y) →
    (∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
      ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
⊢ ((∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
      ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ↔
    ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y

Tactic:
constructor
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 : x ≠ 0 ∧ y ≠ 0
⊢ ((∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
      ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) →
    ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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)
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)
⊢ (∃ (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)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 : 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:
grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
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:
simp_all
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
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)
⊢ (∃ (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:
right
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
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)
⊢ ∃ (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:
use -r
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
⊢ 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:
simp_all
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
⊢ x = 0

Tactic:
rw [norm_zero, norm_eq_zero] at hxy

Premises used: norm_eq_zero, norm_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 = 0
⊢ False

Tactic:
hxyne hxy
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 = 0
⊢ False

Tactic:
exact hxyne hxy
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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‖
⊢ y ≠ 0

Tactic:
have hy : y ≠ 0 := by
    rintro rfl
    rw [norm_zero, norm_eq_zero] at hxy
    exact hxyne hxy
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := norm_ne_zero_iff.1 (hxy.symm ▸ norm_ne_zero_iff.2 hy)
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
⊢ z ≠ 0

Tactic:
have hz : z ≠ 0 := norm_ne_zero_iff.1 (hxz ▸ norm_ne_zero_iff.2 hx)
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 = o.oangle x z - o.oangle x y

Tactic:
(o.oangle_sub_left hx hy hz).symm

Premises used: Orientation.oangle_sub_left, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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))
rw₁ 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))
⊢ 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:
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]

Premises used: Ne.symm, Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
⊢ (↑π : 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:
abel
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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 rw₁ : HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) (x - z))
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (x - y) x - o.oangle (x - z) x) = 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]

Premises used: sub_ne_zero_of_ne, Orientation.oangle_sub_right
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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))
rw₂ rw₃ : HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) (z - x)) = 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))

Tactic:
rw [← oangle_neg_neg, neg_sub, neg_sub]

Premises used: neg_sub, Orientation.oangle_neg_neg