awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
j : ι
φ : K
⊢ MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)

Tactic:
h j i φ
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
j : ι
φ : K
⊢ MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)

Tactic:
exact h j i φ
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
⊢ ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)

Tactic:
have hi (j : ι) (φ : K) :
        MapsTo (f j) ((f i).maxGenEigenspace φ) ((f i).maxGenEigenspace φ) := by
      exact h j i φ
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
φ : K
h₁ :
  ∀ (i_1 j : ι) (φ_1 : K),
    MapsTo (⇑(LinearMap.restrict (f i_1) ⋯) : (a : ↥((f i).maxGenEigenspace φ)) → ↥((f i).maxGenEigenspace φ))
      (↑(maxGenEigenspace (LinearMap.restrict (f j) ⋯) φ_1) : Set ↥((f i).maxGenEigenspace φ))
      (↑(maxGenEigenspace (LinearMap.restrict (f j) ⋯) φ_1) : Set ↥((f i).maxGenEigenspace φ))
h'₁ :
  ∀ (i_1 : ι),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (μ : K), maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) μ) ⊤
h_dim₁ : finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) = finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ)
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤

Tactic:
apply ih _ (hy φ)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
φ : K
j k : ι
μ : K
⊢ MapsTo (⇑(LinearMap.restrict (f j) ⋯) : (a : ↥((f i).maxGenEigenspace φ)) → ↥((f i).maxGenEigenspace φ))
    (↑(maxGenEigenspace (LinearMap.restrict (f k) ⋯) μ) : Set ↥((f i).maxGenEigenspace φ))
    (↑(maxGenEigenspace (LinearMap.restrict (f k) ⋯) μ) : Set ↥((f i).maxGenEigenspace φ))

Tactic:
mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo (f j) (f k) _ _ (h j k μ)

Premises used: Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo, Set.Mem, setOf
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
φ : K
j k : ι
μ : K
⊢ MapsTo (⇑(LinearMap.restrict (f j) ⋯) : (a : ↥((f i).maxGenEigenspace φ)) → ↥((f i).maxGenEigenspace φ))
    (↑(maxGenEigenspace (LinearMap.restrict (f k) ⋯) μ) : Set ↥((f i).maxGenEigenspace φ))
    (↑(maxGenEigenspace (LinearMap.restrict (f k) ⋯) μ) : Set ↥((f i).maxGenEigenspace φ))

Tactic:
exact mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo (f j) (f k) _ _ (h j k μ)

Premises used: Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
φ : K
⊢ ∀ (i_1 : ι),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (μ : K), maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) μ) ⊤

Tactic:
fun j ↦ Module.End.genEigenspace_restrict_eq_top _ (h' j)

Premises used: Module.End.genEigenspace_restrict_eq_top
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
φ : K
⊢ ∀ (i_1 : ι),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (μ : K), maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) μ) ⊤

Tactic:
exact fun j ↦ Module.End.genEigenspace_restrict_eq_top _ (h' j)

Premises used: Module.End.genEigenspace_restrict_eq_top
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
φ : K
⊢ finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) = finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst_4 : AddCommGroup M] [inst_5 : Module K M] [FiniteDimensional K M] (f : ι → End K M)
      (h :
        ∀ (i j : ι) (φ : K),
          MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M))
      (h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤)
      (h_dim : finrank K M = m),
      Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
⊢ ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤

Tactic:
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.genEigenspace_restrict_eq_top _ (h' j)
      · rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
this :
  ∀ (χ : ι → K),
    χ i ≠ φ →
      Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
        (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊥
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤

Tactic:
specialize ih φ
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
φ : K
this :
  ∀ (χ : ι → K),
    χ i ≠ φ →
      Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
        (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊥
ih :
  Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    ((⨆ (i_1 : ι → K), ⨆ (_ : i_1 i ≠ φ), ⊥) ⊔
      ⨆ (i_1 : ι → K), ⨆ (_ : ¬i_1 i ≠ φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (i_1 j))
    ⊤

Tactic:
rw [iSup_split, biSup_congr this] at ih

Premises used: iSup_split, biSup_congr
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
φ : K
this :
  ∀ (χ : ι → K),
    χ i ≠ φ →
      Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
        (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊥
ih_1 :
  Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
ih :
  Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    ((⨆ (i_1 : ι → K), ⨆ (_ : i_1 i ≠ φ), ⊥) ⊔
      ⨆ (i_1 : ι → K), ⨆ (_ : ¬i_1 i ≠ φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (i_1 j))
    ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤

Tactic:
simpa using ih
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
suffices :
  ∀ (χ : ι → K),
    χ i ≠ φ →
      Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
        (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊥
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤

Tactic:
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
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
χ : ι → K
hχ : χ i ≠ φ
rw : Disjoint ((f i).maxGenEigenspace φ) (⨅ (i : ι), (f i).maxGenEigenspace (χ i))
⊢ Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
    (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊥

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

Premises used: Submodule.ker_subtype, LinearMap.ker, Module.End.maxGenEigenspace, Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo, disjoint_iff_inf_le, Submodule.map_le_iff_le_comap, eq_bot_iff
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
χ : ι → K
hχ : χ i ≠ φ
⊢ Disjoint ((f i).maxGenEigenspace φ) (⨅ (i : ι), (f i).maxGenEigenspace (χ i))

Tactic:
((f i).disjoint_genEigenspace hχ.symm _ _).mono_right (iInf_le _ i)

Premises used: Ne.symm, Module.End.disjoint_genEigenspace, Disjoint.mono_right, iInf_le
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
χ : ι → K
hχ : χ i ≠ φ
⊢ Disjoint ((f i).maxGenEigenspace φ) (⨅ (i : ι), (f i).maxGenEigenspace (χ i))

Tactic:
exact ((f i).disjoint_genEigenspace hχ.symm _ _).mono_right (iInf_le _ i)

Premises used: Disjoint.mono_right, iInf_le