-- Mathlib/LinearAlgebra/Eigenspace/Pi.lean
/-- 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 iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo [FiniteDimensional K M]
    (f : ι → End K M)
    (h : ∀ i j φ, MapsTo (f i) ((f j).maxGenEigenspace φ) ((f j).maxGenEigenspace φ))
    (h' : ∀ i, ⨆ μ, (f i).maxGenEigenspace μ = ⊤) :
    ⨆ χ : ι → K, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤

Proof state:
case ind.inr.intro
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [inst_2 : FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
⊢ ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤

Tactic:
have hi (j : ι) (φ : K) :
    MapsTo (f j) ((f i).maxGenEigenspace φ) ((f i).maxGenEigenspace φ) := by
  exact h j i φ

Result:
case ind.inr.intro
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [inst_2 : FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
⊢ ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤

Proof state:
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
⊢ ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ

Tactic:
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]

Result:
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
this :
  ∀ (χ : ι → K),
    χ i = φ →
      ⨅ j, (f j).maxGenEigenspace (χ j) =
        Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
⊢ ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ

Proof state:
case ind.inl
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [inst_2 : FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
χ : ι → K
hχ : ∀ (a : ι), (f a).maxGenEigenspace (χ a) = ⊤
⊢ ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤

Tactic:
replace hχ : ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤ := by simpa

Result:
case ind.inl
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [inst_2 : FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
χ : ι → K
hχ : ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
⊢ ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤

Proof state:
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [inst_2 : FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
χ : ι → K
hχ : ∀ (a : ι), (f a).maxGenEigenspace (χ a) = ⊤
⊢ ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
this :
  ∀ (χ : ι → K),
    χ i = φ →
      ⨅ j, (f j).maxGenEigenspace (χ j) =
        Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
⊢ ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ

Tactic:
simp_rw [biSup_congr this, ← Submodule.map_iSup, ih, Submodule.map_top,
  Submodule.range_subtype]

Result:
no goals