awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ θ.cos • (θ.cos • x - HSMul.hSMul (β := V) θ.sin ((o.rightAngleRotation : (a : V) → V) x : V)) +
      θ.sin • (HSMul.hSMul (β := V) θ.cos ((o.rightAngleRotation : (a : V) → V) x : V) - θ.sin • -x) =
    (HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2) • x

Tactic:
module
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ (LinearMap.id : (a : V) → V) x = HSMul.hSMul (α := ℝ) 1 x

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
h :
  ∀ (x : V),
    Eq (α := V)
      (((HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id - θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) ∘ₗ
              (o.rotationAux θ).toLinearMap :
            (a : V) → V)
          x :
        V)
      ((LinearMap.id : (a : V) → V) x : V)
⊢ (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id - θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) ∘ₗ
      (o.rotationAux θ).toLinearMap =
    LinearMap.id

Tactic:
ext x
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
h :
  ((HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id - θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) ∘ₗ
          (o.rotationAux θ).toLinearMap :
        (a : V) → V)
      x =
    (HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2) • x
h₁ : (LinearMap.id : (a : V) → V) x = HSMul.hSMul (α := ℝ) 1 x
⊢ Eq (α := V)
    (((HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id - θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) ∘ₗ
            (o.rotationAux θ).toLinearMap :
          (a : V) → V)
        x :
      V)
    ((LinearMap.id : (a : V) → V) x : V)

Tactic:
convert! congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1

Premises used: Real.Angle.cos_sq_add_sin_sq, congr_arg, HSMul.hSMul
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
h :
  θ.cos • (θ.cos • x - HSMul.hSMul (β := V) θ.sin ((o.rightAngleRotation : (a : V) → V) x : V)) +
      θ.sin • (HSMul.hSMul (β := V) θ.cos ((o.rightAngleRotation : (a : V) → V) x : V) - θ.sin • -x) =
    (HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2) • x
⊢ ((HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id - θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) ∘ₗ
          (o.rotationAux θ).toLinearMap :
        (a : V) → V)
      x =
    (HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2) • x

Tactic:
simp only [o.rightAngleRotation_rightAngleRotation, o.rotationAux_apply,
          Function.comp_apply, id, LinearEquiv.coe_coe, LinearIsometry.coe_toLinearMap,
          LinearIsometryEquiv.coe_toLinearEquiv, map_add, map_smul, LinearMap.coe_comp,
          LinearMap.id_coe, LinearMap.smul_apply, LinearMap.sub_apply]

Premises used: LinearIsometry.coe_toLinearMap, LinearMap.smul_apply, LinearMap.id_coe, LinearIsometryEquiv.coe_toLinearEquiv, map_add, id, Orientation.rightAngleRotation_rightAngleRotation, LinearMap.coe_comp, LinearMap.sub_apply, Function.comp_apply, Orientation.rotationAux_apply, LinearEquiv.coe_coe, map_smul
-- 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
⊢ (o.rotation θ : (a : V) → V) x = θ.cos • x + HSMul.hSMul (β := V) θ.sin ((o.rightAngleRotation : (a : V) → V) x : V)

Tactic:
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)
θ : Real.Angle
x : V
⊢ ((o.rotation θ).symm : (a : V) → V) x =
    θ.cos • x - HSMul.hSMul (β := V) θ.sin ((o.rightAngleRotation : (a : V) → V) x : V)

Tactic:
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)
θ : Real.Angle
x : V
hx : x ≠ 0
apply :
  ∀ (i : Fin 2),
    Eq (α := V)
      (((↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
          ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) :
        V)
      ((((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx) :
                  (a : Matrix (Fin 2) (Fin 2) ℝ) → V →ₗ[ℝ] V)
                (!![θ.cos, -θ.sin; θ.sin, θ.cos] : Matrix (Fin 2) (Fin 2) ℝ) :
              V →ₗ[ℝ] V) :
            (a : V) → V)
          ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) :
        V)
⊢ (↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) =
    (Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx) :
        (a : Matrix (Fin 2) (Fin 2) ℝ) → V →ₗ[ℝ] V)
      (!![θ.cos, -θ.sin; θ.sin, θ.cos] : Matrix (Fin 2) (Fin 2) ℝ)

