awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪x, (o.rightAngleRotation : (a : E) → E) y⟫ = -⟪(o.rightAngleRotation : (a : E) → E) x, y⟫

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪(o.rightAngleRotation : (a : E) → E) x, y⟫ = -⟪x, (o.rightAngleRotation : (a : E) → E) y⟫

Tactic:
simp [o.inner_rightAngleRotation_swap x y]

Premises used: Orientation.inner_rightAngleRotation_swap
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) x : E) ((o.rightAngleRotation : (a : E) → E) y : E) = ⟪x, y⟫

Tactic:
LinearIsometryEquiv.inner_map_map J x y

Premises used: Orientation.rightAngleRotation, LinearIsometryEquiv.inner_map_map
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
rw :
  (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y =
    -inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) x : E) ((o.rightAngleRotation : (a : E) → E) y : E)
rw₁ :
  Eq (α := ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y :
      ℝ)
    (-
        -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
            y :
      ℝ)
rw₂ rw₃ :
  Eq (α := ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y :
      ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y :
      ℝ)
⊢ (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y =
    -⟪x, y⟫

Tactic:
rw [← o.inner_comp_rightAngleRotation, o.inner_rightAngleRotation_right, neg_neg]

Premises used: neg_neg, Orientation.inner_comp_rightAngleRotation, Orientation.inner_rightAngleRotation_right
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
rw : inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) x : E) ((o.rightAngleRotation : (a : E) → E) y : E) = ⟪x, y⟫
rw₁ rw₂ : ⟪x, y⟫ = ⟪x, y⟫
⊢ (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) ((o.rightAngleRotation : (a : E) → E) y : E) =
    ⟪x, y⟫

Tactic:
rw [← o.inner_rightAngleRotation_left, o.inner_comp_rightAngleRotation]

Premises used: Orientation.inner_comp_rightAngleRotation, Orientation.inner_rightAngleRotation_left
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Eq (α := ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
        ((o.rightAngleRotation : (a : E) → E) y : E) :
      ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
h :
  ∀ (x : E),
    Eq (α := E) ((o.rightAngleRotation.trans o.rightAngleRotation : (a : E) → E) x : E)
      ((LinearIsometryEquiv.neg ℝ : (a : E) → E) x : E)
⊢ o.rightAngleRotation.trans o.rightAngleRotation = LinearIsometryEquiv.neg ℝ

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ Eq (α := E) ((o.rightAngleRotation.trans o.rightAngleRotation : (a : E) → E) x : E)
    ((LinearIsometryEquiv.neg ℝ : (a : E) → E) x : E)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
apply : ∀ (v : E), ⟪((-o).rightAngleRotation : (a : E) → E) x, v⟫ = ⟪-(o.rightAngleRotation : (a : E) → E) x, v⟫
⊢ Eq (α := E) (((-o).rightAngleRotation : (a : E) → E) x : E) (-(o.rightAngleRotation : (a : E) → E) x : E)

Tactic:
apply ext_inner_right ℝ

Premises used: Real, ext_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
rw :
  ((((-o).areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y = ⟪-(o.rightAngleRotation : (a : E) → E) x, y⟫
⊢ ⟪((-o).rightAngleRotation : (a : E) → E) x, y⟫ = ⟪-(o.rightAngleRotation : (a : E) → E) x, y⟫

Tactic:
rw [inner_rightAngleRotation_left]

Premises used: Orientation.inner_rightAngleRotation_left
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ((((-o).areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y = ⟪-(o.rightAngleRotation : (a : E) → E) x, y⟫

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ (-o).rightAngleRotation = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ)

Tactic:
LinearIsometryEquiv.ext <| o.rightAngleRotation_neg_orientation

Premises used: LinearIsometryEquiv.ext, Orientation.rightAngleRotation_neg_orientation
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x : F
apply :
  ∀ (v : F),
    ⟪(rightAngleRotation
              (((map (Fin 2) φ.toLinearEquiv :
                    Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 2)) (Orientation ℝ F (Fin 2))) :
                  (a : Orientation ℝ E (Fin 2)) → Orientation ℝ F (Fin 2))
                o) :
            (a : F) → F)
          x,
        v⟫ =
      ⟪(φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E), v⟫
⊢ Eq (α := F)
    ((rightAngleRotation
            (((map (Fin 2) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 2)) (Orientation ℝ F (Fin 2))) :
                (a : Orientation ℝ E (Fin 2)) → Orientation ℝ F (Fin 2))
              o) :
          (a : F) → F)
        x :
      F)
    ((φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E) : F)

Tactic:
apply ext_inner_right ℝ

Premises used: Real, ext_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
rw :
  (((areaForm
                (((map (Fin 2) φ.toLinearEquiv :
                      Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 2)) (Orientation ℝ F (Fin 2))) :
                    (a : Orientation ℝ E (Fin 2)) → Orientation ℝ F (Fin 2))
                  o) :
              (a : F) → F →ₗ[ℝ] ℝ)
            x :
          F →ₗ[ℝ] ℝ) :
        (a : F) → ℝ)
      y =
    ⟪(φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E), y⟫
