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
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
⊢ 0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) →
    SameRay ℝ x y
have neg : 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))
Tactic: suffices ↑0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • J x) by
      rw [← (o.basisRightAngleRotation x hx).sum_repr y]
      simp only [Fin.sum_univ_succ, coe_basisRightAngleRotation, Matrix.cons_val_zero,
        Fin.succ_zero_eq_one', Finset.univ_eq_empty, Finset.sum_empty, areaForm_apply_self,
        map_smul, map_add, real_inner_smul_right, inner_add_right, Matrix.cons_val_one,
        smul_eq_mul, areaForm_rightAngleRotation_right,
        mul_zero, add_zero, zero_add, neg_zero, inner_rightAngleRotation_right,
        real_inner_self_eq_norm_sq]
      exact this
-- 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
h : SameRay ℝ x y
⊢ 0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ)
have neg : ∀ (r : ℝ) (hr : 0 ≤ r) (h : SameRay ℝ x (r • x)),
  0 ≤ ⟪x, r • x⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) (r • x) : ℝ) (0 : ℝ)
Tactic: obtain ⟨r, hr, rfl⟩ := h.exists_nonneg_left hx
Cleared hypotheses: y, 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)
x : E
hx : ¬x = 0
r : ℝ
hr : 0 ≤ r
h : SameRay ℝ x (r • x)
⊢ 0 ≤ ⟪x, r • x⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) (r • x) : ℝ) (0 : ℝ)
have neg : 0 ≤ r * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: simp only [inner_smul_right, real_inner_self_eq_norm_sq, map_smulₛₗ, areaForm_apply_self,
      smul_eq_mul, mul_zero, and_true]
-- 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
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) y : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) x : ℂ) : ℂ)
have simp : (↑⟪x, y⟫ : ℂ) +
    HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) Complex.I =
  (starRingEnd ℂ : (a : ℂ) → ℂ)
    ((↑⟪y, x⟫ : ℂ) +
      HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) y : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) Complex.I)
Tactic: simp only [kahler_apply_apply]
-- 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, y⟫ : ℂ) +
      HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) Complex.I =
    (starRingEnd ℂ : (a : ℂ) → ℂ)
      ((↑⟪y, x⟫ : ℂ) +
        HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) y : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) Complex.I)
have rw : (↑⟪y, x⟫ : ℂ) +
    HSMul.hSMul (α := ℝ) (-(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) y : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) Complex.I =
  (starRingEnd ℂ : (a : ℂ) → ℂ)
    ((↑⟪y, x⟫ : ℂ) +
      HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) y : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) Complex.I)
Tactic: rw [real_inner_comm, areaForm_swap]
-- 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.kahler : (a : E) → E →ₗ[ℝ] ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y =
    HMul.hMul (β := ℂ) (-Complex.I) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
have simp : (↑((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y) : ℂ) + -(↑⟪x, y⟫ : ℂ) * Complex.I =
  -Complex.I *
    ((↑⟪x, y⟫ : ℂ) + (↑((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y) : ℂ) * Complex.I)
Tactic: simp only [o.areaForm_rightAngleRotation_left, o.inner_rightAngleRotation_left,
    o.kahler_apply_apply, Complex.ofReal_neg, Complex.real_smul]
-- 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.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) y : E) =
    HMul.hMul (β := ℂ) Complex.I ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
have simp : -(↑((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y) : ℂ) + (↑⟪x, y⟫ : ℂ) * Complex.I =
  Complex.I *
    ((↑⟪x, y⟫ : ℂ) + (↑((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y) : ℂ) * Complex.I)
Tactic: simp only [o.areaForm_rightAngleRotation_right, o.inner_rightAngleRotation_right,
    o.kahler_apply_apply, Complex.ofReal_neg, Complex.real_smul]
-- 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
⊢ Eq (α := ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : E →ₗ[ℝ] ℂ) : (a : E) → ℂ)
        ((o.rightAngleRotation : (a : E) → E) y : E) :
      ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
have simp : Complex.I * HMul.hMul (β := ℂ) (-Complex.I) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
  (((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y
Tactic: simp only [kahler_rightAngleRotation_left, kahler_rightAngleRotation_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)
a x y : E
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
have trans : HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
  HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
Tactic: trans ((‖a‖ ^ 2 :) : ℂ) * o.kahler x 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)
a x y : E
trans :
  HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
have trans₁ : HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
  HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
Tactic: trans ((‖a‖ ^ 2 :) : ℂ) * o.kahler x 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)
a x y : E
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
have a₁ : (HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).re =
  (HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).re
Tactic: apply Complex.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 y : E
a₁ :
  (HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
        ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).re =
    (HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
        ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).re
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
have a₂ : (HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).im =
  (HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).im
Tactic: apply Complex.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 y : E
⊢ (HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
        ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).re =
    (HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
        ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).re
have a₁ : (⟪x, a⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1)) *
      (⟪a, y⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1)) -
    (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0)) *
      (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0)) =
  HPow.hPow (β := ℕ) ‖a‖ 2 *
      (⟪x, y⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1)) -
    0 *
      (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0))
