awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
this :
  inner ℝ (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) y : E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) =
    ⟪y, x⟫
rw :
  -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) y : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) =
    ⟪y, -x⟫
rw₁ :
  -inner ℝ (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) y : E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) =
    ⟪y, -x⟫
rw₂ : -⟪y, x⟫ = ⟪y, -x⟫
⊢ ⟪y, (o.rightAngleRotationAux₁ : (a : E) → E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)⟫ = ⟪y, -x⟫
have rw₃ : -⟪y, x⟫ = -⟪y, x⟫
Tactic: rw [o.inner_rightAngleRotationAux₁_right, ← o.inner_rightAngleRotationAux₁_left, this,
    inner_neg_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ o.rightAngleRotationAux₂.toLinearMap ∘ₗ (-o.rightAngleRotationAux₁) = LinearMap.id
have h : ∀ (x : E),
  Eq (α := E) ((o.rightAngleRotationAux₂.toLinearMap ∘ₗ (-o.rightAngleRotationAux₁) : (a : E) → E) x : E)
    ((LinearMap.id : (a : E) → E) x : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ (-o.rightAngleRotationAux₁) ∘ₗ o.rightAngleRotationAux₂.toLinearMap = LinearMap.id
have h : ∀ (x : E),
  Eq (α := E) (((-o.rightAngleRotationAux₁) ∘ₗ o.rightAngleRotationAux₂.toLinearMap : (a : E) → E) x : E)
    ((LinearMap.id : (a : E) → E) x : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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⟫ = (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y
have rw : ⟪(LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) sorry sorry : (a : E) → E) x, y⟫ =
  (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y
Tactic: rw [rightAngleRotation]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y
have rw : ⟪x, (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) sorry sorry : (a : E) → E) y⟫ =
  -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y
Tactic: rw [rightAngleRotation]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ (o.rightAngleRotation : (a : E) → E) ((o.rightAngleRotation : (a : E) → E) x : E) = -x
have rw : (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) sorry sorry : (a : E) → E)
    ((LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) sorry sorry : (a : E) → E) x :
      E) =
  -x
Tactic: rw [rightAngleRotation]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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.symm = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ)
have rw : Eq (α := E ≃ₗᵢ[ℝ] E)
  (LinearIsometryEquiv.symm
    (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) sorry sorry))
  (LinearIsometryEquiv.trans
    (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) sorry sorry)
    (LinearIsometryEquiv.neg ℝ))
Tactic: rw [rightAngleRotation]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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 →ₗ[ℝ] ℝ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y =
    -⟪x, y⟫
have 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)
Tactic: rw [← o.inner_comp_rightAngleRotation, o.inner_rightAngleRotation_right, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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)
⊢ (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y =
    -⟪x, y⟫
have 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 :
    ℝ)
Tactic: rw [← o.inner_comp_rightAngleRotation, o.inner_rightAngleRotation_right, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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 :
      ℝ)
⊢ (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y =
    -⟪x, y⟫
have 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 : ℝ)
Tactic: rw [← o.inner_comp_rightAngleRotation, o.inner_rightAngleRotation_right, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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) → ℝ) ((o.rightAngleRotation : (a : E) → E) y : E) =
    ⟪x, y⟫
have rw : inner ℝ (E := E) ((o.rightAngleRotation : (a : E) → E) x : E) ((o.rightAngleRotation : (a : E) → E) y : E) = ⟪x, y⟫
Tactic: rw [← o.inner_rightAngleRotation_left, o.inner_comp_rightAngleRotation]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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⟫
⊢ (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) ((o.rightAngleRotation : (a : E) → E) y : E) =
    ⟪x, y⟫
