Merge branch 'adomani/add_a_focusing_dot' into adomani/lint_multiple_…

…goals

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -778,37 +778,10 @@ instance (N : LieSubmodule K L M) [IsTriangularizable K L M] : IsTriangularizabl
 See also `LieModule.iSup_genWeightSpace_eq_top'`. -/
 lemma iSup_genWeightSpace_eq_top [IsTriangularizable K L M] :
     ⨆ χ : L → K, genWeightSpace M χ = ⊤ := by
-  generalize h_dim : finrank K M = n
-  induction n using Nat.strongRecOn generalizing M with | ind n ih => ?_
-  obtain h' | ⟨y : L, hy : ¬ ∃ φ, genWeightSpaceOf M φ y = ⊤⟩ :=
-    forall_or_exists_not (fun (x : L) ↦ ∃ (φ : K), genWeightSpaceOf M φ x = ⊤)
-  · choose χ hχ using h'
-    replace hχ : genWeightSpace M χ = ⊤ := by simpa only [genWeightSpace, hχ] using iInf_top
-    exact eq_top_iff.mpr <| hχ ▸ le_iSup (genWeightSpace M) χ
-  · replace hy : ∀ φ, finrank K (genWeightSpaceOf M φ y) < n := fun φ ↦ by
-      simp_rw [not_exists, ← lt_top_iff_ne_top] at hy; exact h_dim ▸ Submodule.finrank_lt (hy φ)
-    replace ih : ∀ φ, ⨆ χ : L → K, genWeightSpace (genWeightSpaceOf M φ y) χ = ⊤ :=
-      fun φ ↦ ih _ (hy φ) (genWeightSpaceOf M φ y) rfl
-    replace ih : ∀ φ, ⨆ (χ : L → K) (_ : χ y = φ),
-        genWeightSpace (genWeightSpaceOf M φ y) χ = ⊤ := by
-      intro φ
-      suffices ∀ χ : L → K, χ y ≠ φ → genWeightSpace (genWeightSpaceOf M φ y) χ = ⊥ by
-        specialize ih φ; rw [iSup_split, biSup_congr this] at ih; simpa using ih
-      intro χ hχ
-      rw [eq_bot_iff, ← (genWeightSpaceOf M φ y).ker_incl, LieModuleHom.ker,
-        ← LieSubmodule.map_le_iff_le_comap, map_genWeightSpace_eq_of_injective
-        (genWeightSpaceOf M φ y).injective_incl, LieSubmodule.range_incl, ← disjoint_iff_inf_le]
-      exact (disjoint_genWeightSpaceOf K L M hχ).mono_left
-        (genWeightSpace_le_genWeightSpaceOf M y χ)
-    replace ih : ∀ φ, ⨆ (χ : L → K) (_ : χ y = φ), genWeightSpace M χ = genWeightSpaceOf M φ y := by
-      intro φ
-      have (χ : L → K) (hχ : χ y = φ) : genWeightSpace M χ =
-          (genWeightSpace (genWeightSpaceOf M φ y) χ).map (genWeightSpaceOf M φ y).incl := by
-        rw [← hχ, genWeightSpace_genWeightSpaceOf_map_incl]
-      simp_rw [biSup_congr this, ← LieSubmodule.map_iSup, ih, LieModuleHom.map_top,
-        LieSubmodule.range_incl]
-    simpa only [← ih, iSup_comm (ι := K), iSup_iSup_eq_right] using
-      iSup_genWeightSpaceOf_eq_top K L M y
+  simp only [← LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.iSup_coe_toSubmodule,
+    LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.top_coeSubmodule, genWeightSpace]
+  exact Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo (toEnd K L M)
+    (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem) (IsTriangularizable.iSup_eq_top)
 
 lemma iSup_genWeightSpace_eq_top' [IsTriangularizable K L M] :
     ⨆ χ : Weight K L M, genWeightSpace M χ = ⊤ := by

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -241,6 +241,10 @@ theorem mem_finset_inf {ι} {s : Finset ι} {p : ι → Submodule R M} {x : M} :
     x ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i := by
   simp only [← SetLike.mem_coe, finset_inf_coe, Set.mem_iInter]
 
