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))
x : M
hx : x ∈ (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) : Set M)
hx' :
  x ∈
    (↑((⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) :
      Set M)
hx₁ : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) x
⊢ Membership.mem (γ := Submodule R M)
    ((⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) x

Tactic:
simp only [SetLike.mem_coe] at hx hx'

Premises used: SetLike.mem_coe
-- 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))
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) x
hx' :
  Membership.mem (γ := Submodule R M)
    ((⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) x
this : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) x
rw :
  Membership.mem (γ := Submodule R M)
    ((⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) x
⊢ x = 0

Tactic:
rw [← Submodule.mem_bot (R := R), ← (disjoint_iInf_maxGenEigenspace f hχ₁₂).eq_bot]

Premises used: Submodule.mem_bot, Module.End.disjoint_iInf_maxGenEigenspace, Disjoint.eq_bot
-- 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))
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) x
hx' :
  Membership.mem (γ := Submodule R M)
    ((⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) x
this : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) x
⊢ Membership.mem (γ := Submodule R M)
    ((⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) x

Tactic:
⟨hx, this⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- 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))
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) x
hx' :
  Membership.mem (γ := Submodule R M)
    ((⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) x
this : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) x
⊢ Membership.mem (γ := Submodule R M)
    ((⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) x

Tactic:
exact ⟨hx, this⟩
-- 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.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))
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) x
hx' :
  Membership.mem (γ := Submodule R M)
    ((⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) x
insert : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) x
⊢ x = 0

Tactic:
suffices x ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i) by
    rw [← Submodule.mem_bot (R := R), ← (disjoint_iInf_maxGenEigenspace f hχ₁₂).eq_bot]
    exact ⟨hx, this⟩
-- 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.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))
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) x
hx' :
  Membership.mem (γ := Submodule R M)
    ((⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) x
insert :
  ∀ (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))
    (hx' :
      Membership.mem (γ := Submodule R M)
        ((⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
        (y + z)),
    Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) (y + z)
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) x

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'

Premises used: Iff.mp, Submodule.mem_sup, rfl
-- 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)
this :
  ∀ (l : ι),
    ∃ (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)
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) (y + z)

Tactic:
simpa [ih.eq_bot, Submodule.mem_bot] using this

Premises used: Submodule.mem_bot, Disjoint.eq_bot
-- 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.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)
insert :
  ∀ (l : ι),
    ∃ (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)
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) (y + z)

Tactic:
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
-- 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.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)
insert :
  ∀ (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)
⊢ ∃ (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)

Tactic:
obtain ⟨k, hk : (g ^ k) y = 0⟩ := (mem_iInf_maxGenEigenspace_iff _ _ _).mp hy l

Premises used: Module.End.mem_iInf_maxGenEigenspace_iff, Iff.mp
-- 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_1 : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f_1 l) : (a : M) → M) (⨅ (i : ι), (↑((f_1 i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f_1 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_1 i).maxGenEigenspace (χ₁ i))
    (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f_1 i).maxGenEigenspace (χ i))
y : M
hy : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f_1 i).maxGenEigenspace (χ₂ i)) y
z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f_1 i).maxGenEigenspace (χ i)) z
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f_1 i).maxGenEigenspace (χ₁ i)) (y + z)
l : ι
g : End R M := HSub.hSub (β := End R M) (f_1 l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M)
k_1 : ℕ
hk : Eq (α := M) ((g ^ k_1 : (a : M) → M) y : M) (0 : M)
f : End R M
φ : R
k : ℕ
p : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
rw :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) φ : End R M)) : (a : M) → M)^[k]
    (↑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:
rw [Module.End.coe_pow]

Premises used: Module.End.coe_pow
-- 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_1 : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f_1 l) : (a : M) → M) (⨅ (i : ι), (↑((f_1 i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f_1 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_1 i).maxGenEigenspace (χ₁ i))
    (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f_1 i).maxGenEigenspace (χ i))
y : M
hy : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f_1 i).maxGenEigenspace (χ₂ i)) y
z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f_1 i).maxGenEigenspace (χ i)) z
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f_1 i).maxGenEigenspace (χ₁ i)) (y + z)
l : ι
g : End R M := HSub.hSub (β := End R M) (f_1 l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M)
k_1 : ℕ
hk : Eq (α := M) ((g ^ k_1 : (a : M) → M) y : M) (0 : M)
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)) : (a : M) → M)^[k]
    (↑p : Set M) (↑p : Set M)

Tactic:
MapsTo.iterate (fun m hm ↦ p.sub_mem (hp hm) (p.smul_mem _ hm)) k

Premises used: Set.MapsTo.iterate, Submodule.sub_mem, Submodule.smul_mem
-- 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_1 : ι → End R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (α := M) (β := M) (⇑(f_1 l) : (a : M) → M) (⨅ (i : ι), (↑((f_1 i).maxGenEigenspace (χ i)) : Set M))
      (⨅ (i : ι), (↑((f_1 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_1 i).maxGenEigenspace (χ₁ i))
    (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f_1 i).maxGenEigenspace (χ i))
y : M
hy : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f_1 i).maxGenEigenspace (χ₂ i)) y
z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f_1 i).maxGenEigenspace (χ i)) z
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f_1 i).maxGenEigenspace (χ₁ i)) (y + z)
l : ι
g : End R M := HSub.hSub (β := End R M) (f_1 l) ((algebraMap R (End R M) : (a : R) → End R M) (χ₂ l) : End R M)
k_1 : ℕ
hk : Eq (α := M) ((g ^ k_1 : (a : M) → M) y : M) (0 : M)
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)) : (a : M) → M)^[k]
    (↑p : Set M) (↑p : Set M)

Tactic:
exact MapsTo.iterate (fun m hm ↦ p.sub_mem (hp hm) (p.smul_mem _ hm)) k

Premises used: Set.MapsTo.iterate, Submodule.sub_mem, Submodule.smul_mem
-- 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)
⊢ ∀ (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
-- 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)
⊢ ∃ (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)

Tactic:
⟨k, Submodule.mem_inf.mp ⟨?_, ?_⟩⟩

Premises used: Submodule.mem_inf, And.intro, Exists.intro, Iff.mp
-- 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.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)
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)
⊢ ∃ (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)

Tactic:
refine ⟨k, Submodule.mem_inf.mp ⟨?_, ?_⟩⟩