Tactic:
apply (o.basisRightAngleRotation x hx).ext

Premises used: Orientation.basisRightAngleRotation, Module.Basis.ext
-- 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
hx : x ≠ 0
i : Fin 2
0 :
  Eq (α := V)
    (((↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : V) :
      V)
    ((((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx) :
                (a : Matrix (Fin 2) (Fin 2) ℝ) → V →ₗ[ℝ] V)
              (!![θ.cos, -θ.sin; θ.sin, θ.cos] : Matrix (Fin 2) (Fin 2) ℝ) :
            V →ₗ[ℝ] V) :
          (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : V) :
      V)
1 :
  Eq (α := V)
    (((↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : V) :
      V)
    ((((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx) :
                (a : Matrix (Fin 2) (Fin 2) ℝ) → V →ₗ[ℝ] V)
              (!![θ.cos, -θ.sin; θ.sin, θ.cos] : Matrix (Fin 2) (Fin 2) ℝ) :
            V →ₗ[ℝ] V) :
          (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : V) :
      V)
⊢ Eq (α := V)
    (((↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) :
      V)
    ((((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx) :
                (a : Matrix (Fin 2) (Fin 2) ℝ) → V →ₗ[ℝ] V)
              (!![θ.cos, -θ.sin; θ.sin, θ.cos] : Matrix (Fin 2) (Fin 2) ℝ) :
            V →ₗ[ℝ] V) :
          (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) :
      V)

Tactic:
fin_cases i
-- 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
hx : x ≠ 0
0 :
  Eq (α := V)
    (((↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : V) :
      V)
    (∑ j : Fin 2,
        HSMul.hSMul (α := ℝ) (β := V) (!![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)
          ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) j : V) :
      V)
⊢ Eq (α := V)
    (((↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : V) :
      V)
    ((((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx) :
                (a : Matrix (Fin 2) (Fin 2) ℝ) → V →ₗ[ℝ] V)
              (!![θ.cos, -θ.sin; θ.sin, θ.cos] : Matrix (Fin 2) (Fin 2) ℝ) :
            V →ₗ[ℝ] V) :
          (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : V) :
      V)

Tactic:
rw [Matrix.toLin_self]

Premises used: Matrix.toLin_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)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ Eq (α := V)
    (((↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : V) :
      V)
    (∑ j : Fin 2,
        HSMul.hSMul (α := ℝ) (β := V) (!![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)
          ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) j : V) :
      V)

Tactic:
simp [rotation_apply, Fin.sum_univ_succ]

Premises used: Orientation.rotation_apply, Fin.sum_univ_succ
-- 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
hx : x ≠ 0
1 :
  Eq (α := V)
    (((↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : V) :
      V)
    (∑ j : Fin 2,
        HSMul.hSMul (α := ℝ) (β := V) (!![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℝ)
          ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) j : V) :
      V)
⊢ Eq (α := V)
    (((↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : V) :
      V)
    ((((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx) :
                (a : Matrix (Fin 2) (Fin 2) ℝ) → V →ₗ[ℝ] V)
              (!![θ.cos, -θ.sin; θ.sin, θ.cos] : Matrix (Fin 2) (Fin 2) ℝ) :
            V →ₗ[ℝ] V) :
          (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : V) :
      V)

Tactic:
rw [Matrix.toLin_self]

Premises used: Matrix.toLin_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)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ Eq (α := V)
    (((↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : V) :
      V)
    (∑ j : Fin 2,
        HSMul.hSMul (α := ℝ) (β := V) (!![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℝ)
          ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) j : V) :
      V)

Tactic:
simp [rotation_apply, Fin.sum_univ_succ, add_comm]

Premises used: add_comm, Orientation.rotation_apply, Fin.sum_univ_succ
-- 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
⊢ Nontrivial V

Tactic:
haveI : Nontrivial V := nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _)
-- 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
this : Nontrivial V
⊢ ∃ (x : V), x ≠ 0

Tactic:
exists_ne (0 : V)

Premises used: exists_ne, OfNat.ofNat
-- 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
this : Nontrivial V
obtain :
  ∀ (x : V) (hx : x ≠ 0),
    Eq (α := ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : ℝ) (1 : ℝ)

Tactic:
obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)

Premises used: exists_ne, OfNat.ofNat
-- 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
this : Nontrivial V
x : V
hx : x ≠ 0
rw :
  Eq (α := ℝ)
    ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ)
        ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx) :
              (a : Matrix (Fin 2) (Fin 2) ℝ) → V →ₗ[ℝ] V)
            (!![θ.cos, -θ.sin; θ.sin, θ.cos] : Matrix (Fin 2) (Fin 2) ℝ) :
          V →ₗ[ℝ] V) :
      ℝ)
    (1 : ℝ)
