From dd84aa07484b6daf2d3ffa56d17dc49f22c8a18a Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Mon, 26 Feb 2024 12:57:04 +0000
Subject: [PATCH] fix

---
 src/linear_algebra/my_ips/pos.lean            | 10 ++--
 src/linear_algebra/my_matrix/basic.lean       |  3 +-
 .../my_matrix/include_block.lean              | 49 ++++++++++---------
 .../pos_eq_linear_map_is_positive.lean        |  2 +-
 src/linear_algebra/of_norm.lean               |  6 +--
 src/linear_algebra/pi_direct_sum.lean         |  8 ++-
 6 files changed, 40 insertions(+), 38 deletions(-)

diff --git a/src/linear_algebra/my_ips/pos.lean b/src/linear_algebra/my_ips/pos.lean
index cb01da9711..466efafc46 100644
--- a/src/linear_algebra/my_ips/pos.lean
+++ b/src/linear_algebra/my_ips/pos.lean
@@ -360,8 +360,10 @@ begin
     exact h, }
 end
 
-lemma ext_inner_left_iff [inner_product_space 𝕜 E] (x y : E) :
-  x = y ↔ ∀ v : E, ⟪x, v⟫ = ⟪y, v⟫ :=
+lemma ext_inner_left_iff {𝕜 E : Type*}
+  [is_R_or_C 𝕜] [normed_add_comm_group E]
+  [inner_product_space 𝕜 E] (x y : E) :
+  x = y ↔ ∀ v : E, inner x v = (inner y v : 𝕜) :=
 begin
   split,
   { intros h v,
@@ -398,7 +400,7 @@ begin
     rw [mul_inv_of_self, one_apply] at ugh,
     exact ugh,
     rw ugh,
-    exact t1.1, exact _inst_4, exact _inst_6, },
+    exact t1.1, },
   { intro x,
     by_cases b : ⅟ T x = 0,
     { rw [b, inner_zero_right, map_zero], },
@@ -533,7 +535,7 @@ begin
 end
 
 open_locale big_operators
-lemma linear_map.is_positive_iff_eq_sum_rank_one {n : ℕ} [inner_product_space 𝕜 E]
+lemma linear_map.is_positive_iff_eq_sum_rank_one {n : ℕ}
   [decidable_eq 𝕜] [finite_dimensional 𝕜 E] (hn : finite_dimensional.finrank 𝕜 E = n)
   (T : E →ₗ[𝕜] E) :
   T.is_positive ↔ ∃ (m : ℕ) (u : fin m → E),
diff --git a/src/linear_algebra/my_matrix/basic.lean b/src/linear_algebra/my_matrix/basic.lean
index f33be712f4..9dcec91ff3 100644
--- a/src/linear_algebra/my_matrix/basic.lean
+++ b/src/linear_algebra/my_matrix/basic.lean
@@ -267,7 +267,8 @@ begin
   simp only [matrix.transpose_apply, matrix.kronecker_map, of_apply],
 end
 
-lemma matrix.kronecker.conj (x y : matrix n n 𝕜) :
+lemma matrix.kronecker.conj
+  {n : Type*} (x y : matrix n n 𝕜) :
   (x ⊗ₖ y)ᴴᵀ = xᴴᵀ ⊗ₖ yᴴᵀ :=
 by rw [conj, matrix.kronecker_conj_transpose, matrix.kronecker.transpose]; refl
 
diff --git a/src/linear_algebra/my_matrix/include_block.lean b/src/linear_algebra/my_matrix/include_block.lean
index 5e84cd7e4c..055735dec3 100644
--- a/src/linear_algebra/my_matrix/include_block.lean
+++ b/src/linear_algebra/my_matrix/include_block.lean
@@ -98,9 +98,9 @@ linear_map.single i
 --     { intros h,
 --       simp only [h, pi.zero_apply, dif_neg, not_false_iff, smul_zero], }, } }
 
