awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this_1 : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
this : ⨅ (j : ι), (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (⨅ (i_1 : ι), Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) (μ i_1)))
    (⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i))
have conv_rhs : Eq.{u_4 + 1} (α := Submodule R M)
  (⨅ (i_1 : ι), Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) sorry) (μ i_1)))
  (⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i))
Tactic: conv_rhs =>
    enter [1]
    ext
    rw [p.inf_genEigenspace (f _) (h _)]
-- 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
μ : ι → R
i : ι
h_1 :
  ∀ (j : ι),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace (μ i)) : Set M) (↑((f i).maxGenEigenspace (μ i)) : Set M)
this_1 : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo (⇑(f j) : (a : M) → M) (↑p : Set M) (↑p : Set M)
this : ⨅ (j : ι), (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ (j : ι), (f j).maxGenEigenspace (μ j)
conv_rhs :
  Eq.{u_4 + 1} (α := Submodule R M)
    (⨅ (i_1 : ι), Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) (μ i_1)))
    (⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i))
⊢ Eq.{u_4 + 1} (α := Submodule R M)
    (⨅ (i_1 : ι), Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) ⋯) (μ i_1)))
    (⨅ (i : ι), p ⊓ (f i).maxGenEigenspace (μ i))
have conv_rhs₁ : Eq.{u_4 + 1} (α := Submodule R M)
  (⨅ (i_1 : ι), Submodule.map p.subtype (maxGenEigenspace (LinearMap.restrict (f i_1) sorry) (μ i_1)))
  (⨅ (x : ι),
    Submodule.map p.subtype ((genEigenspace (LinearMap.restrict (f x) sorry) (μ x) : (a : ℕ∞) → Submodule R ↥p) ⊤))
Tactic: conv_rhs =>
    enter [1]
    ext
    rw [p.inf_genEigenspace (f _) (h _)]
-- 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
χ₁ χ₂ : ι → R
h : χ₁ ≠ χ₂
⊢ Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i))
have obtain : ∀ (j : ι) (hj : χ₁ j ≠ χ₂ j),
  Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i))
Tactic: obtain ⟨j, hj⟩ : ∃ j, χ₁ j ≠ χ₂ j := Function.ne_iff.mp h
-- 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
χ₁ : ι → R
h :
  Membership.mem (γ := Set (ι → R))
    {χ : ι → R | Ne.{u_4 + 1} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊥} χ₁
χ₂ : ι → R
hχ₂ :
  Membership.mem (γ := Set (ι → R))
    {χ : ι → R | Ne.{u_4 + 1} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊥} χ₂
hχ₁₂ :
  Eq.{u_4 + 1} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i))
⊢ χ₁ = χ₂
have contrapose! : ∀ (hχ₂ : χ₁ ≠ χ₂), χ₂ ∉ {χ : ι → R | Ne.{u_4 + 1} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊥}
Tactic: contrapose! hχ₂
Cleared hypotheses: hχ₂
-- 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 :
  ∀ (i j : ι) (φ : R),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
l : ι
χ : ι → R
x : M
hx : Membership.mem (γ := Set M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M)) x
⊢ Membership.mem (α := M) (γ := Set M) (⨅ (i : ι), (↑((f i).maxGenEigenspace (χ i)) : Set M))
    ((f l : (a : M) → M) x : M)
have simp : ∀ (hx : ∀ (i : ι), x ∈ (f i).maxGenEigenspace (χ i)) (i : ι),
  Membership.mem (α := M) ((f i).maxGenEigenspace (χ i)) ((f l : (a : M) → M) x : M)
Tactic: simp only [iInf_eq_iInter, mem_iInter, SetLike.mem_coe] at hx ⊢
Cleared hypotheses: hx
-- 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 :
  ∀ (i j : ι) (φ : R),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