⊢ ⟪(rightAngleRotation
            (((map (Fin 2) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 2)) (Orientation ℝ F (Fin 2))) :
                (a : Orientation ℝ E (Fin 2)) → Orientation ℝ F (Fin 2))
              o) :
          (a : F) → F)
        x,
      y⟫ =
    ⟪(φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E), y⟫

Tactic:
rw [inner_rightAngleRotation_left]

Premises used: Orientation.inner_rightAngleRotation_left
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
trans :
  (((areaForm
                (((map (Fin 2) φ.toLinearEquiv :
                      Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 2)) (Orientation ℝ F (Fin 2))) :
                    (a : Orientation ℝ E (Fin 2)) → Orientation ℝ F (Fin 2))
                  o) :
              (a : F) → F →ₗ[ℝ] ℝ)
            x :
          F →ₗ[ℝ] ℝ) :
        (a : F) → ℝ)
      y =
    inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E)
      ((φ.symm : (a : F) → E) y : E)
trans₁ :
  inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E)
      ((φ.symm : (a : F) → E) y : E) =
    ⟪(φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E), y⟫
⊢ (((areaForm
                (((map (Fin 2) φ.toLinearEquiv :
                      Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 2)) (Orientation ℝ F (Fin 2))) :
                    (a : Orientation ℝ E (Fin 2)) → Orientation ℝ F (Fin 2))
                  o) :
              (a : F) → F →ₗ[ℝ] ℝ)
            x :
          F →ₗ[ℝ] ℝ) :
        (a : F) → ℝ)
      y =
    ⟪(φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E), y⟫

Tactic:
trans ⟪J (φ.symm x), φ.symm y⟫

Premises used: LinearIsometryEquiv.symm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ (((areaForm
                (((map (Fin 2) φ.toLinearEquiv :
                      Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 2)) (Orientation ℝ F (Fin 2))) :
                    (a : Orientation ℝ E (Fin 2)) → Orientation ℝ F (Fin 2))
                  o) :
              (a : F) → F →ₗ[ℝ] ℝ)
            x :
          F →ₗ[ℝ] ℝ) :
        (a : F) → ℝ)
      y =
    inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E)
      ((φ.symm : (a : F) → E) y : E)

Tactic:
simp [o.areaForm_map]

Premises used: Orientation.areaForm_map
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
trans :
  inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E)
      ((φ.symm : (a : F) → E) y : E) =
    inner.{0, u_2} ℝ (E := F)
      ((φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E) : F)
      ((φ : (a : E) → F) ((φ.symm : (a : F) → E) y : E) : F)
trans₁ :
  inner.{0, u_2} ℝ (E := F)
      ((φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E) : F)
      ((φ : (a : E) → F) ((φ.symm : (a : F) → E) y : E) : F) =
    ⟪(φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E), y⟫
⊢ inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E)
      ((φ.symm : (a : F) → E) y : E) =
    ⟪(φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E), y⟫

Tactic:
trans ⟪φ (J (φ.symm x)), φ (φ.symm y)⟫

Premises used: LinearIsometryEquiv.symm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
rw rw₁ :
  inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E)
      ((φ.symm : (a : F) → E) y : E) =
    inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E)
      ((φ.symm : (a : F) → E) y : E)
⊢ inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E)
      ((φ.symm : (a : F) → E) y : E) =
    inner.{0, u_2} ℝ (E := F)
      ((φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E) : F)
      ((φ : (a : E) → F) ((φ.symm : (a : F) → E) y : E) : F)