⊢ Eq (α := ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : ℝ) (1 : ℝ)

Tactic:
rw [o.rotation_eq_matrix_toLin θ hx]

Premises used: Orientation.rotation_eq_matrix_toLin
-- 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
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ Eq (α := ℝ)
    ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ)
        ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx) :
              (a : Matrix (Fin 2) (Fin 2) ℝ) → V →ₗ[ℝ] V)
            (!![θ.cos, -θ.sin; θ.sin, θ.cos] : Matrix (Fin 2) (Fin 2) ℝ) :
          V →ₗ[ℝ] V) :
      ℝ)
    (1 : ℝ)

Tactic:
simpa [sq] using θ.cos_sq_add_sin_sq

Premises used: Real.Angle.cos_sq_add_sin_sq, sq
-- 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
⊢ Eq (α := ℝ) (↑(((LinearEquiv.det : (V ≃ₗ[ℝ] V) →* ℝˣ) : (a : V ≃ₗ[ℝ] V) → ℝˣ) (o.rotation θ).toLinearEquiv) : ℝ)
    (↑1 : ℝ)

Tactic:
simpa only [LinearEquiv.coe_det, Units.val_one] using o.det_rotation θ

Premises used: Orientation.det_rotation, Units.val_one, LinearEquiv.coe_det
-- 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
h : ∀ (x : V), Eq (α := V) (((o.rotation θ).symm : (a : V) → V) x : V) ((o.rotation (-θ) : (a : V) → V) x : V)
⊢ (o.rotation θ).symm = o.rotation (-θ)

Tactic:
ext
-- 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 θ).symm : (a : V) → V) x : V) ((o.rotation (-θ) : (a : V) → V) x : V)

Tactic:
simp [o.rotation_apply, o.rotation_symm_apply, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Orientation.rotation_apply, Orientation.rotation_symm_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)
h : ∀ (x : V), Eq (α := V) ((o.rotation 0 : (a : V) → V) x : V) ((LinearIsometryEquiv.refl ℝ V : (a : V) → V) x : V)
⊢ o.rotation 0 = LinearIsometryEquiv.refl ℝ V

Tactic:
ext
-- 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 0 : (a : V) → V) x : V) ((LinearIsometryEquiv.refl ℝ V : (a : V) → V) x : V)

Tactic:
simp [rotation]

Premises used: Orientation.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)
h :
  ∀ (x : V),
    Eq (α := V) ((o.rotation (↑π : Real.Angle) : (a : V) → V) x : V) ((LinearIsometryEquiv.neg ℝ : (a : V) → V) x : V)
⊢ o.rotation (↑π : Real.Angle) = LinearIsometryEquiv.neg ℝ

Tactic:
ext x
-- 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 (↑π : Real.Angle) : (a : V) → V) x : V) ((LinearIsometryEquiv.neg ℝ : (a : V) → V) x : V)

Tactic:
simp [rotation]

Premises used: Orientation.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)
x : V
⊢ (o.rotation (↑π : Real.Angle) : (a : V) → V) x = -x

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)
h :
  ∀ (x : V),
    Eq (α := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ((o.rightAngleRotation : (a : V) → V) x : V)
⊢ o.rotation (↑(π / 2) : Real.Angle) = o.rightAngleRotation

Tactic:
ext x
-- 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.rightAngleRotation : (a : V) → V) x : V)

Tactic:
simp [rotation]

