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

Proof state:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6483.«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 * ‖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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a) ((o.basisRightAngleRotation a ha) i) =
      (‖a‖ ^ 2 • (innerₛₗ ℝ) 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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a) ((o.basisRightAngleRotation a ha) i) =
    (‖a‖ ^ 2 • (innerₛₗ ℝ) x) ((o.basisRightAngleRotation a ha) i)

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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) 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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a) ((o.basisRightAngleRotation a ha) i) =
      (‖a‖ ^ 2 • (innerₛₗ ℝ) x) ((o.basisRightAngleRotation a ha) i)

Proof state:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6483.«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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a)
      ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨1, ⋯⟩)) =
    (‖a‖ ^ 2 • (innerₛₗ ℝ) 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.add_apply,
  LinearMap.smul_apply, innerₛₗ_apply, inner_rightAngleRotation_right, areaForm_apply_self,
  neg_zero, smul_eq_mul, mul_zero, areaForm_rightAngleRotation_right,
  real_inner_self_eq_norm_sq, zero_add, mul_neg]

Result:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6483.«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
⊢ (o.areaForm a) x * ‖a‖ ^ 2 = -(‖a‖ ^ 2 * (o.areaForm x) a)

Proof state:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6483.«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
⊢ (o.areaForm a) x * ‖a‖ ^ 2 = -(‖a‖ ^ 2 * (o.areaForm x) a)

Tactic:
rw [o.areaForm_swap]

Result:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6483.«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
⊢ -(o.areaForm x) a * ‖a‖ ^ 2 = -(‖a‖ ^ 2 * (o.areaForm x) a)

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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) 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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) 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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) x

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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a) ((o.basisRightAngleRotation a ha) i) =
    (‖a‖ ^ 2 • (innerₛₗ ℝ) x) ((o.basisRightAngleRotation a ha) i)

Tactic:
fin_cases i

Result:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6483.«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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a)
      ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨0, ⋯⟩)) =
    (‖a‖ ^ 2 • (innerₛₗ ℝ) x) ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨0, ⋯⟩))

case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6483.«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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a)
      ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨1, ⋯⟩)) =
    (‖a‖ ^ 2 • (innerₛₗ ℝ) x) ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨1, ⋯⟩))

Proof state:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6483.«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
⊢ -(o.areaForm x) a * ‖a‖ ^ 2 = -(‖a‖ ^ 2 * (o.areaForm x) a)

Tactic:
ring

Result:
no goals

Proof state:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6483.«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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a)
      ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨0, ⋯⟩)) =
    (‖a‖ ^ 2 • (innerₛₗ ℝ) x) ((o.basisRightAngleRotation a ha) ((fun i => i) ⟨0, ⋯⟩))

Tactic:
simp only [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, innerₛₗ_apply,
  real_inner_self_eq_norm_sq, smul_eq_mul, areaForm_apply_self, mul_zero, add_zero,
  real_inner_comm]

Result:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim._hyg.6483.«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 * ‖a‖ ^ 2 = ‖a‖ ^ 2 * inner a 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 • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) x

Tactic:
simp [ha]

Result:
no goals