Tactic:
rw [φ.inner_map_map]

Premises used: LinearIsometryEquiv.inner_map_map
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ inner.{0, u_2} ℝ (E := F)
      ((φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E) : F)
      ((φ : (a : E) → F) ((φ.symm : (a : F) → E) y : E) : F) =
    ⟪(φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E), y⟫

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x : E
⊢ Eq (α := E)
    ((φ : (a : E) → E)
        ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : E) → E) ((φ : (a : E) → E) x : E) : E) : E) :
      E)
    ((rightAngleRotation ((map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o) :
          (a : E) → E)
        ((φ : (a : E) → E) x : E) :
      E)

Tactic:
(o.rightAngleRotation_map φ (φ x)).symm

Premises used: Orientation.rightAngleRotation_map, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x : E
h : x = (φ.symm : (a : E) → E) ((φ : (a : E) → E) x : E)
h₁ : o = (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o
⊢ Eq (α := E) ((φ : (a : E) → E) ((o.rightAngleRotation : (a : E) → E) x : E) : E)
    ((o.rightAngleRotation : (a : E) → E) ((φ : (a : E) → E) x : E) : E)

Tactic:
convert! (o.rightAngleRotation_map φ (φ x)).symm

Premises used: Orientation.rightAngleRotation_map, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x : E
⊢ x = (φ.symm : (a : E) → E) ((φ : (a : E) → E) x : E)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x : E
h : (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o = o
⊢ o = (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o

Tactic:
symm
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x : E
h : Fintype.card (Fin 2) = finrank ℝ E
⊢ (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o = o

Tactic:
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ

Premises used: LinearIsometryEquiv.toLinearEquiv, Orientation.map_eq_iff_det_pos
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x : E
h : Fintype.card (Fin 2) = 2
h₁ h₂ : Eq (α := ℕ) 2 2
⊢ Fintype.card (Fin 2) = finrank ℝ E

Tactic:
rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]

Premises used: Fintype.card_fin, Fact.out
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
inst_5 : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
⊢ rightAngleRotation
      (((map (Fin 2) φ.toLinearEquiv : Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 2)) (Orientation ℝ F (Fin 2))) :
          (a : Orientation ℝ E (Fin 2)) → Orientation ℝ F (Fin 2))
        o) =
    LinearIsometryEquiv.trans (φ.symm.trans o.rightAngleRotation) φ

Tactic:
LinearIsometryEquiv.ext <| o.rightAngleRotation_map φ

Premises used: Orientation.rightAngleRotation_map, LinearIsometryEquiv.ext
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
⊢ Eq (α := E ≃ₗᵢ[ℝ] E) (o.rightAngleRotation.trans φ) (φ.trans o.rightAngleRotation)

Tactic:
LinearIsometryEquiv.ext <| o.linearIsometryEquiv_comp_rightAngleRotation φ hφ

Premises used: Orientation.linearIsometryEquiv_comp_rightAngleRotation, LinearIsometryEquiv.ext
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
i : Fin 2
0 : Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ≠ 0
1 : Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ≠ 0
⊢ ![x, (o.rightAngleRotation : (a : E) → E) x] i ≠ 0

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
⊢ Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ≠ 0

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
⊢ Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ≠ 0

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
i j : Fin 2
hij : i ≠ j
0 :
  ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j),
    ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)),
        ![x, (o.rightAngleRotation : (a : E) → E) x] j⟫ =
      0
1 :
  ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j),
    ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)),
        ![x, (o.rightAngleRotation : (a : E) → E) x] j⟫ =
      0
⊢ ⟪![x, (o.rightAngleRotation : (a : E) → E) x] i, ![x, (o.rightAngleRotation : (a : E) → E) x] j⟫ = 0

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
0 :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)),
        Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))⟫ =
      0
h :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)),
        Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))⟫ =
      0
⊢ ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)),
      ![x, (o.rightAngleRotation : (a : E) → E) x] j⟫ =
    0

Tactic:
fin_cases j
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
1 :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)),
        Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))⟫ =
      0
h :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)),
        Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))⟫ =
      0
⊢ ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)),
      ![x, (o.rightAngleRotation : (a : E) → E) x] j⟫ =
    0

Tactic:
fin_cases j
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)),
      Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))⟫ =
    0

Tactic:
simp_all
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)),
      Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))⟫ =
    0

Tactic:
simp_all