From 602296031d471832609d7016eabf7116837b017d Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sat, 29 Jun 2024 09:17:43 +0200
Subject: [PATCH] Update bilinear.lean

---
 Nevanlinna/bilinear.lean | 33 +++++++++------------------------
 1 file changed, 9 insertions(+), 24 deletions(-)

diff --git a/Nevanlinna/bilinear.lean b/Nevanlinna/bilinear.lean
index 02c514a..ea1d5a1 100644
--- a/Nevanlinna/bilinear.lean
+++ b/Nevanlinna/bilinear.lean
@@ -1,16 +1,6 @@
---import Mathlib.Algebra.BigOperators.Basic
-import Mathlib.LinearAlgebra.TensorProduct.Basic
-import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.Analysis.InnerProductSpace.PiL2
 
-open BigOperators
-open Finset
-open scoped TensorProduct
-
-variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
-variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
-
+open TensorProduct
 
 
 lemma OrthonormalBasis.sum_repr'
@@ -33,19 +23,17 @@ noncomputable def InnerProductSpace.canonicalTensor
 
 theorem InnerProductSpace.InvariantTensor
   (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
-  (v₂ : OrthonormalBasis (Fin (FiniteDimensional.finrank ℝ E)) ℝ E)
-  : InnerProductSpace.canonicalTensor E = ∑ i, (v₂ i) ⊗ₜ[ℝ] (v₂ i) := by
+  (v : OrthonormalBasis (Fin (FiniteDimensional.finrank ℝ E)) ℝ E)
+  : InnerProductSpace.canonicalTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by
 
   unfold InnerProductSpace.canonicalTensor
-
   let v₁ := stdOrthonormalBasis ℝ E
-  simp
 
   conv =>
     right
     arg 2
     intro i
-    rw [v₁.sum_repr' (v₂ i)]
+    rw [v₁.sum_repr' (v i)]
   simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul]
   
   conv =>
@@ -61,13 +49,10 @@ theorem InnerProductSpace.InvariantTensor
     arg 2
     intro i
     rw [← real_inner_comm (v₁ x)]
-  simp_rw [OrthonormalBasis.sum_inner_mul_inner v₂]
+  simp_rw [OrthonormalBasis.sum_inner_mul_inner v]
 
-  have xx {r₀ : Fin (FiniteDimensional.finrank ℝ E)} : ∀ r₁ : Fin (FiniteDimensional.finrank ℝ E), r₁ ≠ r₀ → ⟪v₁ r₀, v₁ r₁⟫_ℝ • v₁ r₀ ⊗ₜ[ℝ] v₁ r₁ = 0 := by
+  have {x : Fin (FiniteDimensional.finrank ℝ E)} : ∑ x_1 : Fin (FiniteDimensional.finrank ℝ E), ⟪v₁ x, v₁ x_1⟫_ℝ • v₁ x ⊗ₜ[ℝ] v₁ x_1 = v₁ x ⊗ₜ[ℝ] v₁ x := by
+    rw [Fintype.sum_eq_single x, orthonormal_iff_ite.1 v₁.orthonormal]; simp
     intro r₁ hr₁
-    rw [orthonormal_iff_ite.1 v₁.orthonormal]
-    simp
-    tauto
-  simp_rw [Fintype.sum_eq_single _ xx]
-  simp_rw [orthonormal_iff_ite.1 v₁.orthonormal]
-  simp
+    rw [orthonormal_iff_ite.1 v₁.orthonormal]; simp; tauto
+  simp_rw [this]