-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem inner_mul_areaForm_sub' (a x : E) : ⟪a, x⟫ • ω a - ω a x • innerₛₗ ℝ a = ‖a‖ ^ 2 • ω x

Proof state:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : a = 0
⊢ inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x

Tactic:
simp [ha]

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x

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

Result:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ∀ (i : Fin 2),
    (inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a) ((o.basisRightAngleRotation a ha) i) =
      (‖a‖ ^ 2 • o.areaForm x) ((o.basisRightAngleRotation a ha) i)

Proof state:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6897.«0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ (inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a)
      ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨0, ⋯⟩)) =
    (‖a‖ ^ 2 • o.areaForm x) ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨0, ⋯⟩))

Tactic:
simp only [o.areaForm_swap a x, neg_smul, sub_neg_eq_add, Fin.zero_eta, Fin.isValue, id_eq,
  coe_basisRightAngleRotation, Nat.succ_eq_add_one, Nat.reduceAdd, Matrix.cons_val_zero,
  LinearMap.add_apply, LinearMap.smul_apply, areaForm_apply_self, smul_eq_mul, mul_zero,
  innerₛₗ_apply, real_inner_self_eq_norm_sq, zero_add]

Result:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6897.«0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ (o.areaForm x) a * ‖a‖ ^ 2 = ‖a‖ ^ 2 * (o.areaForm x) a

Proof state:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6897.«1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ (inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a)
      ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨1, ⋯⟩)) =
    (‖a‖ ^ 2 • o.areaForm x) ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨1, ⋯⟩))

Tactic:
simp only [Fin.mk_one, Fin.isValue, id_eq, coe_basisRightAngleRotation, Nat.succ_eq_add_one,
  Nat.reduceAdd, Matrix.cons_val_one, Matrix.head_cons, LinearMap.sub_apply,
  LinearMap.smul_apply, areaForm_rightAngleRotation_right, real_inner_self_eq_norm_sq,
  smul_eq_mul, innerₛₗ_apply, inner_rightAngleRotation_right, areaForm_apply_self, neg_zero,
  mul_zero, sub_zero, real_inner_comm]

Result:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6897.«1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ inner a x * ‖a‖ ^ 2 = ‖a‖ ^ 2 * inner a x

Proof state:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6897.«1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ inner a x * ‖a‖ ^ 2 = ‖a‖ ^ 2 * inner a x

Tactic:
ring

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
i : Fin 2
⊢ (inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a) ((o.basisRightAngleRotation a ha) i) =
    (‖a‖ ^ 2 • o.areaForm x) ((o.basisRightAngleRotation a ha) i)

Tactic:
fin_cases i

Result:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6897.«0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ (inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a)
      ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨0, ⋯⟩)) =
    (‖a‖ ^ 2 • o.areaForm x) ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨0, ⋯⟩))

case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6897.«1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ (inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a)
      ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨1, ⋯⟩)) =
    (‖a‖ ^ 2 • o.areaForm x) ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨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 : E
⊢ inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x

Tactic:
by_cases ha : a = 0

Result:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : a = 0
⊢ inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x

Proof state:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6897.«0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ (o.areaForm x) a * ‖a‖ ^ 2 = ‖a‖ ^ 2 * (o.areaForm x) a

Tactic:
ring

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ∀ (i : Fin 2),
    (inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a) ((o.basisRightAngleRotation a ha) i) =
      (‖a‖ ^ 2 • o.areaForm x) ((o.basisRightAngleRotation a ha) i)

Tactic:
intro i

Result:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
i : Fin 2
⊢ (inner a x • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a) ((o.basisRightAngleRotation a ha) i) =
    (‖a‖ ^ 2 • o.areaForm x) ((o.basisRightAngleRotation a ha) i)