awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
_n : χ₂ ∉ s
hχ₁₂_1 : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih :
  Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
y : M
hy : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) y
z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) z
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) (y + z)
l : ι
g : End R M := HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M)
k : ℕ
hk : Eq (α := M) ((g ^ k : (a : M) → M) y : M) (0 : M)
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M) (hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)),
    MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) φ : End R M) ^ k) : (a : M) → M)
      (↑p : Set M) (↑p : Set M)
χ : ι → R
h_1 : χ ∈ s
u : M
hu : u ∈ (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
⊢ MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⋂ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
    (⋂ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))

Tactic:
h l χ

Premises used: Set.iInter
-- 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)
_n : χ₂ ∉ s
hχ₁₂_1 : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih :
  Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
y : M
hy : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) y
z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) z
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) (y + z)
l : ι
g : End R M := HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M)
k : ℕ
hk : Eq (α := M) ((g ^ k : (a : M) → M) y : M) (0 : M)
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M) (hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)),
    MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) φ : End R M) ^ k) : (a : M) → M)
      (↑p : Set M) (↑p : Set M)
χ : ι → R
h_1 : χ ∈ s
u : M
hu : u ∈ (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
⊢ MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⋂ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
    (⋂ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))

Tactic:
exact h l χ
-- 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))
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (χ₁ : ι → R) (s : Finset (ι → R)),
    χ₁ ∉ s →
      Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
        (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
⊢ iSupIndep (α := Submodule R M) fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)

Tactic:
classical
  suffices ∀ χ (s : Finset (ι → R)) (_ : χ ∉ s),
      Disjoint (⨅ i, (f i).maxGenEigenspace (χ i))
        (s.sup fun (χ : ι → R) ↦ ⨅ i, (f i).maxGenEigenspace (χ i)) by
    simpa only [iSupIndep_iff_supIndep,
      Finset.supIndep_iff_disjoint_erase] using fun s χ _ ↦ this _ _ (s.notMem_erase χ)
  intro χ₁ s
  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
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
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 μ) ⊤
generalize :
  ∀ (n : ℕ) (h_dim : finrank K M = n),
    Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤

Tactic:
generalize h_dim : finrank K M = n

Premises used: Module.finrank
-- 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
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤

Tactic:
?_
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
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 μ) ⊤
n : ℕ
h_dim : finrank K M = n
ind :
  ∀ (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_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 = n),
    Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤

Tactic:
induction n using Nat.strongRecOn generalizing M with | ind n ih => ?_
-- 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
ind :
  ∀ (this : ∀ (a : ι), ∃ (φ : K), (f a).maxGenEigenspace φ = ⊤),
    Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
ind₁ :
  ∀ (i : ι) (hy : ¬∃ (φ : K), (f i).maxGenEigenspace φ = ⊤),
    Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤

Tactic:
obtain this | ⟨i : ι, hy : ¬ ∃ φ, (f i).maxGenEigenspace φ = ⊤⟩ :=
    forall_or_exists_not (fun j : ι ↦ ∃ φ : K, (f j).maxGenEigenspace φ = ⊤)

Premises used: Exists, Module.End.maxGenEigenspace, forall_or_exists_not, Top.top, Eq
-- 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
this : ∀ (a : ι), ∃ (φ : K), (f a).maxGenEigenspace φ = ⊤
ind :
  ∀ (χ : (a : ι) → K) (hχ : ∀ (a : ι), (f a).maxGenEigenspace (χ a) = ⊤),
    Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤

Tactic:
choose χ hχ using this
-- 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
χ : (a : ι) → K
hχ : ∀ (a : ι), (f a).maxGenEigenspace (χ a) = ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤

Tactic:
simpa
-- 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
χ : (a : ι) → K
hχ : ∀ (a : ι), (f a).maxGenEigenspace (χ a) = ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤

Tactic:
replace hχ : ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤ := by simpa
-- 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
χ : (a : ι) → K
hχ : Eq.{u_4 + 1} (α := Submodule K M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
ind :
  ∀ (hχ : LE.le.{u_4} (α := Submodule K M) ⊤ (⨅ (i : ι), (f i).maxGenEigenspace (χ i))),
    LE.le.{u_4} (α := Submodule K M) ⊤ (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤

Tactic:
simp_rw [eq_top_iff] at hχ ⊢

Premises used: eq_top_iff
-- 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
χ : (a : ι) → K
hχ : LE.le.{u_4} (α := Submodule K M) ⊤ (⨅ (i : ι), (f i).maxGenEigenspace (χ i))
⊢ LE.le.{u_4} (α := Submodule K M) ⊤ (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i))

Tactic:
le_trans hχ <| le_iSup (fun χ : ι → K ↦ ⨅ i, (f i).maxGenEigenspace (χ i)) χ

Premises used: iInf, le_iSup, Module.End.maxGenEigenspace, le_trans
-- 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
χ : (a : ι) → K
hχ : LE.le.{u_4} (α := Submodule K M) ⊤ (⨅ (i : ι), (f i).maxGenEigenspace (χ i))
⊢ LE.le.{u_4} (α := Submodule K M) ⊤ (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i))

Tactic:
exact le_trans hχ <| le_iSup (fun χ : ι → K ↦ ⨅ i, (f i).maxGenEigenspace (χ i)) χ

Premises used: iInf, le_iSup, Module.End.maxGenEigenspace, le_trans
-- 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), (f i).maxGenEigenspace φ = ⊤
φ : K
⊢ ∀ (x : K), (f i).maxGenEigenspace x < ⊤

Tactic:
simp_rw [not_exists, ← lt_top_iff_ne_top] at hy

Premises used: not_exists, lt_top_iff_ne_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 : ι
φ : K
hy : ∀ (x : K), (f i).maxGenEigenspace x < ⊤
⊢ finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n

Tactic:
h_dim ▸ Submodule.finrank_lt (hy φ).ne

Premises used: Eq.rec, Submodule.finrank_lt, LT.lt.ne
-- 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 : ι
φ : K
hy : ∀ (x : K), (f i).maxGenEigenspace x < ⊤
⊢ finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n

Tactic:
exact h_dim ▸ Submodule.finrank_lt (hy φ).ne
-- 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), (f i).maxGenEigenspace φ = ⊤
⊢ ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n

Tactic:
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 φ).ne