chore(linear_algebra/basic): simplify two proofs (#2123)

* chore(linear_algebra/basic): simplify two proofs

Also drop `linear_map.congr_right` in favor of
`linear_equiv.congr_right`. I'll restore the deleted `congr_right`
as `comp_map : (M₂ →ₗ[R] M₃) →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] (M →ₗ[R] M₃)` soon.

* Fix compile

* Restore `congr_right` under the name `comp_right`.

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: urkud

src/linear_algebra/basic.lean

@@ -293,7 +293,7 @@ module.of_core $ by refine { smul := (•), ..};
 
 /-- Composition by `f : M₂ → M₃` is a linear map from the space of linear maps `M → M₂` to the space of
 linear maps `M₂ → M₃`. -/
-def congr_right (f : M₂ →ₗ[R] M₃) : (M →ₗ[R] M₂) →ₗ[R] (M →ₗ[R] M₃) :=
+def comp_right (f : M₂ →ₗ[R] M₃) : (M →ₗ[R] M₂) →ₗ[R] (M →ₗ[R] M₃) :=
 ⟨linear_map.comp f,
 λ _ _, linear_map.ext $ λ _, f.2 _ _,
 λ _ _, linear_map.ext $ λ _, f.3 _ _⟩
@@ -626,53 +626,39 @@ lemma span_union (s t : set M) : span R (s ∪ t) = span R s ⊔ span R t :=
 lemma span_Union {ι} (s : ι → set M) : span R (⋃ i, s i) = ⨆ i, span R (s i) :=
 (submodule.gi R M).gc.l_supr
 
-@[simp] theorem Union_coe_of_directed {ι} (hι : nonempty ι)
-  (S : ι → submodule R M)
-  (H : ∀ i j, ∃ k, S i ≤ S k ∧ S j ≤ S k) :
+@[simp] theorem coe_supr_of_directed {ι} [hι : nonempty ι]
+  (S : ι → submodule R M) (H : directed (≤) S) :
   ((supr S : submodule R M) : set M) = ⋃ i, S i :=
 begin
   refine subset.antisymm _ (Union_subset $ le_supr S),
-  rw [show supr S = ⨆ i, span R (S i), by simp, ← span_Union],
-  unfreezeI,
-  refine λ x hx, span_induction hx (λ _, id) _ _ _,
-  { cases hι with i, exact mem_Union.2 ⟨i, by simp⟩ },
-  { simp, intros x y i hi j hj,
+  suffices : (span R (⋃ i, (S i : set M)) : set M) ⊆ ⋃ (i : ι), ↑(S i),
+    by simpa only [span_Union, span_eq] using this,
+  refine (λ x hx, span_induction hx (λ _, id) _ _ _);
+    simp only [mem_Union, exists_imp_distrib],
+  { exact hι.elim (λ i, ⟨i, (S i).zero_mem⟩) },
+  { intros x y i hi j hj,
     rcases H i j with ⟨k, ik, jk⟩,
     exact ⟨k, add_mem _ (ik hi) (jk hj)⟩ },
-  { simp [-mem_coe]; exact λ a x i hi, ⟨i, smul_mem _ a hi⟩ },
+  { exact λ a x i hi, ⟨i, smul_mem _ a hi⟩ },
 end
 
 lemma mem_supr_of_mem {ι : Sort*} {b : M} (p : ι → submodule R M) (i : ι) (h : b ∈ p i) :
   b ∈ (⨆i, p i) :=
 have p i ≤ (⨆i, p i) := le_supr p i,
 @this b h
 
-@[simp] theorem mem_supr_of_directed {ι} (hι : nonempty ι)
-  (S : ι → submodule R M)
-  (H : ∀ i j, ∃ k, S i ≤ S k ∧ S j ≤ S k) {x} :
+@[simp] theorem mem_supr_of_directed {ι} [nonempty ι]
+  (S : ι → submodule R M) (H : directed (≤) S) {x} :
   x ∈ supr S ↔ ∃ i, x ∈ S i :=
-by rw [← mem_coe, Union_coe_of_directed hι S H, mem_Union]; refl
+by { rw [← mem_coe, coe_supr_of_directed S H, mem_Union], refl }
 
 theorem mem_Sup_of_directed {s : set (submodule R M)}
-  {z} (hzs : z ∈ Sup s) (x ∈ s)
-  (hdir : ∀ i ∈ s, ∀ j ∈ s, ∃ k ∈ s, i ≤ k ∧ j ≤ k) :
-  ∃ y ∈ s, z ∈ y :=
+  {z} (hs : s.nonempty) (hdir : directed_on (≤) s) :
+  z ∈ Sup s ↔ ∃ y ∈ s, z ∈ y :=
 begin
-  haveI := classical.dec, rw Sup_eq_supr at hzs,
-  have : ∃ (i : submodule R M), z ∈ ⨆ (H : i ∈ s), i,
-  { refine (mem_supr_of_directed ⟨⊥⟩ _ (λ i j, _)).1 hzs,
-    by_cases his : i ∈ s; by_cases hjs : j ∈ s,
-    { rcases hdir i his j hjs with ⟨k, hks, hik, hjk⟩,
-        exact ⟨k, le_supr_of_le hks (supr_le $ λ _, hik),
-          le_supr_of_le hks (supr_le $ λ _, hjk)⟩ },
-    { exact ⟨i, le_refl _, supr_le $ hjs.elim⟩ },
-    { exact ⟨j, supr_le $ his.elim, le_refl _⟩ },
-    { exact ⟨⊥, supr_le $ his.elim, supr_le $ hjs.elim⟩ } },
-  cases this with N hzn, by_cases hns : N ∈ s,
-  { have : (⨆ (H : N ∈ s), N) ≤ N := supr_le (λ _, le_refl _),
-    exact ⟨N, hns, this hzn⟩ },
-  { have : (⨆ (H : N ∈ s), N) ≤ ⊥ := supr_le hns.elim,
-    cases (mem_bot R).1 (this hzn), exact ⟨x, H, x.zero_mem⟩ }
+  haveI : nonempty s := hs.to_subtype,
+  rw [Sup_eq_supr, supr_subtype', mem_supr_of_directed, subtype.exists],
+  exact (directed_on_iff_directed _).1 hdir
 end
 
 section
@@ -1475,7 +1461,7 @@ def congr_right (f : M₂ ≃ₗ[R] M₃) : (M →ₗ[R] M₂) ≃ₗ (M →ₗ
 
 /-- If M and M₂ are linearly isomorphic then the two spaces of linear maps from M and M₂ to themselves
 are linearly isomorphic. -/
-def conj (e : M ≃ₗ[R] M₂) : (M →ₗ[R] M) ≃ₗ[R] (M₂ →ₗ[R] M₂) := arrow_congr e e
+def conj (e : M ≃ₗ[R] M₂) : (module.End R M) ≃ₗ[R] (module.End R M₂) := arrow_congr e e
 
 end comm_ring
 

src/ring_theory/ideal_operations.lean

@@ -379,7 +379,7 @@ le_antisymm (le_Inf $ λ J hJ, hJ.2.radical_le_iff.2 hJ.1) $
 λ r hr, classical.by_contradiction $ λ hri,
 let ⟨m, (hrm : r ∉ radical m), him, hm⟩ := zorn.zorn_partial_order₀ {K : ideal R | r ∉ radical K}
   (λ c hc hcc y hyc, ⟨Sup c, λ ⟨n, hrnc⟩, let ⟨y, hyc, hrny⟩ :=
-      submodule.mem_Sup_of_directed hrnc y hyc hcc.directed_on in hc hyc ⟨n, hrny⟩,
+      (submodule.mem_Sup_of_directed ⟨y, hyc⟩ hcc.directed_on).1 hrnc in hc hyc ⟨n, hrny⟩,
     λ z, le_Sup⟩) I hri in
 have ∀ x ∉ m, r ∈ radical (m ⊔ span {x}) := λ x hxm, classical.by_contradiction $ λ hrmx, hxm $
   hm (m ⊔ span {x}) hrmx le_sup_left ▸ (le_sup_right : _ ≤ m ⊔ span {x}) (subset_span $ set.mem_singleton _),

src/ring_theory/ideals.lean

@@ -142,7 +142,8 @@ begin
     cases h J J0 (le_of_lt hJ), exact lt_irrefl _ hJ },
   { intros S SC cC I IS,
     refine ⟨Sup S, λ H, _, λ _, le_Sup⟩,
-    rcases submodule.mem_Sup_of_directed ((eq_top_iff_one _).1 H) I IS cC.directed_on with ⟨J, JS, J0⟩,
+    obtain ⟨J, JS, J0⟩ : ∃ J ∈ S, (1 : α) ∈ J,
+      from (submodule.mem_Sup_of_directed ⟨I, IS⟩ cC.directed_on).1 ((eq_top_iff_one _).1 H),
     exact SC JS ((eq_top_iff_one _).2 J0) }
 end
 

src/ring_theory/noetherian.lean

@@ -250,10 +250,9 @@ theorem is_noetherian_iff_well_founded
   have hN' : ∀ {a b}, a ≤ b → N a ≤ N b :=
     λ a b, (strict_mono.le_iff_le (λ _ _, hN.1)).2,
   have : t ⊆ ⋃ i, (N i : set β),
-  { rw [← submodule.Union_coe_of_directed _ N _],
+  { rw [← submodule.coe_supr_of_directed N _],
     { show t ⊆ M, rw ← h₂,
       apply submodule.subset_span },
-    { apply_instance },
     { exact λ i j, ⟨max i j,
         hN' (le_max_left _ _),
         hN' (le_max_right _ _)⟩ } },

src/ring_theory/polynomial.lean

@@ -213,7 +213,6 @@ begin
   simp only [mem_leading_coeff_nth],
   { split, { rintro ⟨i, p, hpI, hpdeg, rfl⟩, exact ⟨p, hpI, rfl⟩ },
     rintro ⟨p, hpI, rfl⟩, exact ⟨nat_degree p, p, hpI, degree_le_nat_degree, rfl⟩ },
-  { exact ⟨0⟩ },
   intros i j, exact ⟨i + j, I.leading_coeff_nth_mono (nat.le_add_right _ _),
     I.leading_coeff_nth_mono (nat.le_add_left _ _)⟩
 end