Tactic: simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re,
        Complex.mul_im, Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
-- 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 y : E
⊢ (⟪x, a⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) *
        (⟪a, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) -
      (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) =
    HPow.hPow (β := ℕ) ‖a‖ 2 *
        (⟪x, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) -
      0 *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0))
have a₁ : (⟪a, x⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) (-(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1)) *
      (⟪a, y⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1)) -
    (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) (-(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0)) *
      (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0)) =
  HPow.hPow (β := ℕ) ‖a‖ 2 *
      (⟪x, y⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1)) -
    0 *
      (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0))
Tactic: rw [real_inner_comm a x, o.areaForm_swap x a]
-- 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 y : E
⊢ (HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
        ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).im =
    (HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
        ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).im
have a₁ : (⟪x, a⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1)) *
      (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0)) +
    (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0)) *
      (⟪a, y⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1)) =
  HPow.hPow (β := ℕ) ‖a‖ 2 *
      (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0)) +
    0 *
      (⟪x, y⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1))
Tactic: simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re,
        Complex.mul_im, Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
-- 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 y : E
⊢ (⟪x, a⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) +
      (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) *
        (⟪a, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) =
    HPow.hPow (β := ℕ) ‖a‖ 2 *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) +
      0 *
        (⟪x, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1))
have a₁ : (⟪a, x⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) (-(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1)) *
      (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0)) +
    (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) (-(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0)) *
      (⟪a, y⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1)) =
  HPow.hPow (β := ℕ) ‖a‖ 2 *
      (0 +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (1 : ℝ) +
          HMul.hMul (α := ℝ) 0 0)) +
    0 *
      (⟪x, y⟫ +
        (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
            (0 : ℝ) -
          HMul.hMul (α := ℝ) 0 1))
Tactic: rw [real_inner_comm a x, o.areaForm_swap x a]
-- 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 y : E
⊢ HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
have norm_cast : HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
  HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
Tactic: norm_cast
-- 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
⊢ norm (E := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) = ‖x‖ * ‖y‖
have rw : (Complex.normSq : (a : ℂ) → ℝ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
  HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2
Tactic: rw [← sq_eq_sq₀, Complex.sq_norm]
-- 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 :
  (Complex.normSq : (a : ℂ) → ℝ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2
⊢ norm (E := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) = ‖x‖ * ‖y‖
have ha : 0 ≤ norm (E := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
Tactic: rw [← sq_eq_sq₀, Complex.sq_norm]
-- 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 :
  (Complex.normSq : (a : ℂ) → ℝ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2
ha : 0 ≤ norm (E := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
⊢ norm (E := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) = ‖x‖ * ‖y‖
have hb : 0 ≤ ‖x‖ * ‖y‖
Tactic: rw [← sq_eq_sq₀, Complex.sq_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (hypothesis)
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 : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
⊢ x = 0 ∨ y = 0
have this : ‖x‖ * ‖y‖ = 0
Tactic: have : ‖x‖ * ‖y‖ = 0 := by simpa [hx] using (o.norm_kahler x y).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)
x y : E
hx : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
this : ‖x‖ * ‖y‖ = 0
⊢ x = 0 ∨ y = 0
have inl : ∀ (h : ‖x‖ = 0), x = 0 ∨ y = 0
Tactic: rcases eq_zero_or_eq_zero_of_mul_eq_zero this with h | 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)
x y : E
hx : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
this : ‖x‖ * ‖y‖ = 0
inl : ∀ (h : ‖x‖ = 0), x = 0 ∨ y = 0
⊢ x = 0 ∨ y = 0
have inr : ∀ (h : ‖y‖ = 0), x = 0 ∨ y = 0
Tactic: rcases eq_zero_or_eq_zero_of_mul_eq_zero this with h | 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)
x y : E
hx : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 0 ∨ y = 0
have inl : x = 0
Tactic: left