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 : E
hx : x ≠ 0
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

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) ⟨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

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
⊢ Eq (α := (a : Fin 2) → E) (⇑(o.basisRightAngleRotation x hx) : (a : Fin 2) → E)
    ![x, (o.rightAngleRotation : (a : E) → E) x]

Tactic:
coe_basisOfLinearIndependentOfCardEqFinrank _ _

Premises used: coe_basisOfLinearIndependentOfCardEqFinrank
-- 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)
a x : E
pos :
  ∀ (ha : a = 0),
    HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) +
        HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
          ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) =
      HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)
neg :
  ∀ (ha : ¬a = 0),
    HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) +
        HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
          ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) =
      HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)
⊢ HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) +
      HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
        ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) =
    HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)

Tactic:
by_cases ha : a = 0
-- 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)
a x : E
ha : a = 0
⊢ HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) +
      HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
        ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) =
    HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)

Tactic:
simp [ha]
-- 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)
a x : E
ha : ¬a = 0
neg :
  ∀ (i : Fin 2),
    Eq (α := ℝ)
      ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) +
              HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
                ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
                ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
            (a : E) → ℝ)
          ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) i : E) :
        ℝ)
      ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
            (a : E) → ℝ)
          ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) i : E) :
        ℝ)
⊢ HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) +
      HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
        ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) =
    HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)

Tactic:
apply (o.basisRightAngleRotation a ha).ext

Premises used: Orientation.basisRightAngleRotation, Module.Basis.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)
a x : E
ha : ¬a = 0
i : Fin 2
neg :
  Eq (α := ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) +
            HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
              ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : E) :
      ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : E) :
      ℝ)
neg₁ :
  Eq (α := ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) +
            HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
              ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : E) :
      ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : E) :
      ℝ)
⊢ Eq (α := ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) +
            HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
              ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) i : E) :
      ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) i : E) :
      ℝ)

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)
a x : E
ha : ¬a = 0
⊢ Eq (α := ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) +
            HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
              ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : E) :
      ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : E) :
      ℝ)

Tactic:
simp [mul_comm, real_inner_comm]

Premises used: mul_comm, real_inner_comm
-- 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)
a x : E
ha : ¬a = 0
⊢ Eq (α := ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) +
            HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
              ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : E) :
      ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : E) :
      ℝ)

Tactic:
simp [mul_comm, o.areaForm_swap a x]

Premises used: Orientation.areaForm_swap, mul_comm
-- 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)
a x y : E
⊢ ⟪a, x⟫ * ⟪a, y⟫ +
      HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
        ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) =
    HPow.hPow (β := ℕ) ‖a‖ 2 * ⟪x, y⟫

Tactic:
congr_arg (fun f : E →ₗ[ℝ] ℝ => f y) (o.inner_mul_inner_add_areaForm_mul_areaForm' a x)

Premises used: congr_arg, DFunLike.coe, Orientation.inner_mul_inner_add_areaForm_mul_areaForm'
-- 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)
a b : E
⊢ HPow.hPow (β := ℕ) ⟪a, b⟫ 2 +
      HPow.hPow (α := ℝ) (β := ℕ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) b : ℝ) 2 =
    HPow.hPow (β := ℕ) ‖a‖ 2 * HPow.hPow (β := ℕ) ‖b‖ 2

Tactic:
simpa [sq, real_inner_self_eq_norm_sq] using o.inner_mul_inner_add_areaForm_mul_areaForm a b b

Premises used: Orientation.inner_mul_inner_add_areaForm_mul_areaForm, sq, real_inner_self_eq_norm_sq
-- 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)
a x : E
pos :
  ∀ (ha : a = 0),
    HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) -
        HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
          ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) =
      HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)
neg :
  ∀ (ha : ¬a = 0),
    HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) -
        HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
          ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) =
      HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)
⊢ HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) -
      HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
        ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) =
    HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)

Tactic:
by_cases ha : a = 0
-- 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)
a x : E
ha : a = 0
⊢ HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) -
      HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
        ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) =
    HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)

Tactic:
simp [ha]
-- 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)
a x : E
ha : ¬a = 0
neg :
  ∀ (i : Fin 2),
    Eq (α := ℝ)
      ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) -
              HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
                ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
                ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
            (a : E) → ℝ)
          ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) i : E) :
        ℝ)
      ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
            (a : E) → ℝ)
          ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) i : E) :
        ℝ)
⊢ HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) -
      HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
        ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) =
    HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)

Tactic:
apply (o.basisRightAngleRotation a ha).ext

Premises used: Orientation.basisRightAngleRotation, Module.Basis.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)
a x : E
ha : ¬a = 0
i : Fin 2
neg :
  Eq (α := ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) -
            HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
              ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : E) :
      ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : E) :
      ℝ)
neg₁ :
  Eq (α := ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) -
            HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
              ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : E) :
      ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : E) :
      ℝ)
⊢ Eq (α := ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) -
            HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
              ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) i : E) :
      ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) i : E) :
      ℝ)

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)
a x : E
ha : ¬a = 0
⊢ Eq (α := ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) -
            HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
              ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : E) :
      ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : E) :
      ℝ)

Tactic:
simp [mul_comm, o.areaForm_swap a x]

