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)
x : V
rw :
  Eq (α := V) ((o.rotation ((↑π : Real.Angle) + (↑(-π / 2) : Real.Angle)) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
rw₁ :
  Eq (α := V) ((o.rotation (↑(π + -π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
rw₂ :
  Eq (α := V) ((o.rotation (↑(π + -(π / 2)) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
rw₃ :
  Eq (α := V) ((o.rotation (↑(π - π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
rw₄ rw₅ :
  Eq (α := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
⊢ Eq (α := V) (-(o.rotation (↑(-π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)

Tactic:
rw [neg_rotation, ← Real.Angle.coe_add, neg_div, ← sub_eq_add_neg, sub_half]

Premises used: Orientation.neg_rotation, neg_div, Real.Angle.coe_add, sub_eq_add_neg, sub_half
-- 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
⊢ Eq (α := V) (-(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(-π / 2) : Real.Angle) : (a : V) → V) x : V)

Tactic:
(neg_eq_iff_eq_neg.mp <| o.neg_rotation_neg_pi_div_two _).symm

Premises used: Orientation.neg_rotation_neg_pi_div_two, neg_eq_iff_eq_neg, Iff.mp, Eq.symm
-- 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
θ : Real.Angle
⊢ (((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) ((o.rotation θ : (a : V) → V) x : V) : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y =
    HMul.hMul (β := ℂ) (↑(-θ).toCircle : ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)

Tactic:
simp only [Real.Angle.toCircle_neg, Circle.coe_inv_eq_conj, kahler_rotation_left]

Premises used: Circle.coe_inv_eq_conj, Orientation.kahler_rotation_left, Real.Angle.toCircle_neg
-- 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
θ : Real.Angle
simp :
  HMul.hMul (β := ℂ) (↑θ.cos : ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) +
      (↑θ.sin : ℂ) * HMul.hMul (β := ℂ) I ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) =
    HMul.hMul (β := ℂ) ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)
      ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)
⊢ (((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) y : V) =
    HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)

Tactic:
simp only [o.rotation_apply, map_add, map_smulₛₗ, RingHom.id_apply, real_smul,
    kahler_rightAngleRotation_right, Real.Angle.coe_toCircle]

Premises used: Complex.real_smul, RingHom.id_apply, Real.Angle.coe_toCircle, map_add, MulActionSemiHomClass.map_smulₛₗ, Orientation.rotation_apply, Orientation.kahler_rightAngleRotation_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 y : V
θ : Real.Angle
⊢ HMul.hMul (β := ℂ) (↑θ.cos : ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) +
      (↑θ.sin : ℂ) * HMul.hMul (β := ℂ) I ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) =
    HMul.hMul (β := ℂ) ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)
      ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)

Tactic:
ring
-- 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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
simp :
  (↑(HMul.hMul (β := ℂ) (↑(-θ).toCircle : ℂ)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) - θ
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) y = o.oangle x y - θ

Tactic:
simp only [oangle, o.kahler_rotation_left']

Premises used: Orientation.oangle, Orientation.kahler_rotation_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 y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
rw :
  -θ + (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) - θ
hx₁ : (↑(-θ).toCircle : ℂ) ≠ 0
hy₁ : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
⊢ (↑(HMul.hMul (β := ℂ) (↑(-θ).toCircle : ℂ)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) - θ

Tactic:
rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]

Premises used: Real.Angle.arg_toCircle, Complex.arg_mul_coe_angle
-- 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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ -θ + (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) - θ

Tactic:
abel
-- 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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (↑(-θ).toCircle : ℂ) ≠ 0

Tactic:
Circle.coe_ne_zero _

Premises used: Circle.coe_ne_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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (↑(-θ).toCircle : ℂ) ≠ 0

Tactic:
exact Circle.coe_ne_zero _

Premises used: Circle.coe_ne_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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)

Tactic:
o.kahler_ne_zero hx hy

Premises used: Orientation.kahler_ne_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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)

Tactic:
exact o.kahler_ne_zero hx hy

Premises used: Orientation.kahler_ne_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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
simp :
  (↑(HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + θ
⊢ o.oangle x ((o.rotation θ : (a : V) → V) y) = o.oangle x y + θ

Tactic:
simp only [oangle, o.kahler_rotation_right]

Premises used: Orientation.oangle, Orientation.kahler_rotation_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 y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
rw :
  θ + (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + θ
hx₁ : (↑θ.toCircle : ℂ) ≠ 0
hy₁ : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
⊢ (↑(HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + θ

Tactic:
rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]

Premises used: Real.Angle.arg_toCircle, Complex.arg_mul_coe_angle
-- 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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ θ + (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + θ

Tactic:
abel
-- 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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (↑θ.toCircle : ℂ) ≠ 0

Tactic:
Circle.coe_ne_zero _

Premises used: Circle.coe_ne_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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (↑θ.toCircle : ℂ) ≠ 0

Tactic:
exact Circle.coe_ne_zero _

Premises used: Circle.coe_ne_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 : V
hx : x ≠ 0
θ : Real.Angle
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) x = -θ

Tactic:
simp [hx]
-- 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
hx : x ≠ 0
θ : Real.Angle
⊢ o.oangle x ((o.rotation θ : (a : V) → V) x) = θ

Tactic:
simp [hx]
-- 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 : ∀ (hx : x = 0), o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
neg : ∀ (hx : ¬x = 0), o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
⊢ o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0

Tactic:
by_cases hx : x = 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
hx : x = 0
⊢ o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0

Tactic:
simp [hx]
-- 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
hx : ¬x = 0
pos : ∀ (hy : y = 0), o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
neg : ∀ (hy : ¬y = 0), o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
⊢ o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0

Tactic:
by_cases hy : 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
hx : ¬x = 0
hy : y = 0
⊢ o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0

Tactic:
simp [hy]
-- 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
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0

Tactic:
simp [hx, hy]
-- 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
rw : -o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
⊢ o.oangle y ((o.rotation (o.oangle x y) : (a : V) → V) x) = 0

Tactic:
rw [oangle_rev]

Premises used: Orientation.oangle_rev
-- 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
⊢ -o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 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
θ : Real.Angle
pos : ∀ (hx : x = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
neg : ∀ (hx : ¬x = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y

Tactic:
by_cases hx : x = 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
θ : Real.Angle
hx : x = 0
pos : ∀ (hy : y = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
neg : ∀ (hy : ¬y = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y

Tactic:
by_cases hy : 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
θ : Real.Angle
hx : ¬x = 0
pos : ∀ (hy : y = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
neg : ∀ (hy : ¬y = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y

Tactic:
by_cases hy : 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
θ : Real.Angle
hx : x = 0
hy : y = 0
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y

Tactic:
simp [hx, hy]
-- 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
θ : Real.Angle
hx : x = 0
hy : ¬y = 0
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y

Tactic:
simp [hx, hy]
-- 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
θ : Real.Angle
hx : ¬x = 0
hy : y = 0
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y

Tactic:
simp [hx, hy]
-- 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
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y

Tactic:
simp [hx, hy]
-- 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
hx : x ≠ 0
θ : Real.Angle
mp : (o.rotation θ : (a : V) → V) x = x → θ = 0
mpr : θ = 0 → (o.rotation θ : (a : V) → V) x = x
⊢ (o.rotation θ : (a : V) → V) x = x ↔ θ = 0

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 : V
hx : x ≠ 0
θ : Real.Angle
h : (o.rotation θ : (a : V) → V) x = x
mp : 0 = θ
⊢ θ = 0

Tactic:
rw [eq_comm]

Premises used: eq_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
hx : x ≠ 0
θ : Real.Angle
h : (o.rotation θ : (a : V) → V) x = x
⊢ 0 = θ

Tactic:
simpa [hx, h] using o.oangle_rotation_right hx hx θ

Premises used: Orientation.oangle_rotation_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
hx : x ≠ 0
θ : Real.Angle
h : θ = 0
⊢ (o.rotation θ : (a : V) → V) x = x

Tactic:
simp [h]
-- 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
hx : x ≠ 0
θ : Real.Angle
rw : x = (o.rotation θ : (a : V) → V) x ↔ (o.rotation θ : (a : V) → V) x = x
rw₁ rw₂ : (o.rotation θ : (a : V) → V) x = x ↔ (o.rotation θ : (a : V) → V) x = x
⊢ x = (o.rotation θ : (a : V) → V) x ↔ θ = 0

Tactic:
rw [← o.rotation_eq_self_iff_angle_eq_zero hx, eq_comm]

Premises used: eq_comm, Orientation.rotation_eq_self_iff_angle_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 : V
θ : Real.Angle
pos : ∀ (h : x = 0), (o.rotation θ : (a : V) → V) x = x ↔ x = 0 ∨ θ = 0
neg : ∀ (h : ¬x = 0), (o.rotation θ : (a : V) → V) x = x ↔ x = 0 ∨ θ = 0
⊢ (o.rotation θ : (a : V) → V) x = x ↔ x = 0 ∨ θ = 0

Tactic:
by_cases h : x = 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 : V
θ : Real.Angle
h : x = 0
⊢ (o.rotation θ : (a : V) → V) x = x ↔ x = 0 ∨ θ = 0

Tactic:
simp [h]
-- 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
θ : Real.Angle
h : ¬x = 0
⊢ (o.rotation θ : (a : V) → V) x = x ↔ x = 0 ∨ θ = 0

Tactic:
simp [h]
-- 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
θ : Real.Angle
rw : x = (o.rotation θ : (a : V) → V) x ↔ (o.rotation θ : (a : V) → V) x = x
o₁ : Orientation ℝ V (Fin 2)
rw₁ : (o.rotation θ : (a : V) → V) x = x ↔ (o.rotation θ : (a : V) → V) x = x
o₂ : Orientation ℝ V (Fin 2)
rw₂ : (o.rotation θ : (a : V) → V) x = x ↔ (o.rotation θ : (a : V) → V) x = x
o₃ : Orientation ℝ V (Fin 2)
⊢ x = (o.rotation θ : (a : V) → V) x ↔ x = 0 ∨ θ = 0

Tactic:
rw [← rotation_eq_self_iff, eq_comm]

Premises used: Orientation.rotation_eq_self_iff, eq_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
mp : (o.rotation (o.oangle x y) : (a : V) → V) x = y → ‖x‖ = ‖y‖
mpr : ‖x‖ = ‖y‖ → (o.rotation (o.oangle x y) : (a : V) → V) x = y
⊢ (o.rotation (o.oangle x y) : (a : V) → V) x = y ↔ ‖x‖ = ‖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 : (o.rotation (o.oangle x y) : (a : V) → V) x = y
mp : ‖x‖ = norm (E := V) ((o.rotation (o.oangle x y) : (a : V) → V) x : V)
mp₁ mp₂ : ‖x‖ = ‖x‖
⊢ ‖x‖ = ‖y‖

Tactic:
rw [← h, LinearIsometryEquiv.norm_map]

Premises used: LinearIsometryEquiv.norm_map
-- 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‖ = ‖y‖
mpr : o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
mpr₁ : norm (E := V) ((o.rotation (o.oangle x y) : (a : V) → V) x : V) = ‖y‖
⊢ (o.rotation (o.oangle x y) : (a : V) → V) x = y

Tactic:
rw [o.eq_iff_oangle_eq_zero_of_norm_eq]

Premises used: Orientation.eq_iff_oangle_eq_zero_of_norm_eq
-- 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‖ = ‖y‖
⊢ o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0

Tactic:
simp [h]
-- 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‖ = ‖y‖
⊢ norm (E := V) ((o.rotation (o.oangle x y) : (a : V) → V) x : V) = ‖y‖

Tactic:
simp [h]
-- 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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ 0 < ‖y‖ / ‖x‖

Tactic:
have hp := div_pos (norm_pos_iff.2 hy) (norm_pos_iff.2 hx)
-- 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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
mp : o.oangle x y = θ → y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)
mpr : y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) → o.oangle x y = θ
⊢ o.oangle x y = θ ↔ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)

Tactic:
constructor