awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (hypothesis)
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)
⊢ ∃ (k : ℕ),
    Membership.mem (α := M) (γ := Submodule R M)
      ((⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) ⊓ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
      ((HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M) ^ k :
            (a : M) → M)
          (y + z) :
        M)
have 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)
Tactic: 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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)
⊢ ∃ (k : ℕ),
    Membership.mem (α := M) (γ := Submodule R M)
      ((⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) ⊓ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
      ((HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M) ^ k :
            (a : M) → M)
          (y + z) :
        M)
have insert : Membership.mem (α := M) (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) : Set M)
  ((HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M) ^ k : (a : M) → M)
      (y + z) :
    M)
Tactic: refine ⟨k, Submodule.mem_inf.mp ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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.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)
insert :
  Membership.mem (α := M) (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) : Set M)
    ((HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M) ^ k : (a : M) → M)
        (y + z) :
      M)
⊢ ∃ (k : ℕ),
    Membership.mem (α := M) (γ := Submodule R M)
      ((⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) ⊓ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
      ((HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M) ^ k :
            (a : M) → M)
          (y + z) :
        M)
have insert₁ : Membership.mem (α := M) (↑(s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
  ((HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M) ^ k : (a : M) → M)
      (y + z) :
    M)
Tactic: refine ⟨k, Submodule.mem_inf.mp ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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)
⊢ Membership.mem (α := M) (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) : Set M)
    ((HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M) ^ k : (a : M) → M)
        (y + z) :
      M)
have insert : MapsTo (⇑(f l) : (a : M) → M) (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) : Set M)
  (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) : Set M)
Tactic: refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ?_ hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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)
⊢ MapsTo (⇑(f l) : (a : M) → M) (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) : Set M)
    (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) : Set M)
have insert : MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⋂ (i : ι), (↑((f i).maxGenEigenspace (χ₁ i)) : Set M))
  (⋂ (i : ι), (↑((f i).maxGenEigenspace (χ₁ i)) : Set M))
Tactic: simp only [Submodule.coe_iInf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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)
⊢ Membership.mem (α := M) (↑(s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
    ((HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M) ^ k : (a : M) → M)
        (y + z) :
      M)
have insert : Membership.mem (α := M) (↑(s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
  ((HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M) ^ k : (a : M) → M)
      z :
    M)
Tactic: rw [map_add, hk, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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)
⊢ Membership.mem (α := M) (↑(s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
    ((HSub.hSub (β := End R M) (f l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M) ^ k : (a : M) → M)
        z :
      M)
have insert : Submodule.map (g ^ k) (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ≤
  s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)
Tactic: 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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)
⊢ Submodule.map (g ^ k) (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ≤
    s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)
have insert : LE.le.{u_4} (α := Submodule R M) (⨆ i ∈ s, Submodule.map (g ^ k) (⨅ (i_2 : ι), (f i_2).maxGenEigenspace (i i_2)))
  (⨆ a ∈ s, ⨅ (i : ι), (f i).maxGenEigenspace (a i))
Tactic: simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := ι → R), Submodule.map_iSup (ι := _ ∈ s)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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)
⊢ LE.le.{u_4} (α := Submodule R M) (⨆ i ∈ s, Submodule.map (g ^ k) (⨅ (i_2 : ι), (f i_2).maxGenEigenspace (i i_2)))
    (⨆ a ∈ s, ⨅ (i : ι), (f i).maxGenEigenspace (a i))
have insert : ∀ χ ∈ s, Submodule.map (g ^ k) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ≤ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)
Tactic: refine iSup₂_mono fun χ _ ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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)
⊢ Membership.mem (α := M) (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ((g ^ k : (a : M) → M) u : M)
have insert : MapsTo (⇑(f l) : (a : M) → M) (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
  (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
Tactic: refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ i)) ?_ hu
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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 (⇑(f l) : (a : M) → M) (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
    (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
have insert : MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⋂ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
  (⋂ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
Tactic: simp only [Submodule.coe_iInf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
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)
⊢ χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
have empty : χ₁ ∉ ∅ →
  Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (Finset.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 χ
Cleared hypotheses: s