awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : dist p₃ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).tan = dist p₁ p₂
rw₁ : dist p₃ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).tan = dist p₁ p₂
rw₂ : dist p₃ p₂ / Real.tan (∠ p₂ p₁ p₃) = dist p₁ p₂
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂
have rw₃ : dist p₁ p₂ = dist p₁ p₂
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    dist_div_tan_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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 y : V
⊢ inner ℝ (E := V)
      ((HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id + θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V) :
            (a : V) → V)
          x :
        V)
      ((HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id + θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V) :
            (a : V) → V)
          y :
        V) =
    ⟪x, y⟫
have simp : θ.cos *
      (θ.cos * ⟪x, y⟫ +
        HMul.hMul (β := ℝ) θ.sin ((((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ)) +
    θ.sin *
      (HMul.hMul (β := ℝ) θ.cos (-(((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ) +
        θ.sin * - -⟪x, y⟫) =
  ⟪x, y⟫
Tactic: simp only [RCLike.conj_to_real, id, LinearMap.smul_apply, LinearMap.add_apply,
        LinearMap.id_coe, LinearEquiv.coe_coe, LinearIsometryEquiv.coe_toLinearEquiv,
        Orientation.areaForm_rightAngleRotation_left, Orientation.inner_rightAngleRotation_left,
        Orientation.inner_rightAngleRotation_right, inner_add_left, inner_smul_left,
        inner_add_right, inner_smul_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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
⊢ (o.rotationAux θ).toLinearMap ∘ₗ
      (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id - θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) =
    LinearMap.id
have h : ∀ (x : V),
  Eq (α := V)
    (((o.rotationAux θ).toLinearMap ∘ₗ
            (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id -
              θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) :
          (a : V) → V)
        x :
      V)
    ((LinearMap.id : (a : V) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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
⊢ Eq (α := V)
    (((o.rotationAux θ).toLinearMap ∘ₗ
            (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id -
              θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) :
          (a : V) → V)
        x :
      V)
    ((LinearMap.id : (a : V) → V) x : V)
have h : ((o.rotationAux θ).toLinearMap ∘ₗ
        (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id - θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) :
      (a : V) → V)
    x =
  (HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2) • x
Tactic: convert! congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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 :
  ((o.rotationAux θ).toLinearMap ∘ₗ
          (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id -
            θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) :
        (a : V) → V)
      x =
    (HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2) • x
⊢ Eq (α := V)
    (((o.rotationAux θ).toLinearMap ∘ₗ
            (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id -
              θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) :
          (a : V) → V)
        x :
      V)
    ((LinearMap.id : (a : V) → V) x : V)
have h₁ : (LinearMap.id : (a : V) → V) x = HSMul.hSMul (α := ℝ) 1 x
Tactic: convert! congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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
⊢ ((o.rotationAux θ).toLinearMap ∘ₗ
          (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id -
            θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) :
        (a : V) → V)
      x =
    (HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2) • x
have 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
Tactic: simp only [o.rightAngleRotation_rightAngleRotation, o.rotationAux_apply,
          Function.comp_apply, id, LinearEquiv.coe_coe, LinearIsometry.coe_toLinearMap,
          LinearIsometryEquiv.coe_toLinearEquiv, map_smul, map_sub, LinearMap.coe_comp,
          LinearMap.id_coe, LinearMap.smul_apply, LinearMap.sub_apply]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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
⊢ (HSMul.hSMul (β := V →ₗ[ℝ] V) θ.cos LinearMap.id - θ.sin • (↑o.rightAngleRotation.toLinearEquiv : V →ₗ[ℝ] V)) ∘ₗ
      (o.rotationAux θ).toLinearMap =
    LinearMap.id
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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
⊢ 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)
have 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
Tactic: convert! congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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
⊢ 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)
have h₁ : (LinearMap.id : (a : V) → V) x = HSMul.hSMul (α := ℝ) 1 x
Tactic: convert! congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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
⊢ ((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
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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
⊢ (↑(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) ℝ)
have 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)
Tactic: apply (o.basisRightAngleRotation x hx).ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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
⊢ 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)
have 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, sorry⟩) : 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, sorry⟩) : V) :
    V)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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)
⊢ 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)
have 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, sorry⟩) : 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, sorry⟩) : V) :
    V)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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)
    ((((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)
have 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, sorry⟩) : V) :
    V)
  (∑ j : Fin 2,
      HSMul.hSMul (α := ℝ) (β := V) (!![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : ℝ)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) j : V) :
    V)
Tactic: rw [Matrix.toLin_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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)
    ((((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)
have 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, sorry⟩) : V) :
    V)
  (∑ j : Fin 2,
      HSMul.hSMul (α := ℝ) (β := V) (!![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : ℝ)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) j : V) :
    V)
Tactic: rw [Matrix.toLin_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (hypothesis)
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 (α := ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : ℝ) (1 : ℝ)
have this : Nontrivial V
Tactic: haveI : Nontrivial V := nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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
⊢ Eq (α := ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : ℝ) (1 : ℝ)
have obtain : ∀ (x : V) (hx : x ≠ 0),
  Eq (α := ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : ℝ) (1 : ℝ)
Tactic: obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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) → ℝ) (↑(o.rotation θ).toLinearEquiv : V →ₗ[ℝ] V) : ℝ) (1 : ℝ)
have 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 : ℝ)
Tactic: rw [o.rotation_eq_matrix_toLin θ hx]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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
⊢ (o.rotation θ).symm = o.rotation (-θ)
have h : ∀ (x : V), Eq (α := V) (((o.rotation θ).symm : (a : V) → V) x : V) ((o.rotation (-θ) : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
⊢ o.rotation 0 = LinearIsometryEquiv.refl ℝ V
have h : ∀ (x : V), Eq (α := V) ((o.rotation 0 : (a : V) → V) x : V) ((LinearIsometryEquiv.refl ℝ V : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
⊢ o.rotation (↑π : Real.Angle) = LinearIsometryEquiv.neg ℝ
have h : ∀ (x : V),
  Eq (α := V) ((o.rotation (↑π : Real.Angle) : (a : V) → V) x : V) ((LinearIsometryEquiv.neg ℝ : (a : V) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
⊢ o.rotation (↑(π / 2) : Real.Angle) = o.rightAngleRotation
have h : ∀ (x : V),
  Eq (α := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ((o.rightAngleRotation : (a : V) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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) ((o.rotation θ₂ : (a : V) → V) x : V) : V)
    ((o.rotation (θ₁ + θ₂) : (a : V) → V) x : V)
have 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)
Tactic: simp only [o.rotation_apply, Real.Angle.cos_add, Real.Angle.sin_add, map_add,
    map_smul, rightAngleRotation_rightAngleRotation]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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 θ₁).trans (o.rotation θ₂) : (a : V) → V) x : V) ((o.rotation (θ₂ + θ₁) : (a : V) → V) x : V)
have 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)
Tactic: rw [← rotation_rotation, LinearIsometryEquiv.trans_apply]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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)
⊢ Eq (α := V) (((o.rotation θ₁).trans (o.rotation θ₂) : (a : V) → V) x : V) ((o.rotation (θ₂ + θ₁) : (a : V) → V) x : V)
have 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)
Tactic: rw [← rotation_rotation, LinearIsometryEquiv.trans_apply]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
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 (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑θ.toCircle : ℂ) : ℂ)
      ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)
have 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 : ℂ)
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]