-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_eq_matrix_toLin (θ : Real.Angle) {x : V} (hx : x ≠ 0) :
    (o.rotation θ).toLinearMap =
      Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)
        !![θ.cos, -θ.sin; θ.sin, θ.cos]

Proof state:
case «0»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨0, ⋯⟩)) =
    ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos])
      ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨0, ⋯⟩))

Tactic:
rw [Matrix.toLin_self]

Result:
case «0»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨0, ⋯⟩)) =
    ∑ j : Fin 2, !![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun i => i) ⟨0, ⋯⟩) • (o.basisRightAngleRotation x hx) j

Proof state:
case «1»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨1, ⋯⟩)) =
    ∑ j : Fin 2, !![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun i => i) ⟨1, ⋯⟩) • (o.basisRightAngleRotation x hx) j

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

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ∀ (i : Fin 2),
    ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) i) =
      ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos])
        ((o.basisRightAngleRotation x hx) i)

Tactic:
intro i

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
i : Fin 2
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) i) =
    ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos])
      ((o.basisRightAngleRotation x hx) i)

Proof state:
case «0»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨0, ⋯⟩)) =
    ∑ j : Fin 2, !![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun i => i) ⟨0, ⋯⟩) • (o.basisRightAngleRotation x hx) j

Tactic:
simp [rotation_apply, Fin.sum_univ_succ]

Result:
no goals

Proof state:
case «1»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨1, ⋯⟩)) =
    ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos])
      ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨1, ⋯⟩))

Tactic:
rw [Matrix.toLin_self]

Result:
case «1»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨1, ⋯⟩)) =
    ∑ j : Fin 2, !![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun i => i) ⟨1, ⋯⟩) • (o.basisRightAngleRotation x hx) j

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
i : Fin 2
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) i) =
    ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos])
      ((o.basisRightAngleRotation x hx) i)

Tactic:
fin_cases i

Result:
case «0»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨0, ⋯⟩)) =
    ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos])
      ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨0, ⋯⟩))

case «1»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨1, ⋯⟩)) =
    ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos])
      ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨1, ⋯⟩))

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv =
    (Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos]

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

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ∀ (i : Fin 2),
    ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) i) =
      ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos])
        ((o.basisRightAngleRotation x hx) i)