chore(analysis/inner_product_space/basic): extract common variables (#11214)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: hrmacbeth

src/analysis/inner_product_space/basic.lean

@@ -1577,10 +1577,11 @@ open_locale direct_sum
 def orthogonal_family (V : ι → submodule 𝕜 E) : Prop :=
 ∀ ⦃i j⦄, i ≠ j → ∀ {v : E} (hv : v ∈ V i) {w : E} (hw : w ∈ V j), ⟪v, w⟫ = 0
 
-variables {𝕜} {V : ι → submodule 𝕜 E} [dec_V : Π i (x : V i), decidable (x ≠ 0)]
+variables {𝕜} {V : ι → submodule 𝕜 E} (hV : orthogonal_family 𝕜 V)
+  [dec_V : Π i (x : V i), decidable (x ≠ 0)]
 
-include dec_ι
-lemma orthogonal_family.eq_ite (hV : orthogonal_family 𝕜 V) {i j : ι} (v : V i) (w : V j) :
+include hV dec_ι
+lemma orthogonal_family.eq_ite {i j : ι} (v : V i) (w : V j) :
   ⟪(v:E), w⟫ = ite (i = j) ⟪(v:E), w⟫ 0 :=
 begin
   split_ifs,
@@ -1589,8 +1590,7 @@ begin
 end
 
 include dec_V
-lemma orthogonal_family.inner_right_dfinsupp (hV : orthogonal_family 𝕜 V)
-  (l : Π₀ i, V i) (i : ι) (v : V i) :
+lemma orthogonal_family.inner_right_dfinsupp (l : ⨁ i, V i) (i : ι) (v : V i) :
   ⟪(v : E), dfinsupp.lsum ℕ (λ i, (V i).subtype) l⟫ = ⟪v, l i⟫ :=
 calc ⟪(v : E), dfinsupp.lsum ℕ (λ i, (V i).subtype) l⟫
     = l.sum (λ j, λ w, ⟪(v:E), w⟫) :
@@ -1615,8 +1615,7 @@ begin
 end
 omit dec_ι dec_V
 
-lemma orthogonal_family.inner_right_fintype
-  [fintype ι] (hV : orthogonal_family 𝕜 V) (l : Π i, V i) (i : ι) (v : V i) :
+lemma orthogonal_family.inner_right_fintype [fintype ι] (l : Π i, V i) (i : ι) (v : V i) :
   ⟪(v : E), ∑ j : ι, l j⟫ = ⟪v, l i⟫ :=
 by classical;
 calc ⟪(v : E), ∑ j : ι, l j⟫
@@ -1628,8 +1627,7 @@ calc ⟪(v : E), ∑ j : ι, l j⟫
 /-- An orthogonal family forms an independent family of subspaces; that is, any collection of
 elements each from a different subspace in the family is linearly independent. In particular, the
 pairwise intersections of elements of the family are 0. -/
-lemma orthogonal_family.independent (hV : orthogonal_family 𝕜 V) :
-  complete_lattice.independent V :=
+lemma orthogonal_family.independent : complete_lattice.independent V :=
 begin
   classical,
   apply complete_lattice.independent_of_dfinsupp_lsum_injective,
@@ -1646,13 +1644,12 @@ end
 
 /-- The composition of an orthogonal family of subspaces with an injective function is also an
 orthogonal family. -/
-lemma orthogonal_family.comp (hV : orthogonal_family 𝕜 V) {γ : Type*} {f : γ → ι}
-  (hf : function.injective f) :
+lemma orthogonal_family.comp {γ : Type*} {f : γ → ι} (hf : function.injective f) :
   orthogonal_family 𝕜 (V ∘ f) :=
 λ i j hij v hv w hw, hV (hf.ne hij) hv hw
 
-lemma orthogonal_family.orthonormal_sigma_orthonormal (hV : orthogonal_family 𝕜 V) {α : ι → Type*}
-  {v_family : Π i, (α i) → V i} (hv_family : ∀ i, orthonormal 𝕜 (v_family i)) :
+lemma orthogonal_family.orthonormal_sigma_orthonormal {α : ι → Type*} {v_family : Π i, (α i) → V i}
+  (hv_family : ∀ i, orthonormal 𝕜 (v_family i)) :
   orthonormal 𝕜 (λ a : Σ i, α i, (v_family a.1 a.2 : E)) :=
 begin
   split,
@@ -1667,7 +1664,7 @@ begin
 end
 
 include dec_ι
-lemma direct_sum.submodule_is_internal.collected_basis_orthonormal (hV : orthogonal_family 𝕜 V)
+lemma direct_sum.submodule_is_internal.collected_basis_orthonormal
   (hV_sum : direct_sum.submodule_is_internal V) {α : ι → Type*}
   {v_family : Π i, basis (α i) 𝕜 (V i)} (hv_family : ∀ i, orthonormal 𝕜 (v_family i)) :
   orthonormal 𝕜 (hV_sum.collected_basis v_family) :=