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)
⊢ 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:
aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ?_ hx

Premises used: iInf, Module.End.maxGenEigenspace
-- 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 :
  MapsTo (⇑(f l) : (a : M) → M) (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) : Set M)
    (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) : 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)

Tactic:
refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ?_ hx

Premises used: iInf, Module.End.maxGenEigenspace
-- 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 :
  MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⋂ (i : ι), (↑((f i).maxGenEigenspace (χ₁ i)) : Set M))
    (⋂ (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)

Tactic:
simp only [Submodule.coe_iInf]

Premises used: Submodule.coe_iInf
-- 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)
⊢ 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)
⊢ 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))
χ₁ χ₂ : ι → 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) (↑(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)
⊢ 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:
rw [map_add, hk, zero_add]

Premises used: map_add, zero_add
-- 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 :
  Submodule.map (g ^ k) (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ≤
    s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)
⊢ 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:
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)
-- 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 :
  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))
⊢ Submodule.map (g ^ k) (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ≤
    s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)

Tactic:
simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := ι → R), Submodule.map_iSup (ι := _ ∈ s)]

Premises used: Submodule.map_iSup, Finset.sup_eq_iSup
-- 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)
⊢ 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:
iSup₂_mono fun χ _ ↦ ?_

Premises used: iSup₂_mono, Set.Mem, setOf
-- 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 :
  ∀ χ ∈ s, Submodule.map (g ^ k) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ≤ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)
⊢ 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:
refine iSup₂_mono fun χ _ ↦ ?_

Premises used: iSup₂_mono
-- 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)
⊢ Membership.mem (α := M) (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ((g ^ k : (a : M) → M) u : M)

Tactic:
aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ i)) ?_ hu

Premises used: iInf, Set.Mem, Module.End.maxGenEigenspace
-- 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)
χ : ι → R
h_1 : χ ∈ s
u : M
hu : u ∈ (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
insert :
  MapsTo (⇑(f l) : (a : M) → M) (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
    (↑(⨅ (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)

Tactic:
refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ i)) ?_ hu

Premises used: iInf, Module.End.maxGenEigenspace
-- 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)
χ : ι → R
h_1 : χ ∈ s
u : M
hu : u ∈ (↑(⨅ (i : ι), (f i).maxGenEigenspace (χ i)) : Set M)
insert :
  MapsTo (α := M) (β := M) (⇑(f l) : (a : M) → M) (⋂ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
    (⋂ (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)

Tactic:
simp only [Submodule.coe_iInf]

Premises used: Submodule.coe_iInf