[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ ∀ (x y : V),
    inner (↑(Real.Angle.cos θ • LinearMap.id + Real.Angle.sin θ • ↑(rightAngleRotation o).toLinearEquiv) x)
        (↑(Real.Angle.cos θ • LinearMap.id + Real.Angle.sin θ • ↑(rightAngleRotation o).toLinearEquiv) y) =
      inner x y
[PROOFSTEP]
intro x y
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x y : V
⊢ inner (↑(Real.Angle.cos θ • LinearMap.id + Real.Angle.sin θ • ↑(rightAngleRotation o).toLinearEquiv) x)
      (↑(Real.Angle.cos θ • LinearMap.id + Real.Angle.sin θ • ↑(rightAngleRotation o).toLinearEquiv) y) =
    inner x y
[PROOFSTEP]
simp only [IsROrC.conj_to_real, id.def, 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]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x y : V
⊢ Real.Angle.cos θ * (Real.Angle.cos θ * inner x y + Real.Angle.sin θ * ↑(↑(areaForm o) x) y) +
      Real.Angle.sin θ * (Real.Angle.cos θ * -↑(↑(areaForm o) x) y + Real.Angle.sin θ * - -inner x y) =
    inner x y
[PROOFSTEP]
linear_combination inner (𝕜 := ℝ) x y * θ.cos_sq_add_sin_sq
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ LinearMap.comp (rotationAux o θ).toLinearMap
      (Real.Angle.cos θ • LinearMap.id - Real.Angle.sin θ • ↑(rightAngleRotation o).toLinearEquiv) =
    LinearMap.id
[PROOFSTEP]
ext x
[GOAL]
case h
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ↑(LinearMap.comp (rotationAux o θ).toLinearMap
          (Real.Angle.cos θ • LinearMap.id - Real.Angle.sin θ • ↑(rightAngleRotation o).toLinearEquiv))
      x =
    ↑LinearMap.id x
[PROOFSTEP]
convert congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1
[GOAL]
case h.e'_2
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ↑(LinearMap.comp (rotationAux o θ).toLinearMap
          (Real.Angle.cos θ • LinearMap.id - Real.Angle.sin θ • ↑(rightAngleRotation o).toLinearEquiv))
      x =
    (Real.Angle.cos θ ^ 2 + Real.Angle.sin θ ^ 2) • x
[PROOFSTEP]
simp only [o.rightAngleRotation_rightAngleRotation, o.rotationAux_apply, Function.comp_apply, id.def,
  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, ← mul_smul, add_smul, smul_add,
  smul_neg, smul_sub, mul_comm, sq]
[GOAL]
case h.e'_2
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ (Real.Angle.cos θ * Real.Angle.cos θ) • x + (Real.Angle.cos θ * Real.Angle.sin θ) • ↑(rightAngleRotation o) x -
      ((Real.Angle.cos θ * Real.Angle.sin θ) • ↑(rightAngleRotation o) x +
        -((Real.Angle.sin θ * Real.Angle.sin θ) • x)) =
    (Real.Angle.cos θ * Real.Angle.cos θ) • x + (Real.Angle.sin θ * Real.Angle.sin θ) • x
[PROOFSTEP]
abel
[GOAL]
case h.e'_2
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ (Real.Angle.cos θ * Real.Angle.cos θ) • x + (Real.Angle.cos θ * Real.Angle.sin θ) • ↑(rightAngleRotation o) x -
      ((Real.Angle.cos θ * Real.Angle.sin θ) • ↑(rightAngleRotation o) x +
        -((Real.Angle.sin θ * Real.Angle.sin θ) • x)) =
    (Real.Angle.cos θ * Real.Angle.cos θ) • x + (Real.Angle.sin θ * Real.Angle.sin θ) • x
[PROOFSTEP]
abel
[GOAL]
case h.e'_3
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ↑LinearMap.id x = 1 • x
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ LinearMap.comp (Real.Angle.cos θ • LinearMap.id - Real.Angle.sin θ • ↑(rightAngleRotation o).toLinearEquiv)
      (rotationAux o θ).toLinearMap =
    LinearMap.id
[PROOFSTEP]
ext x
[GOAL]
case h
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ↑(LinearMap.comp (Real.Angle.cos θ • LinearMap.id - Real.Angle.sin θ • ↑(rightAngleRotation o).toLinearEquiv)
          (rotationAux o θ).toLinearMap)
      x =
    ↑LinearMap.id x
[PROOFSTEP]
convert congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1
[GOAL]
case h.e'_2
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ↑(LinearMap.comp (Real.Angle.cos θ • LinearMap.id - Real.Angle.sin θ • ↑(rightAngleRotation o).toLinearEquiv)
          (rotationAux o θ).toLinearMap)
      x =
    (Real.Angle.cos θ ^ 2 + Real.Angle.sin θ ^ 2) • x
[PROOFSTEP]
simp only [o.rightAngleRotation_rightAngleRotation, o.rotationAux_apply, Function.comp_apply, id.def,
  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, add_smul, smul_neg, smul_sub,
  smul_smul]
[GOAL]
case h.e'_2
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ (Real.Angle.cos θ * Real.Angle.cos θ) • x - (Real.Angle.cos θ * Real.Angle.sin θ) • ↑(rightAngleRotation o) x +
      ((Real.Angle.sin θ * Real.Angle.cos θ) • ↑(rightAngleRotation o) x -
        -((Real.Angle.sin θ * Real.Angle.sin θ) • x)) =
    Real.Angle.cos θ ^ 2 • x + Real.Angle.sin θ ^ 2 • x
[PROOFSTEP]
ring_nf
[GOAL]
case h.e'_2
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ Real.Angle.cos θ ^ 2 • x - (Real.Angle.cos θ * Real.Angle.sin θ) • ↑(rightAngleRotation o) x +
      ((Real.Angle.cos θ * Real.Angle.sin θ) • ↑(rightAngleRotation o) x - -(Real.Angle.sin θ ^ 2 • x)) =
    Real.Angle.cos θ ^ 2 • x + Real.Angle.sin θ ^ 2 • x
[PROOFSTEP]
abel
[GOAL]
case h.e'_2
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ Real.Angle.cos θ ^ 2 • x - (Real.Angle.cos θ * Real.Angle.sin θ) • ↑(rightAngleRotation o) x +
      ((Real.Angle.cos θ * Real.Angle.sin θ) • ↑(rightAngleRotation o) x - -(Real.Angle.sin θ ^ 2 • x)) =
    Real.Angle.cos θ ^ 2 • x + Real.Angle.sin θ ^ 2 • x
[PROOFSTEP]
abel
[GOAL]
case h.e'_3
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ↑LinearMap.id x = 1 • x
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(rotation o θ).toLinearEquiv =
    ↑(Matrix.toLin (basisRightAngleRotation o x hx) (basisRightAngleRotation o x hx))
      (↑Matrix.of ![![Real.Angle.cos θ, -Real.Angle.sin θ], ![Real.Angle.sin θ, Real.Angle.cos θ]])
[PROOFSTEP]
apply (o.basisRightAngleRotation x hx).ext
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ∀ (i : Fin 2),
    ↑↑(rotation o θ).toLinearEquiv (↑(basisRightAngleRotation o x hx) i) =
      ↑(↑(Matrix.toLin (basisRightAngleRotation o x hx) (basisRightAngleRotation o x hx))
            (↑Matrix.of ![![Real.Angle.cos θ, -Real.Angle.sin θ], ![Real.Angle.sin θ, Real.Angle.cos θ]]))
        (↑(basisRightAngleRotation o x hx) i)
[PROOFSTEP]
intro i
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
i : Fin 2
⊢ ↑↑(rotation o θ).toLinearEquiv (↑(basisRightAngleRotation o x hx) i) =
    ↑(↑(Matrix.toLin (basisRightAngleRotation o x hx) (basisRightAngleRotation o x hx))
          (↑Matrix.of ![![Real.Angle.cos θ, -Real.Angle.sin θ], ![Real.Angle.sin θ, Real.Angle.cos θ]]))
      (↑(basisRightAngleRotation o x hx) i)
[PROOFSTEP]
fin_cases i
[GOAL]
case head
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑↑(rotation o θ).toLinearEquiv (↑(basisRightAngleRotation o x hx) { val := 0, isLt := (_ : 0 < 2) }) =
    ↑(↑(Matrix.toLin (basisRightAngleRotation o x hx) (basisRightAngleRotation o x hx))
          (↑Matrix.of ![![Real.Angle.cos θ, -Real.Angle.sin θ], ![Real.Angle.sin θ, Real.Angle.cos θ]]))
      (↑(basisRightAngleRotation o x hx) { val := 0, isLt := (_ : 0 < 2) })
[PROOFSTEP]
rw [Matrix.toLin_self]
[GOAL]
case head
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑↑(rotation o θ).toLinearEquiv (↑(basisRightAngleRotation o x hx) { val := 0, isLt := (_ : 0 < 2) }) =
    Finset.sum Finset.univ fun j =>
      ↑Matrix.of ![![Real.Angle.cos θ, -Real.Angle.sin θ], ![Real.Angle.sin θ, Real.Angle.cos θ]] j
          { val := 0, isLt := (_ : 0 < 2) } •
        ↑(basisRightAngleRotation o x hx) j
[PROOFSTEP]
simp [rotation_apply, Fin.sum_univ_succ]
[GOAL]
case tail.head
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑↑(rotation o θ).toLinearEquiv (↑(basisRightAngleRotation o x hx) { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑(↑(Matrix.toLin (basisRightAngleRotation o x hx) (basisRightAngleRotation o x hx))
          (↑Matrix.of ![![Real.Angle.cos θ, -Real.Angle.sin θ], ![Real.Angle.sin θ, Real.Angle.cos θ]]))
      (↑(basisRightAngleRotation o x hx) { val := 1, isLt := (_ : (fun a => a < 2) 1) })
[PROOFSTEP]
rw [Matrix.toLin_self]
[GOAL]
case tail.head
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑↑(rotation o θ).toLinearEquiv (↑(basisRightAngleRotation o x hx) { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    Finset.sum Finset.univ fun j =>
      ↑Matrix.of ![![Real.Angle.cos θ, -Real.Angle.sin θ], ![Real.Angle.sin θ, Real.Angle.cos θ]] j
          { val := 1, isLt := (_ : (fun a => a < 2) 1) } •
        ↑(basisRightAngleRotation o x hx) j
[PROOFSTEP]
simp [rotation_apply, Fin.sum_univ_succ, add_comm]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ ↑LinearMap.det ↑(rotation o θ).toLinearEquiv = 1
[PROOFSTEP]
haveI : Nontrivial V := FiniteDimensional.nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _)
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
⊢ ↑LinearMap.det ↑(rotation o θ).toLinearEquiv = 1
[PROOFSTEP]
obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)
[GOAL]
case intro
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑LinearMap.det ↑(rotation o θ).toLinearEquiv = 1
[PROOFSTEP]
rw [o.rotation_eq_matrix_toLin θ hx]
[GOAL]
case intro
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑LinearMap.det
      (↑(Matrix.toLin (basisRightAngleRotation o x hx) (basisRightAngleRotation o x hx))
        (↑Matrix.of ![![Real.Angle.cos θ, -Real.Angle.sin θ], ![Real.Angle.sin θ, Real.Angle.cos θ]])) =
    1
[PROOFSTEP]
simpa [sq] using θ.cos_sq_add_sin_sq
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ ↑(↑LinearEquiv.det (rotation o θ).toLinearEquiv) = ↑1
[PROOFSTEP]
simpa only [LinearEquiv.coe_det, Units.val_one] using o.det_rotation θ
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ LinearIsometryEquiv.symm (rotation o θ) = rotation o (-θ)
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x✝ : V
⊢ ↑(LinearIsometryEquiv.symm (rotation o θ)) x✝ = ↑(rotation o (-θ)) x✝
[PROOFSTEP]
simp [o.rotation_apply, o.rotation_symm_apply, sub_eq_add_neg]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
⊢ rotation o 0 = LinearIsometryEquiv.refl ℝ V
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x✝ : V
⊢ ↑(rotation o 0) x✝ = ↑(LinearIsometryEquiv.refl ℝ V) x✝
[PROOFSTEP]
simp [rotation]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
⊢ rotation o ↑π = LinearIsometryEquiv.neg ℝ
[PROOFSTEP]
ext x
[GOAL]
case h
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ ↑(rotation o ↑π) x = ↑(LinearIsometryEquiv.neg ℝ) x
[PROOFSTEP]
simp [rotation]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ ↑(rotation o ↑π) x = -x
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
⊢ rotation o ↑(π / 2) = rightAngleRotation o
[PROOFSTEP]
ext x
[GOAL]
case h
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ ↑(rotation o ↑(π / 2)) x = ↑(rightAngleRotation o) x
[PROOFSTEP]
simp [rotation]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ₁ θ₂ : Real.Angle
x : V
⊢ ↑(rotation o θ₁) (↑(rotation o θ₂) x) = ↑(rotation o (θ₁ + θ₂)) x
[PROOFSTEP]
simp only [o.rotation_apply, ← mul_smul, Real.Angle.cos_add, Real.Angle.sin_add, add_smul, sub_smul,
  LinearIsometryEquiv.trans_apply, smul_add, LinearIsometryEquiv.map_add, LinearIsometryEquiv.map_smul,
  rightAngleRotation_rightAngleRotation, smul_neg]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ₁ θ₂ : Real.Angle
x : V
⊢ (Real.Angle.cos θ₂ * Real.Angle.cos θ₁) • x + (Real.Angle.cos θ₂ * Real.Angle.sin θ₁) • ↑(rightAngleRotation o) x +
      ((Real.Angle.sin θ₂ * Real.Angle.cos θ₁) • ↑(rightAngleRotation o) x +
        -((Real.Angle.sin θ₂ * Real.Angle.sin θ₁) • x)) =
    (Real.Angle.cos θ₁ * Real.Angle.cos θ₂) • x - (Real.Angle.sin θ₁ * Real.Angle.sin θ₂) • x +
      ((Real.Angle.sin θ₁ * Real.Angle.cos θ₂) • ↑(rightAngleRotation o) x +
        (Real.Angle.cos θ₁ * Real.Angle.sin θ₂) • ↑(rightAngleRotation o) x)
[PROOFSTEP]
ring_nf
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ₁ θ₂ : Real.Angle
x : V
⊢ (Real.Angle.cos θ₂ * Real.Angle.cos θ₁) • x + (Real.Angle.cos θ₂ * Real.Angle.sin θ₁) • ↑(rightAngleRotation o) x +
      ((Real.Angle.cos θ₁ * Real.Angle.sin θ₂) • ↑(rightAngleRotation o) x +
        -((Real.Angle.sin θ₁ * Real.Angle.sin θ₂) • x)) =
    (Real.Angle.cos θ₂ * Real.Angle.cos θ₁) • x - (Real.Angle.sin θ₁ * Real.Angle.sin θ₂) • x +
      ((Real.Angle.cos θ₂ * Real.Angle.sin θ₁) • ↑(rightAngleRotation o) x +
        (Real.Angle.cos θ₁ * Real.Angle.sin θ₂) • ↑(rightAngleRotation o) x)
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ₁ θ₂ : Real.Angle
x : V
⊢ (Real.Angle.cos θ₂ * Real.Angle.cos θ₁) • x + (Real.Angle.cos θ₂ * Real.Angle.sin θ₁) • ↑(rightAngleRotation o) x +
      ((Real.Angle.cos θ₁ * Real.Angle.sin θ₂) • ↑(rightAngleRotation o) x +
        -((Real.Angle.sin θ₁ * Real.Angle.sin θ₂) • x)) =
    (Real.Angle.cos θ₂ * Real.Angle.cos θ₁) • x - (Real.Angle.sin θ₁ * Real.Angle.sin θ₂) • x +
      ((Real.Angle.cos θ₂ * Real.Angle.sin θ₁) • ↑(rightAngleRotation o) x +
        (Real.Angle.cos θ₁ * Real.Angle.sin θ₂) • ↑(rightAngleRotation o) x)
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ₁ θ₂ : Real.Angle
x✝ : V
⊢ ↑(LinearIsometryEquiv.trans (rotation o θ₁) (rotation o θ₂)) x✝ = ↑(rotation o (θ₂ + θ₁)) x✝
[PROOFSTEP]
rw [← rotation_rotation, LinearIsometryEquiv.trans_apply]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ ↑(↑(kahler o) (↑(rotation o θ) x)) y = ↑(starRingEnd ℂ) ↑(Real.Angle.expMapCircle θ) * ↑(↑(kahler o) x) y
[PROOFSTEP]
simp only [o.rotation_apply, map_add, map_mul, LinearMap.map_smulₛₗ, RingHom.id_apply, LinearMap.add_apply,
  LinearMap.smul_apply, real_smul, kahler_rightAngleRotation_left, Real.Angle.coe_expMapCircle, Complex.conj_ofReal,
  conj_I]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ ↑(Real.Angle.cos θ) * ↑(↑(kahler o) x) y + ↑(Real.Angle.sin θ) * (-I * ↑(↑(kahler o) x) y) =
    (↑(Real.Angle.cos θ) + ↑(Real.Angle.sin θ) * -I) * ↑(↑(kahler o) x) y
[PROOFSTEP]
ring
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ -↑(rotation o θ) x = ↑(rotation o (↑π + θ)) x
[PROOFSTEP]
rw [← o.rotation_pi_apply, rotation_rotation]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ -↑(rotation o ↑(-π / 2)) x = ↑(rotation o ↑(π / 2)) x
[PROOFSTEP]
rw [neg_rotation, ← Real.Angle.coe_add, neg_div, ← sub_eq_add_neg, sub_half]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ ↑(↑(kahler o) (↑(rotation o θ) x)) y = ↑(Real.Angle.expMapCircle (-θ)) * ↑(↑(kahler o) x) y
[PROOFSTEP]
simp only [Real.Angle.expMapCircle_neg, coe_inv_circle_eq_conj, kahler_rotation_left]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ ↑(↑(kahler o) x) (↑(rotation o θ) y) = ↑(Real.Angle.expMapCircle θ) * ↑(↑(kahler o) x) y
[PROOFSTEP]
simp only [o.rotation_apply, map_add, LinearMap.map_smulₛₗ, RingHom.id_apply, real_smul,
  kahler_rightAngleRotation_right, Real.Angle.coe_expMapCircle]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ ↑(Real.Angle.cos θ) * ↑(↑(kahler o) x) y + ↑(Real.Angle.sin θ) * (I * ↑(↑(kahler o) x) y) =
    (↑(Real.Angle.cos θ) + ↑(Real.Angle.sin θ) * I) * ↑(↑(kahler o) x) y
[PROOFSTEP]
ring
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ oangle o (↑(rotation o θ) x) y = oangle o x y - θ
[PROOFSTEP]
simp only [oangle, o.kahler_rotation_left']
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(arg (↑(Real.Angle.expMapCircle (-θ)) * ↑(↑(kahler o) x) y)) = ↑(arg (↑(↑(kahler o) x) y)) - θ
[PROOFSTEP]
rw [Complex.arg_mul_coe_angle, Real.Angle.arg_expMapCircle]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ -θ + ↑(arg (↑(↑(kahler o) x) y)) = ↑(arg (↑(↑(kahler o) x) y)) - θ
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ -θ + ↑(arg (↑(↑(kahler o) x) y)) = ↑(arg (↑(↑(kahler o) x) y)) - θ
[PROOFSTEP]
abel
[GOAL]
case hx
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(Real.Angle.expMapCircle (-θ)) ≠ 0
[PROOFSTEP]
exact ne_zero_of_mem_circle _
[GOAL]
case hy
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(↑(kahler o) x) y ≠ 0
[PROOFSTEP]
exact o.kahler_ne_zero hx hy
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ oangle o x (↑(rotation o θ) y) = oangle o x y + θ
[PROOFSTEP]
simp only [oangle, o.kahler_rotation_right]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(arg (↑(Real.Angle.expMapCircle θ) * ↑(↑(kahler o) x) y)) = ↑(arg (↑(↑(kahler o) x) y)) + θ
[PROOFSTEP]
rw [Complex.arg_mul_coe_angle, Real.Angle.arg_expMapCircle]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ θ + ↑(arg (↑(↑(kahler o) x) y)) = ↑(arg (↑(↑(kahler o) x) y)) + θ
[PROOFSTEP]
abel
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ θ + ↑(arg (↑(↑(kahler o) x) y)) = ↑(arg (↑(↑(kahler o) x) y)) + θ
[PROOFSTEP]
abel
[GOAL]
case hx
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(Real.Angle.expMapCircle θ) ≠ 0
[PROOFSTEP]
exact ne_zero_of_mem_circle _
[GOAL]
case hy
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(↑(kahler o) x) y ≠ 0
[PROOFSTEP]
exact o.kahler_ne_zero hx hy
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ oangle o (↑(rotation o θ) x) x = -θ
[PROOFSTEP]
simp [hx]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ oangle o x (↑(rotation o θ) x) = θ
[PROOFSTEP]
simp [hx]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ oangle o (↑(rotation o (oangle o x y)) x) y = 0
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ oangle o (↑(rotation o (oangle o x y)) x) y = 0
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ oangle o (↑(rotation o (oangle o x y)) x) y = 0
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ oangle o (↑(rotation o (oangle o x y)) x) y = 0
[PROOFSTEP]
simp [hy]
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ oangle o (↑(rotation o (oangle o x y)) x) y = 0
[PROOFSTEP]
simp [hx, hy]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ oangle o y (↑(rotation o (oangle o x y)) x) = 0
[PROOFSTEP]
rw [oangle_rev]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ -oangle o (↑(rotation o (oangle o x y)) x) y = 0
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ oangle o (↑(rotation o θ) x) (↑(rotation o θ) y) = oangle o x y
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : x = 0
⊢ oangle o (↑(rotation o θ) x) (↑(rotation o θ) y) = oangle o x y
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
⊢ oangle o (↑(rotation o θ) x) (↑(rotation o θ) y) = oangle o x y
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : x = 0
hy : y = 0
⊢ oangle o (↑(rotation o θ) x) (↑(rotation o θ) y) = oangle o x y
[PROOFSTEP]
simp [hx, hy]
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : x = 0
hy : ¬y = 0
⊢ oangle o (↑(rotation o θ) x) (↑(rotation o θ) y) = oangle o x y
[PROOFSTEP]
simp [hx, hy]
[GOAL]
case pos
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : y = 0
⊢ oangle o (↑(rotation o θ) x) (↑(rotation o θ) y) = oangle o x y
[PROOFSTEP]
simp [hx, hy]
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
⊢ oangle o (↑(rotation o θ) x) (↑(rotation o θ) y) = oangle o x y
[PROOFSTEP]
simp [hx, hy]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ ↑(rotation o θ) x = x ↔ θ = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ ↑(rotation o θ) x = x → θ = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
h : ↑(rotation o θ) x = x
⊢ θ = 0
[PROOFSTEP]
rw [eq_comm]
[GOAL]
case mp
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
h : ↑(rotation o θ) x = x
⊢ 0 = θ
[PROOFSTEP]
simpa [hx, h] using o.oangle_rotation_right hx hx θ
[GOAL]
case mpr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ θ = 0 → ↑(rotation o θ) x = x
[PROOFSTEP]
intro h
[GOAL]
case mpr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
h : θ = 0
⊢ ↑(rotation o θ) x = x
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ x = ↑(rotation o θ) x ↔ θ = 0
[PROOFSTEP]
rw [← o.rotation_eq_self_iff_angle_eq_zero hx, eq_comm]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
θ : Real.Angle
⊢ ↑(rotation o θ) x = x ↔ x = 0 ∨ θ = 0
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
θ : Real.Angle
h : x = 0
⊢ ↑(rotation o θ) x = x ↔ x = 0 ∨ θ = 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
θ : Real.Angle
h : ¬x = 0
⊢ ↑(rotation o θ) x = x ↔ x = 0 ∨ θ = 0
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
θ : Real.Angle
⊢ x = ↑(rotation o θ) x ↔ x = 0 ∨ θ = 0
[PROOFSTEP]
rw [← rotation_eq_self_iff, eq_comm]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ ↑(rotation o (oangle o x y)) x = y ↔ ‖x‖ = ‖y‖
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ ↑(rotation o (oangle o x y)) x = y → ‖x‖ = ‖y‖
[PROOFSTEP]
intro h
[GOAL]
case mp
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ↑(rotation o (oangle o x y)) x = y
⊢ ‖x‖ = ‖y‖
[PROOFSTEP]
rw [← h, LinearIsometryEquiv.norm_map]
[GOAL]
case mpr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ ‖x‖ = ‖y‖ → ↑(rotation o (oangle o x y)) x = y
[PROOFSTEP]
intro h
[GOAL]
case mpr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ ↑(rotation o (oangle o x y)) x = y
[PROOFSTEP]
rw [o.eq_iff_oangle_eq_zero_of_norm_eq]
[GOAL]
case mpr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ oangle o (↑(rotation o (oangle o x y)) x) y = 0
[PROOFSTEP]
simp [h]
[GOAL]
case mpr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ ‖↑(rotation o (oangle o x y)) x‖ = ‖y‖
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ oangle o x y = θ ↔ y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x
[PROOFSTEP]
have hp := div_pos (norm_pos_iff.2 hy) (norm_pos_iff.2 hx)
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
⊢ oangle o x y = θ ↔ y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
⊢ oangle o x y = θ → y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
hp : 0 < ‖y‖ / ‖x‖
⊢ y = (‖y‖ / ‖x‖) • ↑(rotation o (oangle o x y)) x
[PROOFSTEP]
rw [← LinearIsometryEquiv.map_smul, ← o.oangle_smul_left_of_pos x y hp, eq_comm, rotation_oangle_eq_iff_norm_eq,
  norm_smul, Real.norm_of_nonneg hp.le, div_mul_cancel _ (norm_ne_zero_iff.2 hx)]
[GOAL]
case mpr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
⊢ y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x → oangle o x y = θ
[PROOFSTEP]
intro hye
[GOAL]
case mpr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
hye : y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x
⊢ oangle o x y = θ
[PROOFSTEP]
rw [hye, o.oangle_smul_right_of_pos _ _ hp, o.oangle_rotation_self_right hx]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ oangle o x y = θ ↔ ∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ oangle o x y = θ → ∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x
[PROOFSTEP]
intro h
[GOAL]
case mp
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
h : oangle o x y = θ
⊢ ∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x
[PROOFSTEP]
rw [o.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero hx hy] at h
[GOAL]
case mp
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
h : y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x
⊢ ∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x
[PROOFSTEP]
exact ⟨‖y‖ / ‖x‖, div_pos (norm_pos_iff.2 hy) (norm_pos_iff.2 hx), h⟩
[GOAL]
case mpr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x) → oangle o x y = θ
[PROOFSTEP]
rintro ⟨r, hr, rfl⟩
[GOAL]
case mpr.intro.intro
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
r : ℝ
hr : 0 < r
hy : r • ↑(rotation o θ) x ≠ 0
⊢ oangle o x (r • ↑(rotation o θ) x) = θ
[PROOFSTEP]
rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right hx]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ oangle o x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : x = 0
⊢ oangle o x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
simp [hx, eq_comm]
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
⊢ oangle o x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : y = 0
⊢ oangle o x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
simp [hy, eq_comm]
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
⊢ oangle o x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
rw [o.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero hx hy]
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
⊢ y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • ↑(rotation o θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
simp [hx, hy]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ oangle o x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : x = 0
⊢ oangle o x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
simp [hx, eq_comm]
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
⊢ oangle o x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : y = 0
⊢ oangle o x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
simp [hy, eq_comm]
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
⊢ oangle o x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
rw [o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero hx hy]
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
⊢ (∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x) ↔
    (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • ↑(rotation o θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
[PROOFSTEP]
simp [hx, hy]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
⊢ ∃ θ, f = rotation o θ
[PROOFSTEP]
haveI : Nontrivial V := FiniteDimensional.nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _)
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
⊢ ∃ θ, f = rotation o θ
[PROOFSTEP]
obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)
[GOAL]
case intro
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ∃ θ, f = rotation o θ
[PROOFSTEP]
use o.oangle x (f x)
[GOAL]
case h
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ f = rotation o (oangle o x (↑f x))
[PROOFSTEP]
apply LinearIsometryEquiv.toLinearEquiv_injective
[GOAL]
case h.a
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ f.toLinearEquiv = (rotation o (oangle o x (↑f x))).toLinearEquiv
[PROOFSTEP]
apply LinearEquiv.toLinearMap_injective
[GOAL]
case h.a.a
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑f.toLinearEquiv = ↑(rotation o (oangle o x (↑f x))).toLinearEquiv
[PROOFSTEP]
apply (o.basisRightAngleRotation x hx).ext
[GOAL]
case h.a.a
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ∀ (i : Fin 2),
    ↑↑f.toLinearEquiv (↑(basisRightAngleRotation o x hx) i) =
      ↑↑(rotation o (oangle o x (↑f x))).toLinearEquiv (↑(basisRightAngleRotation o x hx) i)
[PROOFSTEP]
intro i
[GOAL]
case h.a.a
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
i : Fin 2
⊢ ↑↑f.toLinearEquiv (↑(basisRightAngleRotation o x hx) i) =
    ↑↑(rotation o (oangle o x (↑f x))).toLinearEquiv (↑(basisRightAngleRotation o x hx) i)
[PROOFSTEP]
symm
[GOAL]
case h.a.a
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
i : Fin 2
⊢ ↑↑(rotation o (oangle o x (↑f x))).toLinearEquiv (↑(basisRightAngleRotation o x hx) i) =
    ↑↑f.toLinearEquiv (↑(basisRightAngleRotation o x hx) i)
[PROOFSTEP]
fin_cases i
[GOAL]
case h.a.a.head
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑↑(rotation o (oangle o x (↑f x))).toLinearEquiv
      (↑(basisRightAngleRotation o x hx) { val := 0, isLt := (_ : 0 < 2) }) =
    ↑↑f.toLinearEquiv (↑(basisRightAngleRotation o x hx) { val := 0, isLt := (_ : 0 < 2) })
[PROOFSTEP]
simp
[GOAL]
case h.a.a.tail.head
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑↑(rotation o (oangle o x (↑f x))).toLinearEquiv
      (↑(basisRightAngleRotation o x hx) { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑↑f.toLinearEquiv (↑(basisRightAngleRotation o x hx) { val := 1, isLt := (_ : (fun a => a < 2) 1) })
[PROOFSTEP]
have : o.oangle (J x) (f (J x)) = o.oangle x (f x) := by
  simp only [oangle, o.linearIsometryEquiv_comp_rightAngleRotation f hd, o.kahler_comp_rightAngleRotation]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ oangle o (↑(rightAngleRotation o) x) (↑f (↑(rightAngleRotation o) x)) = oangle o x (↑f x)
[PROOFSTEP]
simp only [oangle, o.linearIsometryEquiv_comp_rightAngleRotation f hd, o.kahler_comp_rightAngleRotation]
[GOAL]
case h.a.a.tail.head
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < ↑LinearMap.det ↑f.toLinearEquiv
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : oangle o (↑(rightAngleRotation o) x) (↑f (↑(rightAngleRotation o) x)) = oangle o x (↑f x)
⊢ ↑↑(rotation o (oangle o x (↑f x))).toLinearEquiv
      (↑(basisRightAngleRotation o x hx) { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑↑f.toLinearEquiv (↑(basisRightAngleRotation o x hx) { val := 1, isLt := (_ : (fun a => a < 2) 1) })
[PROOFSTEP]
simp [← this]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
f : V ≃ₗᵢ[ℝ] V'
x : V'
⊢ ↑(rotation (↑(map (Fin 2) f.toLinearEquiv) o) θ) x = ↑f (↑(rotation o θ) (↑(LinearIsometryEquiv.symm f) x))
[PROOFSTEP]
simp [rotation_apply, o.rightAngleRotation_map]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
z : ℂ
⊢ ↑(rotation Complex.orientation θ) z = ↑(Real.Angle.expMapCircle θ) * z
[PROOFSTEP]
simp only [rotation_apply, Complex.rightAngleRotation, Real.Angle.coe_expMapCircle, real_smul]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
z : ℂ
⊢ ↑(Real.Angle.cos θ) * z + ↑(Real.Angle.sin θ) * (I * z) = (↑(Real.Angle.cos θ) + ↑(Real.Angle.sin θ) * I) * z
[PROOFSTEP]
ring
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
f : V ≃ₗᵢ[ℝ] ℂ
hf : ↑(map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : V
⊢ ↑f (↑(rotation o θ) x) = ↑(Real.Angle.expMapCircle θ) * ↑f x
[PROOFSTEP]
rw [← Complex.rotation, ← hf, o.rotation_map, LinearIsometryEquiv.symm_apply_apply]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ ∀ (x : V), ↑(rotation (-o) θ) x = ↑(rotation o (-θ)) x
[PROOFSTEP]
simp [rotation_apply]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ inner (↑(rotation o ↑(π / 2)) x) x = 0
[PROOFSTEP]
rw [rotation_pi_div_two, inner_rightAngleRotation_self]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ inner x (↑(rotation o ↑(π / 2)) x) = 0
[PROOFSTEP]
rw [real_inner_comm, inner_rotation_pi_div_two_left]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ inner (r • ↑(rotation o ↑(π / 2)) x) x = 0
[PROOFSTEP]
rw [inner_smul_left, inner_rotation_pi_div_two_left, mul_zero]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ inner x (r • ↑(rotation o ↑(π / 2)) x) = 0
[PROOFSTEP]
rw [real_inner_comm, inner_smul_rotation_pi_div_two_left]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ inner (↑(rotation o ↑(π / 2)) x) (r • x) = 0
[PROOFSTEP]
rw [inner_smul_right, inner_rotation_pi_div_two_left, mul_zero]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ inner (r • x) (↑(rotation o ↑(π / 2)) x) = 0
[PROOFSTEP]
rw [real_inner_comm, inner_rotation_pi_div_two_left_smul]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
⊢ inner (r₁ • ↑(rotation o ↑(π / 2)) x) (r₂ • x) = 0
[PROOFSTEP]
rw [inner_smul_right, inner_smul_rotation_pi_div_two_left, mul_zero]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
⊢ inner (r₂ • x) (r₁ • ↑(rotation o ↑(π / 2)) x) = 0
[PROOFSTEP]
rw [real_inner_comm, inner_smul_rotation_pi_div_two_smul_left]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ inner x y = 0 ↔ x = 0 ∨ ∃ r, r • ↑(rotation o ↑(π / 2)) x = y
[PROOFSTEP]
rw [← o.eq_zero_or_oangle_eq_iff_inner_eq_zero]
[GOAL]
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ x = 0 ∨ y = 0 ∨ oangle o x y = ↑(π / 2) ∨ oangle o x y = ↑(-π / 2) ↔ x = 0 ∨ ∃ r, r • ↑(rotation o ↑(π / 2)) x = y
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : x = 0 ∨ y = 0 ∨ oangle o x y = ↑(π / 2) ∨ oangle o x y = ↑(-π / 2)
⊢ x = 0 ∨ ∃ r, r • ↑(rotation o ↑(π / 2)) x = y
[PROOFSTEP]
rcases h with (rfl | rfl | h | h)
[GOAL]
case refine'_1.inl
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
y : V
⊢ 0 = 0 ∨ ∃ r, r • ↑(rotation o ↑(π / 2)) 0 = y
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case refine'_1.inr.inl
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ x = 0 ∨ ∃ r, r • ↑(rotation o ↑(π / 2)) x = 0
[PROOFSTEP]
exact Or.inr ⟨0, zero_smul _ _⟩
[GOAL]
case refine'_1.inr.inr.inl
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ x = 0 ∨ ∃ r, r • ↑(rotation o ↑(π / 2)) x = y
[PROOFSTEP]
obtain ⟨r, _, rfl⟩ :=
  (o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero (o.left_ne_zero_of_oangle_eq_pi_div_two h)
        (o.right_ne_zero_of_oangle_eq_pi_div_two h) _).1
    h
[GOAL]
case refine'_1.inr.inr.inl.intro.intro
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
left✝ : 0 < r
h : oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(π / 2)
⊢ x = 0 ∨ ∃ r_1, r_1 • ↑(rotation o ↑(π / 2)) x = r • ↑(rotation o ↑(π / 2)) x
[PROOFSTEP]
exact Or.inr ⟨r, rfl⟩
[GOAL]
case refine'_1.inr.inr.inr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(-π / 2)
⊢ x = 0 ∨ ∃ r, r • ↑(rotation o ↑(π / 2)) x = y
[PROOFSTEP]
obtain ⟨r, _, rfl⟩ :=
  (o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero (o.left_ne_zero_of_oangle_eq_neg_pi_div_two h)
        (o.right_ne_zero_of_oangle_eq_neg_pi_div_two h) _).1
    h
[GOAL]
case refine'_1.inr.inr.inr.intro.intro
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
left✝ : 0 < r
h : oangle o x (r • ↑(rotation o ↑(-π / 2)) x) = ↑(-π / 2)
⊢ x = 0 ∨ ∃ r_1, r_1 • ↑(rotation o ↑(π / 2)) x = r • ↑(rotation o ↑(-π / 2)) x
[PROOFSTEP]
refine' Or.inr ⟨-r, _⟩
[GOAL]
case refine'_1.inr.inr.inr.intro.intro
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
left✝ : 0 < r
h : oangle o x (r • ↑(rotation o ↑(-π / 2)) x) = ↑(-π / 2)
⊢ -r • ↑(rotation o ↑(π / 2)) x = r • ↑(rotation o ↑(-π / 2)) x
[PROOFSTEP]
rw [neg_smul, ← smul_neg, o.neg_rotation_pi_div_two]
[GOAL]
case refine'_2
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : x = 0 ∨ ∃ r, r • ↑(rotation o ↑(π / 2)) x = y
⊢ x = 0 ∨ y = 0 ∨ oangle o x y = ↑(π / 2) ∨ oangle o x y = ↑(-π / 2)
[PROOFSTEP]
rcases h with (rfl | ⟨r, rfl⟩)
[GOAL]
case refine'_2.inl
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
y : V
⊢ 0 = 0 ∨ y = 0 ∨ oangle o 0 y = ↑(π / 2) ∨ oangle o 0 y = ↑(-π / 2)
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case refine'_2.inr.intro
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ x = 0 ∨
    r • ↑(rotation o ↑(π / 2)) x = 0 ∨
      oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(π / 2) ∨ oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(-π / 2)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : x = 0
⊢ x = 0 ∨
    r • ↑(rotation o ↑(π / 2)) x = 0 ∨
      oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(π / 2) ∨ oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(-π / 2)
[PROOFSTEP]
exact Or.inl hx
[GOAL]
case neg
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
⊢ x = 0 ∨
    r • ↑(rotation o ↑(π / 2)) x = 0 ∨
      oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(π / 2) ∨ oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(-π / 2)
[PROOFSTEP]
rcases lt_trichotomy r 0 with (hr | rfl | hr)
[GOAL]
case neg.inl
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : r < 0
⊢ x = 0 ∨
    r • ↑(rotation o ↑(π / 2)) x = 0 ∨
      oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(π / 2) ∨ oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(-π / 2)
[PROOFSTEP]
refine' Or.inr (Or.inr (Or.inr _))
[GOAL]
case neg.inl
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : r < 0
⊢ oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(-π / 2)
[PROOFSTEP]
rw [o.oangle_smul_right_of_neg _ _ hr, o.neg_rotation_pi_div_two, o.oangle_rotation_self_right hx]
[GOAL]
case neg.inr.inl
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : ¬x = 0
⊢ x = 0 ∨
    0 • ↑(rotation o ↑(π / 2)) x = 0 ∨
      oangle o x (0 • ↑(rotation o ↑(π / 2)) x) = ↑(π / 2) ∨ oangle o x (0 • ↑(rotation o ↑(π / 2)) x) = ↑(-π / 2)
[PROOFSTEP]
exact Or.inr (Or.inl (zero_smul _ _))
[GOAL]
case neg.inr.inr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : 0 < r
⊢ x = 0 ∨
    r • ↑(rotation o ↑(π / 2)) x = 0 ∨
      oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(π / 2) ∨ oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(-π / 2)
[PROOFSTEP]
refine' Or.inr (Or.inr (Or.inl _))
[GOAL]
case neg.inr.inr
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : 0 < r
⊢ oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(π / 2)
[PROOFSTEP]
rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right hx]


[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
α β : F ⟶ G
⊢ T.map (α.f + β.f) ≫ G.a = F.a ≫ (α.f + β.f)
[PROOFSTEP]
simp only [Functor.map_add, add_comp, Monad.Algebra.Hom.h, comp_add]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ ∀ (a b c : F ⟶ G), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ b✝ c✝ : F ⟶ G
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ b✝ c✝ : F ⟶ G
⊢ (a✝ + b✝ + c✝).f = (a✝ + (b✝ + c✝)).f
[PROOFSTEP]
apply add_assoc
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ T.map 0 ≫ G.a = F.a ≫ 0
[PROOFSTEP]
simp only [Functor.map_zero, zero_comp, comp_zero]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ ∀ (a : F ⟶ G), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ : F ⟶ G
⊢ 0 + a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ : F ⟶ G
⊢ (0 + a✝).f = a✝.f
[PROOFSTEP]
apply zero_add
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ ∀ (a : F ⟶ G), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ : F ⟶ G
⊢ a✝ + 0 = a✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ : F ⟶ G
⊢ (a✝ + 0).f = a✝.f
[PROOFSTEP]
apply add_zero
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
n : ℕ
α : F ⟶ G
⊢ T.map (n • α.f) ≫ G.a = F.a ≫ (n • α.f)
[PROOFSTEP]
rw [Functor.map_nsmul, nsmul_comp, Monad.Algebra.Hom.h, comp_nsmul]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ ∀ (x : F ⟶ G), (fun n α => Algebra.Hom.mk (n • α.f)) 0 x = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
x✝ : F ⟶ G
⊢ (fun n α => Algebra.Hom.mk (n • α.f)) 0 x✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
x✝ : F ⟶ G
⊢ ((fun n α => Algebra.Hom.mk (n • α.f)) 0 x✝).f = 0.f
[PROOFSTEP]
apply zero_smul
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ ∀ (n : ℕ) (x : F ⟶ G), (fun n α => Algebra.Hom.mk (n • α.f)) (n + 1) x = x + (fun n α => Algebra.Hom.mk (n • α.f)) n x
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
n✝ : ℕ
x✝ : F ⟶ G
⊢ (fun n α => Algebra.Hom.mk (n • α.f)) (n✝ + 1) x✝ = x✝ + (fun n α => Algebra.Hom.mk (n • α.f)) n✝ x✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
n✝ : ℕ
x✝ : F ⟶ G
⊢ ((fun n α => Algebra.Hom.mk (n • α.f)) (n✝ + 1) x✝).f = (x✝ + (fun n α => Algebra.Hom.mk (n • α.f)) n✝ x✝).f
[PROOFSTEP]
apply succ_nsmul
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
α : F ⟶ G
⊢ T.map (-α.f) ≫ G.a = F.a ≫ (-α.f)
[PROOFSTEP]
simp only [Functor.map_neg, neg_comp, Monad.Algebra.Hom.h, comp_neg]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
α β : F ⟶ G
⊢ T.map (α.f - β.f) ≫ G.a = F.a ≫ (α.f - β.f)
[PROOFSTEP]
simp only [Functor.map_sub, sub_comp, Monad.Algebra.Hom.h, comp_sub]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ ∀ (a b : F ⟶ G), a - b = a + -b
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ b✝ : F ⟶ G
⊢ a✝ - b✝ = a✝ + -b✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ b✝ : F ⟶ G
⊢ (a✝ - b✝).f = (a✝ + -b✝).f
[PROOFSTEP]
apply sub_eq_add_neg
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
r : ℤ
α : F ⟶ G
⊢ T.map (r • α.f) ≫ G.a = F.a ≫ (r • α.f)
[PROOFSTEP]
rw [Functor.map_zsmul, zsmul_comp, Monad.Algebra.Hom.h, comp_zsmul]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ ∀ (a : F ⟶ G), (fun r α => Algebra.Hom.mk (r • α.f)) 0 a = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ : F ⟶ G
⊢ (fun r α => Algebra.Hom.mk (r • α.f)) 0 a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ : F ⟶ G
⊢ ((fun r α => Algebra.Hom.mk (r • α.f)) 0 a✝).f = 0.f
[PROOFSTEP]
apply zero_smul
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ ∀ (n : ℕ) (a : F ⟶ G),
    (fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n)) a =
      a + (fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
n✝ : ℕ
a✝ : F ⟶ G
⊢ (fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n✝)) a✝ =
    a✝ + (fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat n✝) a✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
n✝ : ℕ
a✝ : F ⟶ G
⊢ ((fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n✝)) a✝).f =
    (a✝ + (fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat n✝) a✝).f
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
n✝ : ℕ
a✝ : F ⟶ G
⊢ ↑(Nat.succ n✝) • a✝.f = (a✝ + Algebra.Hom.mk (↑n✝ • a✝.f)).f
[PROOFSTEP]
simp only [coe_nat_zsmul, succ_nsmul]
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
n✝ : ℕ
a✝ : F ⟶ G
⊢ a✝.f + n✝ • a✝.f = (a✝ + Algebra.Hom.mk (n✝ • a✝.f)).f
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ ∀ (n : ℕ) (a : F ⟶ G),
    (fun r α => Algebra.Hom.mk (r • α.f)) (Int.negSucc n) a = -(fun r α => Algebra.Hom.mk (r • α.f)) (↑(Nat.succ n)) a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
n✝ : ℕ
a✝ : F ⟶ G
⊢ (fun r α => Algebra.Hom.mk (r • α.f)) (Int.negSucc n✝) a✝ = -(fun r α => Algebra.Hom.mk (r • α.f)) (↑(Nat.succ n✝)) a✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
n✝ : ℕ
a✝ : F ⟶ G
⊢ ((fun r α => Algebra.Hom.mk (r • α.f)) (Int.negSucc n✝) a✝).f =
    (-(fun r α => Algebra.Hom.mk (r • α.f)) (↑(Nat.succ n✝)) a✝).f
[PROOFSTEP]
simp only [negSucc_zsmul, neg_inj, nsmul_eq_smul_cast ℤ]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ ∀ (a : F ⟶ G), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ : F ⟶ G
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ : F ⟶ G
⊢ (-a✝ + a✝).f = 0.f
[PROOFSTEP]
apply add_left_neg
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
⊢ ∀ (a b : F ⟶ G), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ b✝ : F ⟶ G
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
F G : Algebra T
a✝ b✝ : F ⟶ G
⊢ (a✝ + b✝).f = (b✝ + a✝).f
[PROOFSTEP]
apply add_comm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
⊢ ∀ (P Q R : Algebra T) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
P✝ Q✝ R✝ : Algebra T
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
P✝ Q✝ R✝ : Algebra T
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ ((f✝ + f'✝) ≫ g✝).f = (f✝ ≫ g✝ + f'✝ ≫ g✝).f
[PROOFSTEP]
apply add_comp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
⊢ ∀ (P Q R : Algebra T) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
P✝ Q✝ R✝ : Algebra T
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : Functor.Additive T.toFunctor
P✝ Q✝ R✝ : Algebra T
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ (f✝ ≫ (g✝ + g'✝)).f = (f✝ ≫ g✝ + f✝ ≫ g'✝).f
[PROOFSTEP]
apply comp_add
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
α β : F ⟶ G
⊢ F.a ≫ U.map (α.f + β.f) = (α.f + β.f) ≫ G.a
[PROOFSTEP]
simp only [Functor.map_add, comp_add, Comonad.Coalgebra.Hom.h, add_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ ∀ (a b c : F ⟶ G), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ b✝ c✝ : F ⟶ G
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ b✝ c✝ : F ⟶ G
⊢ (a✝ + b✝ + c✝).f = (a✝ + (b✝ + c✝)).f
[PROOFSTEP]
apply add_assoc
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ F.a ≫ U.map 0 = 0 ≫ G.a
[PROOFSTEP]
simp only [Functor.map_zero, comp_zero, zero_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ ∀ (a : F ⟶ G), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ : F ⟶ G
⊢ 0 + a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ : F ⟶ G
⊢ (0 + a✝).f = a✝.f
[PROOFSTEP]
apply zero_add
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ ∀ (a : F ⟶ G), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ : F ⟶ G
⊢ a✝ + 0 = a✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ : F ⟶ G
⊢ (a✝ + 0).f = a✝.f
[PROOFSTEP]
apply add_zero
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
n : ℕ
α : F ⟶ G
⊢ F.a ≫ U.map (n • α.f) = (n • α.f) ≫ G.a
[PROOFSTEP]
rw [Functor.map_nsmul, comp_nsmul, Comonad.Coalgebra.Hom.h, nsmul_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ ∀ (x : F ⟶ G), (fun n α => Coalgebra.Hom.mk (n • α.f)) 0 x = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
x✝ : F ⟶ G
⊢ (fun n α => Coalgebra.Hom.mk (n • α.f)) 0 x✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
x✝ : F ⟶ G
⊢ ((fun n α => Coalgebra.Hom.mk (n • α.f)) 0 x✝).f = 0.f
[PROOFSTEP]
apply zero_smul
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ ∀ (n : ℕ) (x : F ⟶ G),
    (fun n α => Coalgebra.Hom.mk (n • α.f)) (n + 1) x = x + (fun n α => Coalgebra.Hom.mk (n • α.f)) n x
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
n✝ : ℕ
x✝ : F ⟶ G
⊢ (fun n α => Coalgebra.Hom.mk (n • α.f)) (n✝ + 1) x✝ = x✝ + (fun n α => Coalgebra.Hom.mk (n • α.f)) n✝ x✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
n✝ : ℕ
x✝ : F ⟶ G
⊢ ((fun n α => Coalgebra.Hom.mk (n • α.f)) (n✝ + 1) x✝).f = (x✝ + (fun n α => Coalgebra.Hom.mk (n • α.f)) n✝ x✝).f
[PROOFSTEP]
apply succ_nsmul
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
α : F ⟶ G
⊢ F.a ≫ U.map (-α.f) = (-α.f) ≫ G.a
[PROOFSTEP]
simp only [Functor.map_neg, comp_neg, Comonad.Coalgebra.Hom.h, neg_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
α β : F ⟶ G
⊢ F.a ≫ U.map (α.f - β.f) = (α.f - β.f) ≫ G.a
[PROOFSTEP]
simp only [Functor.map_sub, comp_sub, Comonad.Coalgebra.Hom.h, sub_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ ∀ (a b : F ⟶ G), a - b = a + -b
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ b✝ : F ⟶ G
⊢ a✝ - b✝ = a✝ + -b✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ b✝ : F ⟶ G
⊢ (a✝ - b✝).f = (a✝ + -b✝).f
[PROOFSTEP]
apply sub_eq_add_neg
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
r : ℤ
α : F ⟶ G
⊢ F.a ≫ U.map (r • α.f) = (r • α.f) ≫ G.a
[PROOFSTEP]
rw [Functor.map_zsmul, comp_zsmul, Comonad.Coalgebra.Hom.h, zsmul_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ ∀ (a : F ⟶ G), (fun r α => Coalgebra.Hom.mk (r • α.f)) 0 a = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ : F ⟶ G
⊢ (fun r α => Coalgebra.Hom.mk (r • α.f)) 0 a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ : F ⟶ G
⊢ ((fun r α => Coalgebra.Hom.mk (r • α.f)) 0 a✝).f = 0.f
[PROOFSTEP]
apply zero_smul
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ ∀ (n : ℕ) (a : F ⟶ G),
    (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n)) a =
      a + (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
n✝ : ℕ
a✝ : F ⟶ G
⊢ (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n✝)) a✝ =
    a✝ + (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat n✝) a✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
n✝ : ℕ
a✝ : F ⟶ G
⊢ ((fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n✝)) a✝).f =
    (a✝ + (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat n✝) a✝).f
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
n✝ : ℕ
a✝ : F ⟶ G
⊢ ↑(Nat.succ n✝) • a✝.f = (a✝ + Coalgebra.Hom.mk (↑n✝ • a✝.f)).f
[PROOFSTEP]
simp only [coe_nat_zsmul, succ_nsmul]
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
n✝ : ℕ
a✝ : F ⟶ G
⊢ a✝.f + n✝ • a✝.f = (a✝ + Coalgebra.Hom.mk (n✝ • a✝.f)).f
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ ∀ (n : ℕ) (a : F ⟶ G),
    (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.negSucc n) a =
      -(fun r α => Coalgebra.Hom.mk (r • α.f)) (↑(Nat.succ n)) a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
n✝ : ℕ
a✝ : F ⟶ G
⊢ (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.negSucc n✝) a✝ =
    -(fun r α => Coalgebra.Hom.mk (r • α.f)) (↑(Nat.succ n✝)) a✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
n✝ : ℕ
a✝ : F ⟶ G
⊢ ((fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.negSucc n✝) a✝).f =
    (-(fun r α => Coalgebra.Hom.mk (r • α.f)) (↑(Nat.succ n✝)) a✝).f
[PROOFSTEP]
simp only [negSucc_zsmul, neg_inj, nsmul_eq_smul_cast ℤ]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ ∀ (a : F ⟶ G), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ : F ⟶ G
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ : F ⟶ G
⊢ (-a✝ + a✝).f = 0.f
[PROOFSTEP]
apply add_left_neg
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
⊢ ∀ (a b : F ⟶ G), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ b✝ : F ⟶ G
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
F G : Coalgebra U
a✝ b✝ : F ⟶ G
⊢ (a✝ + b✝).f = (b✝ + a✝).f
[PROOFSTEP]
apply add_comm
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
⊢ ∀ (P Q R : Coalgebra U) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
P✝ Q✝ R✝ : Coalgebra U
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
P✝ Q✝ R✝ : Coalgebra U
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ ((f✝ + f'✝) ≫ g✝).f = (f✝ ≫ g✝ + f'✝ ≫ g✝).f
[PROOFSTEP]
apply add_comp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
⊢ ∀ (P Q R : Coalgebra U) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
P✝ Q✝ R✝ : Coalgebra U
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : Functor.Additive T.toFunctor
U : Comonad C
inst✝ : Functor.Additive U.toFunctor
P✝ Q✝ R✝ : Coalgebra U
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ (f✝ ≫ (g✝ + g'✝)).f = (f✝ ≫ g✝ + f✝ ≫ g'✝).f
[PROOFSTEP]
apply comp_add