-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_mul (a x y : E) : o.kahler x a * o.kahler a y = ‖a‖ ^ 2 * o.kahler x y

Proof state:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ((o.kahler x) a * (o.kahler a) y).re = (↑(‖a‖ ^ 2) * (o.kahler x) 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]

Result:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner x a + ((o.areaForm x) a * 0 - 0 * 1)) * (inner a y + ((o.areaForm a) y * 0 - 0 * 1)) -
      (0 + ((o.areaForm x) a * 1 + 0 * 0)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) =
    ‖a‖ ^ 2 * (inner x y + ((o.areaForm x) y * 0 - 0 * 1)) - 0 * (0 + ((o.areaForm x) y * 1 + 0 * 0))

Proof state:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner a x + (-(o.areaForm a) x * 0 - 0 * 1)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) +
      (0 + (-(o.areaForm a) x * 1 + 0 * 0)) * (inner a y + ((o.areaForm a) y * 0 - 0 * 1)) =
    ‖a‖ ^ 2 * (0 + ((o.areaForm x) y * 1 + 0 * 0)) + 0 * (inner x y + ((o.areaForm x) y * 0 - 0 * 1))

Tactic:
linear_combination o.inner_mul_areaForm_sub a x y

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (o.kahler x) a * (o.kahler a) y = ↑‖a‖ ^ 2 * (o.kahler x) y

Tactic:
trans ((‖a‖ ^ 2 :) : ℂ) * o.kahler x y

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (o.kahler x) a * (o.kahler a) y = ↑(‖a‖ ^ 2) * (o.kahler x) y

E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ↑(‖a‖ ^ 2) * (o.kahler x) y = ↑‖a‖ ^ 2 * (o.kahler x) y

Proof state:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ((o.kahler x) a * (o.kahler a) y).im = (↑(‖a‖ ^ 2) * (o.kahler x) y).im

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]

Result:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner x a + ((o.areaForm x) a * 0 - 0 * 1)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) +
      (0 + ((o.areaForm x) a * 1 + 0 * 0)) * (inner a y + ((o.areaForm a) y * 0 - 0 * 1)) =
    ‖a‖ ^ 2 * (0 + ((o.areaForm x) y * 1 + 0 * 0)) + 0 * (inner x y + ((o.areaForm x) y * 0 - 0 * 1))

Proof state:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner a x + (-(o.areaForm a) x * 0 - 0 * 1)) * (inner a y + ((o.areaForm a) y * 0 - 0 * 1)) -
      (0 + (-(o.areaForm a) x * 1 + 0 * 0)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) =
    ‖a‖ ^ 2 * (inner x y + ((o.areaForm x) y * 0 - 0 * 1)) - 0 * (0 + ((o.areaForm x) y * 1 + 0 * 0))

Tactic:
linear_combination o.inner_mul_inner_add_areaForm_mul_areaForm a x y

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ↑(‖a‖ ^ 2) * (o.kahler x) y = ↑‖a‖ ^ 2 * (o.kahler x) y

Tactic:
norm_cast

Result:
no goals

Proof state:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner x a + ((o.areaForm x) a * 0 - 0 * 1)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) +
      (0 + ((o.areaForm x) a * 1 + 0 * 0)) * (inner a y + ((o.areaForm a) y * 0 - 0 * 1)) =
    ‖a‖ ^ 2 * (0 + ((o.areaForm x) y * 1 + 0 * 0)) + 0 * (inner x y + ((o.areaForm x) y * 0 - 0 * 1))

Tactic:
rw [real_inner_comm a x, o.areaForm_swap x a]

Result:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner a x + (-(o.areaForm a) x * 0 - 0 * 1)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) +
      (0 + (-(o.areaForm a) x * 1 + 0 * 0)) * (inner a y + ((o.areaForm a) y * 0 - 0 * 1)) =
    ‖a‖ ^ 2 * (0 + ((o.areaForm x) y * 1 + 0 * 0)) + 0 * (inner x y + ((o.areaForm x) y * 0 - 0 * 1))

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (o.kahler x) a * (o.kahler a) y = ↑(‖a‖ ^ 2) * (o.kahler x) y

Tactic:
apply Complex.ext

Result:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ((o.kahler x) a * (o.kahler a) y).re = (↑(‖a‖ ^ 2) * (o.kahler x) y).re

case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ((o.kahler x) a * (o.kahler a) y).im = (↑(‖a‖ ^ 2) * (o.kahler x) y).im

Proof state:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner x a + ((o.areaForm x) a * 0 - 0 * 1)) * (inner a y + ((o.areaForm a) y * 0 - 0 * 1)) -
      (0 + ((o.areaForm x) a * 1 + 0 * 0)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) =
    ‖a‖ ^ 2 * (inner x y + ((o.areaForm x) y * 0 - 0 * 1)) - 0 * (0 + ((o.areaForm x) y * 1 + 0 * 0))

Tactic:
rw [real_inner_comm a x, o.areaForm_swap x a]

Result:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner a x + (-(o.areaForm a) x * 0 - 0 * 1)) * (inner a y + ((o.areaForm a) y * 0 - 0 * 1)) -
      (0 + (-(o.areaForm a) x * 1 + 0 * 0)) * (0 + ((o.areaForm a) y * 1 + 0 * 0)) =
    ‖a‖ ^ 2 * (inner x y + ((o.areaForm x) y * 0 - 0 * 1)) - 0 * (0 + ((o.areaForm x) y * 1 + 0 * 0))