Premises used: Orientation.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
simp :
  θ₁.cos • (θ₂.cos • x + HSMul.hSMul (β := V) θ₂.sin ((o.rightAngleRotation : (a : V) → V) x : V)) +
      θ₁.sin • (HSMul.hSMul (β := V) θ₂.cos ((o.rightAngleRotation : (a : V) → V) x : V) + θ₂.sin • -x) =
    (θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin) • x +
      HSMul.hSMul (β := V) (θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin) ((o.rightAngleRotation : (a : V) → V) x : V)
⊢ Eq (α := V) ((o.rotation θ₁ : (a : V) → V) ((o.rotation θ₂ : (a : V) → V) x : V) : V)
    ((o.rotation (θ₁ + θ₂) : (a : V) → V) x : V)

Tactic:
simp only [o.rotation_apply, Real.Angle.cos_add, Real.Angle.sin_add, map_add,
    map_smul, rightAngleRotation_rightAngleRotation]

Premises used: Real.Angle.cos_add, map_add, Orientation.rightAngleRotation_rightAngleRotation, Real.Angle.sin_add, Orientation.rotation_apply, map_smul
-- 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
⊢ θ₁.cos • (θ₂.cos • x + HSMul.hSMul (β := V) θ₂.sin ((o.rightAngleRotation : (a : V) → V) x : V)) +
      θ₁.sin • (HSMul.hSMul (β := V) θ₂.cos ((o.rightAngleRotation : (a : V) → V) x : V) + θ₂.sin • -x) =
    (θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin) • x +
      HSMul.hSMul (β := V) (θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin) ((o.rightAngleRotation : (a : V) → V) x : V)

Tactic:
module
-- 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
rw :
  Eq (α := V) (((o.rotation θ₁).trans (o.rotation θ₂) : (a : V) → V) x : V)
    ((o.rotation θ₂ : (a : V) → V) ((o.rotation θ₁ : (a : V) → V) x : V) : V)
rw₁ rw₂ :
  Eq (α := V) ((o.rotation θ₂ : (a : V) → V) ((o.rotation θ₁ : (a : V) → V) x : V) : V)
    ((o.rotation θ₂ : (a : V) → V) ((o.rotation θ₁ : (a : V) → V) x : V) : V)
⊢ Eq (α := V) (((o.rotation θ₁).trans (o.rotation θ₂) : (a : V) → V) x : V) ((o.rotation (θ₂ + θ₁) : (a : V) → V) x : V)

Tactic:
rw [← rotation_rotation, LinearIsometryEquiv.trans_apply]

Premises used: Orientation.rotation_rotation, LinearIsometryEquiv.trans_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 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 →ₗ[ℝ] ℂ) ((o.rotation θ : (a : V) → V) x : V) : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑θ.toCircle : ℂ) : ℂ)
      ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)

Tactic:
simp only [o.rotation_apply, map_add, map_mul, map_smulₛₗ, RingHom.id_apply,
    LinearMap.add_apply, LinearMap.smul_apply, real_smul, kahler_rightAngleRotation_left,
    Real.Angle.coe_toCircle, Complex.conj_ofReal, conj_I]

Premises used: Complex.real_smul, RingHom.id_apply, LinearMap.smul_apply, LinearMap.add_apply, Real.Angle.coe_toCircle, map_add, MulActionSemiHomClass.map_smulₛₗ, map_mul, Orientation.kahler_rightAngleRotation_left, Orientation.rotation_apply, Complex.conj_ofReal, Complex.conj_I
-- 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)
θ : Real.Angle
x : V
rw :
  Eq (α := V) ((o.rotation (↑π : Real.Angle) : (a : V) → V) ((o.rotation θ : (a : V) → V) x : V) : V)
    ((o.rotation ((↑π : Real.Angle) + θ) : (a : V) → V) x : V)
rw₁ rw₂ :
  Eq (α := V) ((o.rotation ((↑π : Real.Angle) + θ) : (a : V) → V) x : V)
    ((o.rotation ((↑π : Real.Angle) + θ) : (a : V) → V) x : V)
⊢ Eq (α := V) (-(o.rotation θ : (a : V) → V) x : V) ((o.rotation ((↑π : Real.Angle) + θ) : (a : V) → V) x : V)

Tactic:
rw [← o.rotation_pi_apply, rotation_rotation]

Premises used: Orientation.rotation_pi_apply, Orientation.rotation_rotation