awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
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:
exact this
-- 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
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))
⊢ 0 ≤ ⟪x, y⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) (0 : ℝ) →
    SameRay ℝ x y

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

Tactic:
obtain ⟨r, hr, rfl⟩ := h.exists_nonneg_left hx

Premises used: SameRay.exists_nonneg_left, rfl
-- 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
r : ℝ
hr : 0 ≤ r
h : SameRay ℝ x (r • x)
neg : 0 ≤ r * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ 0 ≤ ⟪x, r • x⟫ ∧ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) (r • x) : ℝ) (0 : ℝ)

Tactic:
simp only [inner_smul_right, real_inner_self_eq_norm_sq, map_smulₛₗ, areaForm_apply_self,
      smul_eq_mul, mul_zero, and_true]

Premises used: and_true, MulActionSemiHomClass.map_smulₛₗ, MulZeroClass.mul_zero, real_inner_self_eq_norm_sq, inner_smul_right, Orientation.areaForm_apply_self, smul_eq_mul
-- 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
r : ℝ
hr : 0 ≤ r
h : SameRay ℝ x (r • x)
⊢ 0 ≤ r * HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y =
    (↑⟪x, y⟫ : ℂ) +
      HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) Complex.I

Tactic:
rfl

Premises used: rfl
-- 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
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)
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) y : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) x : ℂ) : ℂ)

Tactic:
simp only [kahler_apply_apply]

Premises used: Orientation.kahler_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
rw :
  (↑⟪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)
⊢ (↑⟪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:
rw [real_inner_comm, areaForm_swap]

Premises used: Orientation.areaForm_swap, 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)
x y : E
⊢ (↑⟪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:
simp [Complex.conj_ofReal]

Premises used: Complex.conj_ofReal
-- 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
⊢ (((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) x = HPow.hPow (β := ℕ) (↑‖x‖ : ℂ) 2

Tactic:
simp [kahler_apply_apply]

Premises used: Orientation.kahler_apply_apply
-- 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
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)
⊢ (((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 : ℂ)

Tactic:
simp only [o.areaForm_rightAngleRotation_left, o.inner_rightAngleRotation_left,
    o.kahler_apply_apply, Complex.ofReal_neg, Complex.real_smul]

Premises used: Complex.real_smul, Complex.ofReal_neg, Orientation.inner_rightAngleRotation_left, Orientation.kahler_apply_apply, Orientation.areaForm_rightAngleRotation_left
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (↑((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y) : ℂ) + -(↑⟪x, y⟫ : ℂ) * Complex.I =
    -Complex.I *
      ((↑⟪x, y⟫ : ℂ) + (↑((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y) : ℂ) * Complex.I)

Tactic:
linear_combination ω x y * Complex.I_sq

Premises used: Complex.I_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)
x y : E
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)
⊢ (((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 : ℂ)

Tactic:
simp only [o.areaForm_rightAngleRotation_right, o.inner_rightAngleRotation_right,
    o.kahler_apply_apply, Complex.ofReal_neg, Complex.real_smul]

Premises used: Complex.real_smul, Complex.ofReal_neg, Orientation.inner_rightAngleRotation_right, Orientation.kahler_apply_apply, Orientation.areaForm_rightAngleRotation_right
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ -(↑((((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:
linear_combination -ω x y * Complex.I_sq

Premises used: Complex.I_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)
x y : E
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
⊢ 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 : ℂ)

Tactic:
simp only [kahler_rightAngleRotation_left, kahler_rightAngleRotation_right]

Premises used: Orientation.kahler_rightAngleRotation_left, Orientation.kahler_rightAngleRotation_right
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 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:
linear_combination -o.kahler x y * Complex.I_sq

Premises used: Complex.I_sq, DFunLike.coe, Orientation.kahler
-- 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
⊢ -(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:
linear_combination -o.kahler x y * Complex.I_sq

Premises used: Complex.I_sq, DFunLike.coe, Orientation.kahler
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Eq (α := ℂ) (((((-o).kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) : ℂ)

Tactic:
simp [kahler_apply_apply, Complex.conj_ofReal]

Premises used: Orientation.kahler_apply_apply, Complex.conj_ofReal
-- 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
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 : ℂ)
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 : ℂ)
⊢ 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

Premises used: Norm.norm, Complex.ofReal, HPow.hPow, OfNat.ofNat, DFunLike.coe, Orientation.kahler
-- 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₁ :
  (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
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
⊢ 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:
apply Complex.ext

Premises used: Complex.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 y : E
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))
⊢ (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:
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]

Premises used: Complex.mul_im, Complex.real_smul, Complex.add_im, Complex.mul_re, Complex.add_re, Complex.I_re, Complex.I_im, Complex.ofReal_re, Orientation.kahler_apply_apply, Complex.ofReal_im
-- 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₁ :
  (⟪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))
⊢ (⟪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:
rw [real_inner_comm a x, o.areaForm_swap x a]

Premises used: Orientation.areaForm_swap, 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
⊢ (⟪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:
linear_combination o.inner_mul_inner_add_areaForm_mul_areaForm a x y

Premises used: Orientation.inner_mul_inner_add_areaForm_mul_areaForm