⊢ iSupIndep (α := Submodule R M) fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)
have 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))
Tactic: replace h (l : ι) (χ : ι → R) :
      MapsTo (f l) (⨅ i, (f i).maxGenEigenspace (χ i)) (⨅ i, (f i).maxGenEigenspace (χ i)) := by
    intro x hx
    simp only [iInf_eq_iInter, mem_iInter, SetLike.mem_coe] at hx ⊢
    exact fun i ↦ h l i (χ i) (hx i)
Cleared hypotheses: h
-- 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))
⊢ iSupIndep (α := Submodule R M) fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)
have 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))
Tactic: 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 χ)
-- 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
ih :
  χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
hχ₁₂ : χ₁ ∉ insert χ₂ s
⊢ ¬χ₁ = χ₂ ∧ χ₁ ∉ s
have rwa : ∀ (hχ₁₂ : ¬(χ₁ = χ₂ ∨ χ₁ ∈ s)), ¬χ₁ = χ₂ ∧ χ₁ ∉ s
Tactic: rwa [Finset.mem_insert, not_or] at hχ₁₂
-- 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
ih :
  χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
hχ₁₂ : χ₁ ∉ insert χ₂ s
rwa : ∀ (hχ₁₂ : ¬(χ₁ = χ₂ ∨ χ₁ ∈ s)), ¬χ₁ = χ₂ ∧ χ₁ ∉ s
⊢ ¬χ₁ = χ₂ ∧ χ₁ ∉ s
have rwa₁ : ∀ (hχ₁₂ : ¬χ₁ = χ₂ ∧ χ₁ ∉ s), ¬χ₁ = χ₂ ∧ χ₁ ∉ s
Tactic: rwa [Finset.mem_insert, not_or] at hχ₁₂
-- 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
ih :
  χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
hχ₁₂ : χ₁ ∉ insert χ₂ s
⊢ Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    ((insert χ₂ s).sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
have hχ₁₃ : χ₁ ≠ χ₂
Tactic: obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂
-- 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
ih :
  χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
hχ₁₂ : χ₁ ∉ insert χ₂ s
hχ₁₃ : χ₁ ≠ χ₂
⊢ Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    ((insert χ₂ s).sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
have hχ₁ : χ₁ ∉ s
Tactic: obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂
-- 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
ih :
  χ₁ ∉ s →
    Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
      (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
hχ₁₂_1 : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
⊢ Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    ((insert χ₂ s).sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
have ih₁ : Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
  (s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
Tactic: specialize ih hχ₁
Cleared hypotheses: ih
-- 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))
⊢ Disjoint.{u_4} (α := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i))
    ((insert χ₂ s).sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i))
have insert : ∀ (x : M),
  Membership.mem (γ := Submodule R M)
      ((⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) ⊓
        ((⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) ⊔ s.sup fun (χ : ι → R) ↦ ⨅ (i : ι), (f i).maxGenEigenspace (χ i)))
      x →
    x = 0
Tactic: rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
-- 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))
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)
⊢ x = 0
have hx₁ : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) x
Tactic: simp only [SetLike.mem_coe] at hx hx'
Cleared hypotheses: hx, hx'
-- 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))
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
⊢ x = 0
have hx'₁ : 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'
Cleared hypotheses: hx, 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))
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
⊢ x = 0
have rw : Membership.mem (γ := Submodule R M)
  ((⨅ (i : ι), (f i).maxGenEigenspace (χ₁ i)) ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) x
Tactic: rw [← Submodule.mem_bot (R := R), ← (disjoint_iInf_maxGenEigenspace f hχ₁₂).eq_bot]
-- 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))
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
⊢ x = 0
have insert : Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) x
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⟩
-- 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))
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
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) x
have 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)
Tactic: obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'
Cleared hypotheses: x, hx, 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)
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ι), (f i).maxGenEigenspace (χ₂ i)) (y + z)
have 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)
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
-- 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 : ℕ),
    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 : ∀ (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)
Tactic: obtain ⟨k, hk : (g ^ k) y = 0⟩ := (mem_iInf_maxGenEigenspace_iff _ _ _).mp hy l
-- 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_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) ^ k) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
have 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)
Tactic: rw [Module.End.coe_pow]