feat(linear_algebra/pi): add linear_equiv.Pi_congr_left (#8070)

This definition was hiding inside the proof for `is_noetherian_pi`

src/linear_algebra/pi.lean

@@ -23,9 +23,9 @@ It contains theorems relating these to each other, as well as to `linear_map.ker
 
 -/
 
-universes u v w x y z u' v' w' y'
+universes u v w x y z u' v' w' x' y'
 variables {R : Type u} {K : Type u'} {M : Type v} {V : Type v'} {M₂ : Type w} {V₂ : Type w'}
-variables {M₃ : Type y} {V₃ : Type y'} {M₄ : Type z} {ι : Type x}
+variables {M₃ : Type y} {V₃ : Type y'} {M₄ : Type z} {ι : Type x} {ι' : Type x'}
 
 open function submodule
 open_locale big_operators
@@ -242,12 +242,13 @@ variables [semiring R] {φ ψ χ : ι → Type*} [∀ i, add_comm_monoid (φ i)]
 variables [∀ i, add_comm_monoid (ψ i)] [∀ i, module R (ψ i)]
 variables [∀ i, add_comm_monoid (χ i)] [∀ i, module R (χ i)]
 
-/-- Combine a family of linear equivalences into a linear equivalence of `pi`-types. -/
+/-- Combine a family of linear equivalences into a linear equivalence of `pi`-types.
+
+This is `equiv.Pi_congr_right` as a `linear_equiv` -/
 @[simps apply] def Pi_congr_right (e : Π i, φ i ≃ₗ[R] ψ i) : (Π i, φ i) ≃ₗ[R] (Π i, ψ i) :=
 { to_fun := λ f i, e i (f i),
   inv_fun := λ f i, (e i).symm (f i),
   map_smul' := λ c f, by { ext, simp },
-  left_inv := λ f, by { ext, simp },
   .. add_equiv.Pi_congr_right (λ j, (e j).to_add_equiv) }
 
 @[simp]
@@ -262,6 +263,22 @@ lemma Pi_congr_right_trans (e : Π i, φ i ≃ₗ[R] ψ i) (f : Π i, ψ i ≃
   (Pi_congr_right e).trans (Pi_congr_right f) = (Pi_congr_right $ λ i, (e i).trans (f i)) :=
 rfl
 
+variables (R φ)
+
+/-- Transport dependent functions through an equivalence of the base space.
+
+This is `equiv.Pi_congr_left'` as a `linear_equiv`. -/
+@[simps {simp_rhs := tt}]
+def Pi_congr_left' (e : ι ≃ ι') : (Π i', φ i') ≃ₗ[R] (Π i, φ $ e.symm i) :=
+{ map_add' := λ x y, rfl, map_smul' := λ x y, rfl, .. equiv.Pi_congr_left' φ e }
+
+/-- Transporting dependent functions through an equivalence of the base,
+expressed as a "simplification".
+
+This is `equiv.Pi_congr_left` as a `linear_equiv` -/
+def Pi_congr_left (e : ι' ≃ ι) : (Π i', φ (e i')) ≃ₗ[R] (Π i, φ i) :=
+(Pi_congr_left' R φ e.symm).symm
+
 variables (ι R M) (S : Type*) [fintype ι] [decidable_eq ι] [semiring S]
   [add_comm_monoid M] [module R M] [module S M] [smul_comm_class R S M]
 

src/ring_theory/noetherian.lean

@@ -389,22 +389,17 @@ instance is_noetherian_pi {R ι : Type*} {M : ι → Type*} [ring R]
   [∀ i, is_noetherian R (M i)] : is_noetherian R (Π i, M i) :=
 begin
   haveI := classical.dec_eq ι,
-  suffices : ∀ s : finset ι, is_noetherian R (Π i : (↑s : set ι), M i),
-  { letI := this finset.univ,
-    refine @is_noetherian_of_linear_equiv _ _ _ _ _ _ _ _
-      ⟨_, _, _, _, _, _⟩ (this finset.univ),
-    { exact λ f i, f ⟨i, finset.mem_univ _⟩ },
-    { intros, ext, refl },
-    { intros, ext, refl },
-    { exact λ f i, f i.1 },
-    { intro, ext ⟨⟩, refl },
-    { intro, ext i, refl } },
+  suffices on_finset : ∀ s : finset ι, is_noetherian R (Π i : s, M i),
+  { let coe_e := equiv.subtype_univ_equiv finset.mem_univ,
+    letI : is_noetherian R (Π i : finset.univ, M (coe_e i)) := on_finset finset.univ,
+    exact is_noetherian_of_linear_equiv (linear_equiv.Pi_congr_left R M coe_e), },
   intro s,
   induction s using finset.induction with a s has ih,
   { split, intro s, convert submodule.fg_bot, apply eq_bot_iff.2,
     intros x hx, refine (submodule.mem_bot R).2 _, ext i, cases i.2 },
   refine @is_noetherian_of_linear_equiv _ _ _ _ _ _ _ _
-    ⟨_, _, _, _, _, _⟩ (@is_noetherian_prod _ (M a) _ _ _ _ _ _ _ ih),
+    _ (@is_noetherian_prod _ (M a) _ _ _ _ _ _ _ ih),
+  fconstructor,
   { exact λ f i, or.by_cases (finset.mem_insert.1 i.2)
       (λ h : i.1 = a, show M i.1, from (eq.rec_on h.symm f.1))
       (λ h : i.1 ∈ s, show M i.1, from f.2 ⟨i.1, h⟩) },
@@ -427,9 +422,9 @@ begin
       rw [dif_neg this, dif_pos his] } },
   { intro f, ext ⟨i, hi⟩,
     rcases finset.mem_insert.1 hi with rfl | h,
-    { simp only [or.by_cases, dif_pos], refl },
+    { simp only [or.by_cases, dif_pos], },
     { have : ¬i = a, { rintro rfl, exact has h },
-      simp only [or.by_cases, dif_neg this, dif_pos h], refl } }
+      simp only [or.by_cases, dif_neg this, dif_pos h], } }
 end
 
 end