-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
χ₁ : ι → R
s : Finset (ι → R)
empty :
  χ₁ ∉ ∅ →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (Finset.sup ∅ fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
insert :
  ∀ (χ₂ : ι → R) (s : Finset (ι → R)) (_n : χ₂ ∉ s)
    (ih :
      χ₁ ∉ s →
        Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
          (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))),
    χ₁ ∉ Insert.insert χ₂ s →
      Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
        ((Insert.insert χ₂ s).sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
⊢ χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert χ₂ s _n ih =>
  intro hχ₁₂
  obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂
  specialize ih hχ₁
  rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
  rintro x ⟨hx, hx'⟩
  simp only [SetLike.mem_coe] at hx hx'
  suffices x ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i) by
    rw [← Submodule.mem_bot (R := R), ← (disjoint_iInf_maxGenEigenspace f hχ₁₂).eq_bot]
    exact ⟨hx, this⟩
  obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx'
  suffices ∀ l, ∃ (k : ℕ),
      ((f l - algebraMap R (Module.End R M) (χ₂ l)) ^ k) (y + z) ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓
        Finset.sup s fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i) by
    simpa [ih.eq_bot, Submodule.mem_bot] using this
  intro l
  let g : Module.End R M := f l - algebraMap R (Module.End R M) (χ₂ l)
  obtain ⟨k, hk : (g ^ k) y = 0⟩ := (mem_iInf_maxGenEigenspace_iff _ _ _).mp hy l
  have aux (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M) (hp : MapsTo f p p) :
      MapsTo ((f - algebraMap R (Module.End R M) φ) ^ k) p p := by
    rw [Module.End.coe_pow]
    exact MapsTo.iterate (fun m hm ↦ p.sub_mem (hp hm) (p.smul_mem _ hm)) k
  refine ⟨k, Submodule.mem_inf.mp ⟨?_, ?_⟩⟩
  · refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ?_ hx
    simp only [Submodule.coe_iInf]
    exact h l χ₁
  · rw [map_add, hk, zero_add]
    suffices (s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i))).map (g ^ k) ≤
        s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i)) from
      this (Submodule.mem_map_of_mem hz)
    simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := ι → R), Submodule.map_iSup (ι := _ ∈ s)]
    refine iSup₂_mono fun χ _ ↦ ?_
    rintro - ⟨u, hu, rfl⟩
    refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ i)) ?_ hu
    simp only [Submodule.coe_iInf]
    exact h l χ

Premises used: Submodule.map_iSup, Finset.sup_insert, iSup₂_mono, disjoint_iff, map_add, Insert.insert, Submodule.coe_iInf, zero_add, Finset.sup_eq_iSup, SetLike.mem_coe, Submodule.eq_bot_iff, rfl