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 : E
hx : x ≠ 0
j : Fin 2
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
have 0 : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)),
  ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)),
      Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))⟫ =
    0
Tactic: fin_cases j
Cleared hypotheses: j, 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
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
⊢ ⟪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
have 0₁ : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)),
  ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)),
      Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))⟫ =
    0
Tactic: fin_cases j
Cleared hypotheses: j, 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
j : Fin 2
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
have 1 : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)),
  ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)),
      Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))⟫ =
    0
Tactic: fin_cases j
Cleared hypotheses: j, 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
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
⊢ ⟪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
have 1₁ : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)),
  ⟪Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)),
      Matrix.vecCons (n := 1) x ![(o.rightAngleRotation : (a : E) → E) x] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))⟫ =
    0
Tactic: fin_cases j
Cleared hypotheses: j, 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)
a 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 →ₗ[ℝ] ℝ)
have 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 →ₗ[ℝ] ℝ)
Tactic: by_cases ha : a = 0
-- 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)
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 →ₗ[ℝ] ℝ)
⊢ 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 →ₗ[ℝ] ℝ)
have 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 →ₗ[ℝ] ℝ)
Tactic: by_cases ha : a = 0
-- 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)
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 →ₗ[ℝ] ℝ)
have 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) :
      ℝ)
Tactic: apply (o.basisRightAngleRotation a ha).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)
a x : E
ha : ¬a = 0
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) :
      ℝ)
have 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, sorry⟩) : 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, sorry⟩) : E) :
    ℝ)
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)
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) :
      ℝ)
⊢ 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) :
      ℝ)
have 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, sorry⟩) : 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, sorry⟩) : E) :
    ℝ)
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)
a 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 →ₗ[ℝ] ℝ)
have 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 →ₗ[ℝ] ℝ)
Tactic: by_cases ha : a = 0
-- 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)
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 →ₗ[ℝ] ℝ)
⊢ 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 →ₗ[ℝ] ℝ)
have 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 →ₗ[ℝ] ℝ)
Tactic: by_cases ha : a = 0
-- 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)
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 →ₗ[ℝ] ℝ)
have 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) :
      ℝ)
Tactic: apply (o.basisRightAngleRotation a ha).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)
a x : E
ha : ¬a = 0
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) :
      ℝ)
have 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, sorry⟩) : 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, sorry⟩) : E) :
    ℝ)
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)
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) :
      ℝ)
⊢ 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) :
      ℝ)
have 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, sorry⟩) : 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, sorry⟩) : E) :
    ℝ)
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 y : E
⊢ 0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) ↔
    SameRay ℝ x y
have pos : ∀ (hx : x = 0),
  0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) ↔
    SameRay ℝ x y
Tactic: by_cases hx : x = 0
-- 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
pos :
  ∀ (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
have neg : ∀ (hx : ¬x = 0),
  0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) ↔
    SameRay ℝ x y
Tactic: by_cases hx : x = 0
-- 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
hx : ¬x = 0
⊢ 0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) ↔
    SameRay ℝ x y
have neg : 0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) →
  SameRay ℝ x y
Tactic: constructor
-- 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
hx : ¬x = 0
neg :
  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
have neg₁ : SameRay ℝ x y →
  0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ)
Tactic: constructor
-- 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
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 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) →
    SameRay ℝ x y
have 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))
Tactic: rw [← (o.basisRightAngleRotation x hx).sum_repr y]