-lemma include_block_apply {o : Type*} [fintype o] [decidable_eq o] {m' : o → Type*}
+lemma include_block_apply {o : Type*} [decidable_eq o] {m' : o → Type*}
   {α : Type*}
-  [Π i, fintype (m' i)] [Π i, decidable_eq (m' i)] [comm_semiring α] {i : o} (x : matrix (m' i) (m' i) α) :
+  [comm_semiring α] {i : o} (x : matrix (m' i) (m' i) α) :
   (include_block : matrix (m' i) (m' i) α →ₗ[α] Π j, matrix (m' j) (m' j) α) x
     = λ (j : o), dite (i = j) (λ h, eq.mp (by rw [h]) x) (λ _, 0) :=
 begin
@@ -224,8 +224,8 @@ lemma is_block_diagonal.eq {k : Type*} [decidable_eq k]
   block_diagonal' (x.block_diag') = x :=
 hx
 
-lemma is_block_diagonal.add {k : Type*} [fintype k] [decidable_eq k]
-  {s : k → Type*} [Π i, fintype (s i)] [Π i, decidable_eq (s i)]
+lemma is_block_diagonal.add {k : Type*} [decidable_eq k]
+  {s : k → Type*}
   {x y : matrix (Σ i, s i) (Σ i, s i) R} (hx : x.is_block_diagonal)
   (hy : y.is_block_diagonal) :
   (x + y).is_block_diagonal :=
@@ -294,8 +294,8 @@ lemma is_block_diagonal.coe_zero {k : Type*} [fintype k] [decidable_eq k]
   ((0 : { x : matrix (Σ i, s i) (Σ i, s i) R // x.is_block_diagonal }) : matrix (Σ i, s i) (Σ i, s i) R) = 0 :=
 rfl
 
-lemma is_block_diagonal.smul  {k : Type*} [fintype k] [decidable_eq k]
-  {s : k → Type*} [Π i, fintype (s i)] [Π i, decidable_eq (s i)]
+lemma is_block_diagonal.smul  {k : Type*} [decidable_eq k]
+  {s : k → Type*}
   {x : matrix (Σ i, s i) (Σ i, s i) R} (hx : x.is_block_diagonal) (α : R) :
   (α • x).is_block_diagonal :=
 begin
@@ -342,15 +342,15 @@ begin
   rw [matrix.is_block_diagonal, block_diag'_block_diagonal'],
 end
 
-lemma is_block_diagonal_iff {k : Type*} [fintype k] [decidable_eq k]
-  {s : k → Type*} [Π i, fintype (s i)] [Π i, decidable_eq (s i)]
+lemma is_block_diagonal_iff {k : Type*} [decidable_eq k]
+  {s : k → Type*}
   (x : matrix (Σ i, s i) (Σ i, s i) R) :
   x.is_block_diagonal ↔ ∃ y : (Π i, matrix (s i) (s i) R), x = block_diagonal' y :=
 ⟨λ h, ⟨x.block_diag', h.symm⟩,
   by rintros ⟨y, rfl⟩; exact matrix.is_block_diagonal.block_diagonal' y⟩
 
-def std_basis_matrix_block_diagonal {k : Type*} [fintype k] [decidable_eq k]
-  {s : k → Type*} [Π i, fintype (s i)] [Π i, decidable_eq (s i)]
+def std_basis_matrix_block_diagonal {k : Type*} [decidable_eq k]
+  {s : k → Type*} [Π i, decidable_eq (s i)]
   (i : k) (j l : s i) (α : R) :
   {x : matrix (Σ i, s i) (Σ i, s i) R // x.is_block_diagonal} :=
 ⟨std_basis_matrix ⟨i, j⟩ ⟨i, l⟩ α, by {
@@ -469,7 +469,7 @@ begin
 end
 
 lemma is_block_diagonal.mul {k : Type*} [fintype k] [decidable_eq k]
-  {s : k → Type*} [Π i, fintype (s i)] [Π i, decidable_eq (s i)]
+  {s : k → Type*} [Π i, fintype (s i)]
   {x y : matrix (Σ i, s i) (Σ i, s i) R} (hx : x.is_block_diagonal)
   (hy : y.is_block_diagonal) :
   (x ⬝ y).is_block_diagonal :=
@@ -495,8 +495,8 @@ lemma is_block_diagonal.one {k : Type*} [decidable_eq k]
   (1 : matrix (Σ i, s i) (Σ i, s i) R).is_block_diagonal :=
 by simp only [matrix.is_block_diagonal, block_diag'_one, block_diagonal'_one]
 
-@[instance] def is_block_diagonal.has_one {k : Type*} [fintype k] [decidable_eq k]
-  {s : k → Type*} [Π i, fintype (s i)] [Π i, decidable_eq (s i)] :
+@[instance] def is_block_diagonal.has_one {k : Type*} [decidable_eq k]
+  {s : k → Type*} [Π i, decidable_eq (s i)] :
   has_one {x : matrix (Σ i, s i) (Σ i, s i) R // x.is_block_diagonal} :=
 { one := ⟨(1 : matrix (Σ i, s i) (Σ i, s i) R), is_block_diagonal.one⟩ }
 
@@ -625,8 +625,8 @@ x.2
       is_block_diagonal.coe_block_diagonal'_block_diag' (x * y),
       is_block_diagonal.coe_mul, mul_eq_mul], }, }
 
-lemma is_block_diagonal.star {R : Type*} [comm_semiring R] [star_add_monoid R] {k : Type*} [fintype k] [decidable_eq k]
-  {s : k → Type*} [Π i, fintype (s i)] [Π i, decidable_eq (s i)]
+lemma is_block_diagonal.star {R : Type*} [comm_semiring R] [star_add_monoid R] {k : Type*} [decidable_eq k]
+  {s : k → Type*}
   {x : matrix (Σ i, s i) (Σ i, s i) R} (hx : x.is_block_diagonal) :
   (xᴴ).is_block_diagonal :=
 begin
@@ -705,7 +705,7 @@ end
     refl, }, }
 
 lemma is_block_diagonal.apply_of_ne {R : Type*} [comm_semiring R] {k : Type*}
-  [fintype k] [decidable_eq k] {s : k → Type*} [Π i, fintype (s i)] [Π i, decidable_eq (s i)]
+  [decidable_eq k] {s : k → Type*}
   {x : matrix (Σ i, s i) (Σ i, s i) R} (hx : x.is_block_diagonal)
   (i j : Σ i, s i) (h : i.1 ≠ j.1) :
   x i j = 0 :=
@@ -745,8 +745,8 @@ end
   [Π i, fintype (s i)] [Π i, decidable_eq (s i)] :
   ((Π i, matrix (s i) (s i) R) →ₗ[R] (Π i, matrix (s i) (s i) R))
     ≃ₐ[R]
-  { x : matrix (Σ i, s i) (Σ i, s i) R // x.is_block_diagonal }
-    →ₗ[R] { x : matrix (Σ i, s i) (Σ i, s i) R // x.is_block_diagonal } :=
+  ({ x : matrix (Σ i, s i) (Σ i, s i) R // x.is_block_diagonal }
+    →ₗ[R] { x : matrix (Σ i, s i) (Σ i, s i) R // x.is_block_diagonal }) :=
 is_block_diagonal_pi_alg_equiv.symm.to_linear_equiv.inner_conj
 
 end matrix
@@ -760,14 +760,15 @@ local notation `ℍ_ `i := matrix (s i) (s i) R
 open matrix
 
 lemma tensor_product.assoc_include_block
+  {k : Type*} [decidable_eq k] {s : k → Type*}
   {i j : k} :
-  ↑(tensor_product.assoc R ℍ₂ ℍ₂ ℍ₂).symm ∘ₗ
-    ((include_block : (ℍ_ i) →ₗ[R] ℍ₂)
-      ⊗ₘ ((include_block : (ℍ_ j) →ₗ[R] ℍ₂) ⊗ₘ (include_block : (ℍ_ j) →ₗ[R] ℍ₂)))
+  ↑(tensor_product.assoc R (Π a, matrix (s a) (s a) R) (Π a, matrix (s a) (s a) R) (Π a, matrix (s a) (s a) R)).symm ∘ₗ
+    ((include_block : (matrix (s i) (s i) R) →ₗ[R] Π a, matrix (s a) (s a) R)
+      ⊗ₘ ((include_block : (matrix (s j) (s j) R) →ₗ[R] Π a, matrix (s a) (s a) R) ⊗ₘ (include_block : (matrix (s j) (s j) R) →ₗ[R] Π a, matrix (s a) (s a) R)))
   =
-   (((include_block : (ℍ_ i) →ₗ[R] ℍ₂)
-      ⊗ₘ ((include_block : (ℍ_ j) →ₗ[R] ℍ₂))) ⊗ₘ (include_block : (ℍ_ j) →ₗ[R] ℍ₂)) ∘ₗ
-    ↑(tensor_product.assoc R (ℍ_ i) (ℍ_ j) (ℍ_ j)).symm :=
+   (((include_block : (matrix (s i) (s i) R) →ₗ[R] Π a, matrix (s a) (s a) R)
+      ⊗ₘ ((include_block : (matrix (s j)(s j) R) →ₗ[R] Π a, matrix (s a) (s a) R))) ⊗ₘ (include_block : (matrix (s j) (s j) R) →ₗ[R] Π a, matrix (s a) (s a) R)) ∘ₗ
+    ↑(tensor_product.assoc R (matrix (s i) (s i) R) (matrix (s j) (s j) R) (matrix (s j) (s j) R)).symm :=
 begin
   apply tensor_product.ext_threefold',
   intros x y z,
diff --git a/src/linear_algebra/my_matrix/pos_eq_linear_map_is_positive.lean b/src/linear_algebra/my_matrix/pos_eq_linear_map_is_positive.lean
index b79da3f4d1..3d152c24c5 100644
--- a/src/linear_algebra/my_matrix/pos_eq_linear_map_is_positive.lean
+++ b/src/linear_algebra/my_matrix/pos_eq_linear_map_is_positive.lean
@@ -357,7 +357,7 @@ def linear_map.positive_map (T : (M₁ →ₗ[ℂ] M₁) →ₗ[ℂ] (M₂ →
 ∀ x : M₁ →ₗ[ℂ] M₁, x.is_positive → (T x).is_positive
 
 /-- a $^*$-homomorphism from $L(M_1)$ to $L(M_2)$ is a positive map -/
-lemma linear_map.positive_map.star_hom {n₁ n₂ : ℕ}
+lemma linear_map.positive_map.star_hom {n₁ : ℕ}
   [finite_dimensional ℂ M₁] [finite_dimensional ℂ M₂]
   (hn₁ : finite_dimensional.finrank ℂ M₁ = n₁)
   (φ : star_alg_hom ℂ (M₁ →ₗ[ℂ] M₁) (M₂ →ₗ[ℂ] M₂)) :
diff --git a/src/linear_algebra/of_norm.lean b/src/linear_algebra/of_norm.lean
index d67e1c20fb..1ee1796ad0 100644
--- a/src/linear_algebra/of_norm.lean
+++ b/src/linear_algebra/of_norm.lean
@@ -460,20 +460,20 @@ begin
   simp only [and_iff_right_iff_imp, f.is_linear, implies_true_iff],
 end
 
-def with_bound (𝕜 : Type*) {E : Type*}
+def with_bound {E : Type*}
   [normed_add_comm_group E] {F : Type*} [normed_add_comm_group F] (f : E → F) : Prop :=
 ∃ M, 0 < M ∧ ∀ x : E, ‖f x‖ ≤ M * ‖x‖
 
 lemma is_bounded_linear_map.def {𝕜 E : Type*} [nontrivially_normed_field 𝕜]
   [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type*} [normed_add_comm_group F]
   [normed_space 𝕜 F] {f : E → F} :
-  is_bounded_linear_map 𝕜 f ↔ (is_linear_map 𝕜 f ∧ with_bound 𝕜 f) :=
+  is_bounded_linear_map 𝕜 f ↔ (is_linear_map 𝕜 f ∧ with_bound f) :=
 ⟨λ h, ⟨h.1, h.2⟩, λ h, ⟨h.1, h.2⟩⟩
 
 lemma linear_map.with_bound_iff_is_continuous {𝕜 E : Type*} [nontrivially_normed_field 𝕜]
   [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type*} [normed_add_comm_group F]
   [normed_space 𝕜 F] {f : E →ₗ[𝕜] F} :
-  with_bound 𝕜 f ↔ continuous f :=
+  with_bound f ↔ continuous f :=
 begin
   have := @is_bounded_linear_map_iff_is_continuous_linear_map 𝕜 _ _ _ _ _ _ _ f,
   simp only [is_bounded_linear_map.def, is_continuous_linear_map, and.congr_right_iff,
diff --git a/src/linear_algebra/pi_direct_sum.lean b/src/linear_algebra/pi_direct_sum.lean
index 19bc12d5b2..f994089a46 100644
--- a/src/linear_algebra/pi_direct_sum.lean
+++ b/src/linear_algebra/pi_direct_sum.lean
@@ -62,8 +62,7 @@ def direct_sum_tensor_to_fun
       refl, } }
 
 lemma direct_sum_tensor_to_fun_apply
-  {R : Type*} [comm_semiring R] {ι₁ : Type*} {ι₂ : Type*} [decidable_eq ι₁]
-  [decidable_eq ι₂]
+  {R : Type*} [comm_semiring R] {ι₁ : Type*} {ι₂ : Type*}
   {M₁ : ι₁ → Type*} {M₂ : ι₂ → Type*} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)]
   [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)]
   [Π (i₂ : ι₂), module R (M₂ i₂)] (x : Π i, M₁ i) (y : Π i, M₂ i) (i : ι₁ × ι₂) :
@@ -83,7 +82,7 @@ def direct_sum_tensor_inv_fun {R : Type*} [comm_ring R] {ι₁ : Type*} {ι₂ :
   map_smul' := λ r x, by { simp only [smul_hom_class.map_smul, pi.smul_apply, ring_hom.id_apply],
     rw [← finset.smul_sum], } }
 
-lemma function.sum_update_eq_self {R : Type*} {ι₁ : Type*} [decidable_eq ι₁]
+lemma function.sum_update_eq_self {ι₁ : Type*} [decidable_eq ι₁]
   [fintype ι₁]
   {M₁ : ι₁ → Type*} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] (x : Π i, M₁ i) :
   ∑ (x_1 : ι₁), function.update 0 x_1 (x x_1) = x :=
@@ -122,7 +121,7 @@ begin
     by { simp only [tensor_product.tmul_sum, tensor_product.sum_tmul], }
     ... = x ⊗ₜ[R] y : _,
     congr;
-    exact @function.sum_update_eq_self R _ _ _ _ _ _, },
+    exact @function.sum_update_eq_self _ _ _ _ _ _, },
   { intros x y hx hy,
     simp only [map_add, hx, hy], },
 end
@@ -267,7 +266,6 @@ end
   [Π i, add_comm_monoid (φ i)] [Π i, module R (φ i)]
   [Π i, add_comm_monoid (ψ i)] [Π i, module R (ψ i)]
   (S : Type*) [fintype ι₁] [decidable_eq ι₁]
-  [fintype ι₂] [decidable_eq ι₂]
   [semiring S] [Π i, module S (ψ i)] [Π i, smul_comm_class R S (ψ i)] :
   (Π i : ι₁ × ι₂, φ i.1 →ₗ[R] ψ i.2)
     ≃ₗ[S] (Π i, φ i) →ₗ[R] (Π i, ψ i) :=