+lemma inf_iInf {ι : Type*} [Nonempty ι] {p : ι → Submodule R M} (q : Submodule R M) :
+    q ⊓ ⨅ i, p i = ⨅ i, q ⊓ p i :=
+  SetLike.coe_injective <| by simpa only [inf_coe, iInf_coe] using Set.inter_iInter _ _
+
 theorem mem_sup_left {S T : Submodule R M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T := by
   have : S ≤ S ⊔ T := le_sup_left
   rw [LE.le] at this

Mathlib/Algebra/Module/Submodule/LinearMap.lean

@@ -183,6 +183,13 @@ lemma restrict_comp
     (g ∘ₗ f).restrict hfg = (g.restrict hg) ∘ₗ (f.restrict hf) :=
   rfl
 
+-- TODO Consider defining `Algebra R (p.compatibleMaps p)`, `AlgHom` version of `LinearMap.restrict`
+lemma restrict_smul_one
+    {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M}
+    (μ : R) (h : ∀ x ∈ p, (μ • (1 : Module.End R M)) x ∈ p := fun _ ↦ p.smul_mem μ) :
+    (μ • 1 : Module.End R M).restrict h = μ • (1 : Module.End R p) :=
+  rfl
+
 lemma restrict_commute {f g : M →ₗ[R] M} (h : Commute f g) {p : Submodule R M}
     (hf : MapsTo f p p) (hg : MapsTo g p p) :
     Commute (f.restrict hf) (g.restrict hg) := by

Mathlib/Algebra/Module/Submodule/Map.lean

@@ -120,6 +120,10 @@ theorem map_inf (f : F) {p q : Submodule R M} (hf : Injective f) :
     (p ⊓ q).map f = p.map f ⊓ q.map f :=
   SetLike.coe_injective <| Set.image_inter hf
 
+lemma map_iInf {ι : Type*} [Nonempty ι] {p : ι → Submodule R M} (f : F) (hf : Injective f) :
+    (⨅ i, p i).map f = ⨅ i, (p i).map f :=
+  SetLike.coe_injective <| by simpa only [map_coe, iInf_coe] using hf.injOn.image_iInter_eq
+
 theorem range_map_nonempty (N : Submodule R M) :
     (Set.range (fun ϕ => Submodule.map ϕ N : (M →ₛₗ[σ₁₂] M₂) → Submodule R₂ M₂)).Nonempty :=
   ⟨_, Set.mem_range.mpr ⟨0, rfl⟩⟩

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

@@ -449,6 +449,51 @@ lemma _root_.Submodule.inf_genEigenspace (f : End R M) (p : Submodule R M) {k :
       (genEigenspace (LinearMap.restrict f hfp) μ k).map p.subtype := by
   rw [f.genEigenspace_restrict _ _ _ hfp, Submodule.map_comap_eq, Submodule.range_subtype]
 
+/-- Given a family of endomorphisms `i ↦ f i`, a family of candidate eigenvalues `i ↦ μ i`, and a
+submodule `p` which is invariant wrt every `f i`, the intersection of `p` with the simultaneous
+maximal generalised eigenspace (taken over all `i`), is the same as the simultaneous maximal
+generalised eigenspace of the `f i` restricted to `p`. -/
+lemma _root_.Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo {ι : Type*} {μ : ι → R}
+    (f : ι → End R M) (p : Submodule R M) (hfp : ∀ i, MapsTo (f i) p p) :
+    p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) =
+      (⨅ i, maxGenEigenspace ((f i).restrict (hfp i)) (μ i)).map p.subtype := by
+  cases isEmpty_or_nonempty ι
+  · simp [iInf_of_isEmpty]
+  · simp_rw [inf_iInf, maxGenEigenspace, ((f _).genEigenspace _).mono.directed_le.inf_iSup_eq,
+      p.inf_genEigenspace _ (hfp _), ← Submodule.map_iSup, Submodule.map_iInf _ p.injective_subtype]
+
+/-- Given a family of endomorphisms `i ↦ f i`, a family of candidate eigenvalues `i ↦ μ i`, and a
+distinguished index `i` whose maximal generalised `μ i`-eigenspace is invariant wrt every `f j`,
+taking simultaneous maximal generalised eigenspaces is unaffected by first restricting to the
+distinguished generalised `μ i`-eigenspace. -/
+lemma iInf_maxGenEigenspace_restrict_map_subtype_eq
+    {ι : Type*} {μ : ι → R} (i : ι) (f : ι → End R M)
+    (h : ∀ j, MapsTo (f j) ((f i).maxGenEigenspace (μ i)) ((f i).maxGenEigenspace (μ i))) :
+    letI p := (f i).maxGenEigenspace (μ i)
+    letI q (j : ι) := maxGenEigenspace ((f j).restrict (h j)) (μ j)
+    (⨅ j, q j).map p.subtype = ⨅ j, (f j).maxGenEigenspace (μ j) := by
+  have : Nonempty ι := ⟨i⟩
+  set p := (f i).maxGenEigenspace (μ i)
+  have : ⨅ j, (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ j, (f j).maxGenEigenspace (μ j) := by
+    refine le_antisymm ?_ inf_le_right
+    simpa only [le_inf_iff, le_refl, and_true] using iInf_le _ _
+  rw [Submodule.map_iInf _ p.injective_subtype, this, Submodule.inf_iInf]
+  simp_rw [maxGenEigenspace_def, Submodule.map_iSup,
+    ((f _).genEigenspace _).mono.directed_le.inf_iSup_eq, p.inf_genEigenspace (f _) (h _)]
+  rfl
+
+lemma mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo
+    {p : Submodule R M} (f g : End R M) (hf : MapsTo f p p) (hg : MapsTo g p p) {μ₁ μ₂ : R}
+    (h : MapsTo f (g.maxGenEigenspace μ₁) (g.maxGenEigenspace μ₂)) :
+    MapsTo (f.restrict hf)
+      (maxGenEigenspace (g.restrict hg) μ₁)
+      (maxGenEigenspace (g.restrict hg) μ₂) := by
+  intro x hx
+  simp_rw [SetLike.mem_coe, mem_maxGenEigenspace, ← LinearMap.restrict_smul_one _,
+    LinearMap.restrict_sub _, LinearMap.pow_restrict _, LinearMap.restrict_apply,
+    Submodule.mk_eq_zero, ← mem_maxGenEigenspace] at hx ⊢
+  exact h hx
+
 /-- If `p` is an invariant submodule of an endomorphism `f`, then the `μ`-eigenspace of the
 restriction of `f` to `p` is a submodule of the `μ`-eigenspace of `f`. -/
 theorem eigenspace_restrict_le_eigenspace (f : End R M) {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p)

Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

@@ -222,3 +222,52 @@ theorem Module.End.iSup_genEigenspace_restrict_eq_top
   simp_rw [Submodule.inf_genEigenspace f p h, Submodule.comap_subtype_self,
     ← Submodule.map_iSup, Submodule.comap_map_eq_of_injective h_inj] at this
   exact this.symm
+
+/-- Given a family of endomorphisms `i ↦ f i` which are compatible in the sense that every maximal
+generalised eigenspace of `f i` is invariant wrt `f j`, if each `f i` is triangularizable, the
+family is simultaneously triangularizable. -/
+lemma Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo
+    {ι : Type*} [FiniteDimensional K V]
+    (f : ι → End K V)
+    (h : ∀ i j φ, MapsTo (f i) ((f j).maxGenEigenspace φ) ((f j).maxGenEigenspace φ))
+    (h' : ∀ i, ⨆ μ, (f i).maxGenEigenspace μ = ⊤) :
+    ⨆ χ : ι → K, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤ := by
+  generalize h_dim : finrank K V = n
+  induction n using Nat.strongRecOn generalizing V with | ind n ih => ?_
+  obtain this | ⟨i : ι, hy : ¬ ∃ φ, (f i).maxGenEigenspace φ = ⊤⟩ :=
+    forall_or_exists_not (fun j : ι ↦ ∃ φ : K, (f j).maxGenEigenspace φ = ⊤)
+  · choose χ hχ using this
+    replace hχ : ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤ := by simpa
+    simp_rw [eq_top_iff] at hχ ⊢
+    exact le_trans hχ <| le_iSup (fun χ : ι → K ↦ ⨅ i, (f i).maxGenEigenspace (χ i)) χ
+  · replace hy : ∀ φ, finrank K ((f i).maxGenEigenspace φ) < n := fun φ ↦ by
+      simp_rw [not_exists, ← lt_top_iff_ne_top] at hy; exact h_dim ▸ Submodule.finrank_lt (hy φ)
+    have hi (j : ι) (φ : K) :
+        MapsTo (f j) ((f i).maxGenEigenspace φ) ((f i).maxGenEigenspace φ) := by
+      exact h j i φ
+    replace ih (φ : K) :
+        ⨆ χ : ι → K, ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊤ := by
+      apply ih _ (hy φ)
+      · intro j k μ
+        exact mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo (f j) (f k) _ _ (h j k μ)
+      · exact fun j ↦ Module.End.iSup_genEigenspace_restrict_eq_top _ (h' j)
+      · rfl
+    replace ih (φ : K) :
+        ⨆ (χ : ι → K) (_ : χ i = φ), ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊤ := by
+      suffices ∀ χ : ι → K, χ i ≠ φ → ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊥ by
+        specialize ih φ; rw [iSup_split, biSup_congr this] at ih; simpa using ih
+      intro χ hχ
+      rw [eq_bot_iff, ← ((f i).maxGenEigenspace φ).ker_subtype, LinearMap.ker,
+        ← Submodule.map_le_iff_le_comap, ← Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo,
+        ← disjoint_iff_inf_le]
+      exact ((f i).disjoint_iSup_genEigenspace hχ.symm).mono_right (iInf_le _ i)
+    replace ih (φ : K) :
+        ⨆ (χ : ι → K) (_ : χ i = φ), ⨅ j, maxGenEigenspace (f j) (χ j) =
+        maxGenEigenspace (f i) φ := by
+      have (χ : ι → K) (hχ : χ i = φ) : ⨅ j, maxGenEigenspace (f j) (χ j) =
+          (⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j)).map
+            ((f i).maxGenEigenspace φ).subtype := by
+        rw [← hχ, iInf_maxGenEigenspace_restrict_map_subtype_eq]
+      simp_rw [biSup_congr this, ← Submodule.map_iSup, ih, Submodule.map_top,
+        Submodule.range_subtype]
+    simpa only [← ih, iSup_comm (ι := K), iSup_iSup_eq_right] using h' i

Mathlib/RingTheory/LaurentSeries.lean

@@ -771,7 +771,7 @@ theorem Cauchy.eventually_mem_nhds {ℱ : Filter (LaurentSeries K)} (hℱ : Cauc
     rw [← WithZero.coe_unzero γ.ne_zero, WithZero.coe_lt_coe, hD₀, neg_neg, ofAdd_sub,
       ofAdd_toAdd, div_lt_comm, div_self', ← ofAdd_zero, Multiplicative.ofAdd_lt]
     exact zero_lt_one
-  apply coeff_eventually_equal hℱ |>.mono
+  apply coeff_eventually_equal (D := D) hℱ |>.mono
   intro _ hf
   apply lt_of_le_of_lt (valuation_le_iff_coeff_lt_eq_zero K |>.mpr _) hD
   intro n hn

Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

@@ -106,7 +106,8 @@ def ker : TwoSidedIdeal R :=
     (by rintro _ _ (h : f _ = 0); simp [h])
 
 lemma mem_ker {x : R} : x ∈ ker f ↔ f x = 0 := by
-  delta ker; rw [mem_mk']; rfl
+  delta ker; rw [mem_mk']
+  · rfl
   · rintro _ _ (h1 : f _ = 0) (h2 : f _ = 0); simp [h1, h2]
   · rintro _ (h : f _ = 0); simp [h]
   · rintro _ _ (h : f _ = 0); simp [h]