have rw₁ : ⟪x, y⟫ = ⟪x, y⟫
Tactic: rw [← o.inner_rightAngleRotation_left, o.inner_comp_rightAngleRotation]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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.trans o.rightAngleRotation = LinearIsometryEquiv.neg ℝ
have h : ∀ (x : E),
  Eq (α := E) ((o.rightAngleRotation.trans o.rightAngleRotation : (a : E) → E) x : E)
    ((LinearIsometryEquiv.neg ℝ : (a : E) → E) x : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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 : (a : E) → E) x : E) (-(o.rightAngleRotation : (a : E) → E) x : E)
have apply : ∀ (v : E), ⟪((-o).rightAngleRotation : (a : E) → E) x, v⟫ = ⟪-(o.rightAngleRotation : (a : E) → E) x, v⟫
Tactic: apply ext_inner_right ℝ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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⟫ = ⟪-(o.rightAngleRotation : (a : E) → E) x, y⟫
have rw : ((((-o).areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y = ⟪-(o.rightAngleRotation : (a : E) → E) x, y⟫
Tactic: rw [inner_rightAngleRotation_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ 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)
have 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⟫
Tactic: apply ext_inner_right ℝ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ ⟪(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⟫
have 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⟫
Tactic: rw [inner_rightAngleRotation_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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 =
    ⟪(φ : (a : E) → F) ((o.rightAngleRotation : (a : E) → E) ((φ.symm : (a : F) → E) x : E) : E), y⟫
have 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)
Tactic: trans ⟪J (φ.symm x), φ.symm y⟫
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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)
⊢ (((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⟫
have 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⟫
Tactic: trans ⟪J (φ.symm x), φ.symm y⟫
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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 ℝ (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⟫
have 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)
Tactic: trans ⟪φ (J (φ.symm x)), φ (φ.symm y)⟫
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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)
⊢ 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⟫
have 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⟫
Tactic: trans ⟪φ (J (φ.symm x)), φ (φ.symm y)⟫
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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 ℝ (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)
have 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)
Tactic: rw [φ.inner_map_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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) x : E) : E)
    ((o.rightAngleRotation : (a : E) → E) ((φ : (a : E) → E) x : E) : E)
have h : x = (φ.symm : (a : E) → E) ((φ : (a : E) → E) x : E)
Tactic: convert! (o.rightAngleRotation_map φ (φ x)).symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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)
⊢ Eq (α := E) ((φ : (a : E) → E) ((o.rightAngleRotation : (a : E) → E) x : E) : E)
    ((o.rightAngleRotation : (a : E) → E) ((φ : (a : E) → E) x : E) : E)
have h₁ : o = (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o
Tactic: convert! (o.rightAngleRotation_map φ (φ x)).symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ o = (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o
have h : (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o = o
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o = o
have h : Fintype.card (Fin 2) = finrank ℝ E
Tactic: rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ Fintype.card (Fin 2) = finrank ℝ E
have h : Fintype.card (Fin 2) = 2
Tactic: rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ Fintype.card (Fin 2) = finrank ℝ E
have h₁ : Eq (α := ℕ) 2 2
Tactic: rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ ![x, (o.rightAngleRotation : (a : E) → E) x] i ≠ 0
have 0 : Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ≠ 0
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ ![x, (o.rightAngleRotation : (a : E) → E) x] i ≠ 0
have 1 : Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ≠ 0
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ ⟪![x, (o.rightAngleRotation : (a : E) → E) x] i, ![x, (o.rightAngleRotation : (a : E) → E) x] j⟫ = 0
have 0 : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨0, sorry⟩ ≠ j),
  ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)),
      ![x, (o.rightAngleRotation : (a : E) → E) x] j⟫ =
    0
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ ⟪![x, (o.rightAngleRotation : (a : E) → E) x] i, ![x, (o.rightAngleRotation : (a : E) → E) x] j⟫ = 0
have 1 : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨1, sorry⟩ ≠ j),
  ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)),
      ![x, (o.rightAngleRotation : (a : E) → E) x] j⟫ =
    0
Tactic: fin_cases i
Cleared hypotheses: i, hij