Premises used: Orientation.areaForm_swap, mul_comm
-- 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)
a x : E
ha : ¬a = 0
⊢ Eq (α := ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) ⟪a, x⟫ ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) -
            HSMul.hSMul (α := ℝ) (β := E →ₗ[ℝ] ℝ)
              ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              ((innerₛₗ ℝ : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : E) :
      ℝ)
    ((HSMul.hSMul (β := E →ₗ[ℝ] ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2) ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((o.basisRightAngleRotation a ha : (a : Fin 2) → E) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : E) :
      ℝ)

Tactic:
simp [mul_comm, real_inner_comm]

Premises used: mul_comm, real_inner_comm
-- 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)
a x y : E
⊢ HMul.hMul (β := ℝ) ⟪a, x⟫ ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) -
      HMul.hMul (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) ⟪a, y⟫ =
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖a‖ 2)
      ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)

Tactic:
congr_arg (fun f : E →ₗ[ℝ] ℝ => f y) (o.inner_mul_areaForm_sub' a x)

Premises used: congr_arg, Orientation.inner_mul_areaForm_sub', 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)
x y : E
pos :
  ∀ (hx : x = 0),
    0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) ↔
      SameRay ℝ x y
neg :
  ∀ (hx : ¬x = 0),
    0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) ↔
      SameRay ℝ x y
⊢ 0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) ↔
    SameRay ℝ x y

Tactic:
by_cases hx : x = 0
-- 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
hx : x = 0
⊢ 0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) ↔
    SameRay ℝ x y

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 y : E
hx : ¬x = 0
neg :
  0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) →
    SameRay ℝ x y
neg₁ :
  SameRay ℝ x y →
    0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ)
⊢ 0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) ↔
    SameRay ℝ x y

Tactic:
constructor
-- 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
hx : ¬x = 0
a : ℝ := ((((o.basisRightAngleRotation x hx).repr : (a : E) → Fin 2 →₀ ℝ) y : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) 0
b : ℝ := ((((o.basisRightAngleRotation x hx).repr : (a : E) → Fin 2 →₀ ℝ) y : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) 1
this :
  0 ≤ a * HPow.hPow (β := ℕ) ‖x‖ 2 ∧ b * HPow.hPow (β := ℕ) ‖x‖ 2 = 0 →
    SameRay ℝ x (a • x + HSMul.hSMul (β := E) b ((o.rightAngleRotation : (a : E) → E) x : E))
rw :
  0 ≤
        ⟪x,
          ∑ i : Fin 2,
            HSMul.hSMul (α := ℝ) (β := E)
              (((((o.basisRightAngleRotation x hx).repr : (a : E) → Fin 2 →₀ ℝ) y : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) i :
                ℝ)
              ((o.basisRightAngleRotation x hx : (a : Fin 2) → E) i : E)⟫ ∧
      Eq (α := ℝ)
        ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
            (∑ i : Fin 2,
              HSMul.hSMul (α := ℝ) (β := E)
                (((((o.basisRightAngleRotation x hx).repr : (a : E) → Fin 2 →₀ ℝ) y : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) i :
                  ℝ)
                ((o.basisRightAngleRotation x hx : (a : Fin 2) → E) i : E)) :
          ℝ)
        (0 : ℝ) →
    SameRay ℝ x
      (∑ i : Fin 2,
        HSMul.hSMul (α := ℝ) (β := E)
          (((((o.basisRightAngleRotation x hx).repr : (a : E) → Fin 2 →₀ ℝ) y : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) i : ℝ)
          ((o.basisRightAngleRotation x hx : (a : Fin 2) → E) i : E))
⊢ 0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) →
    SameRay ℝ x y

Tactic:
rw [← (o.basisRightAngleRotation x hx).sum_repr y]

Premises used: Orientation.basisRightAngleRotation, Module.Basis.sum_repr
-- 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
hx : ¬x = 0
a : ℝ := ((((o.basisRightAngleRotation x hx).repr : (a : E) → Fin 2 →₀ ℝ) y : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) 0
b : ℝ := ((((o.basisRightAngleRotation x hx).repr : (a : E) → Fin 2 →₀ ℝ) y : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) 1
this :
  0 ≤ a * HPow.hPow (β := ℕ) ‖x‖ 2 ∧ b * HPow.hPow (β := ℕ) ‖x‖ 2 = 0 →
    SameRay ℝ x (a • x + HSMul.hSMul (β := E) b ((o.rightAngleRotation : (a : E) → E) x : E))
⊢ 0 ≤
        HMul.hMul (α := ℝ)
          (((((o.basisRightAngleRotation x hx).repr : (a : E) → Fin 2 →₀ ℝ) y : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) 0 : ℝ)
          (HPow.hPow (β := ℕ) ‖x‖ 2) ∧
      HMul.hMul (α := ℝ)
          (((((o.basisRightAngleRotation x hx).repr : (a : E) → Fin 2 →₀ ℝ) y : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) 1 : ℝ)
          (HPow.hPow (β := ℕ) ‖x‖ 2) =
        0 →
    SameRay ℝ x
      (HSMul.hSMul (α := ℝ)
          (((((o.basisRightAngleRotation x hx).repr : (a : E) → Fin 2 →₀ ℝ) y : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) 0 : ℝ)
          x +
        HSMul.hSMul (α := ℝ) (β := E)
          (((((o.basisRightAngleRotation x hx).repr : (a : E) → Fin 2 →₀ ℝ) y : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) 1 : ℝ)
          ((o.rightAngleRotation : (a : E) → E) x : E))

Tactic:
this