awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
⊢ ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤

Tactic:
replace ih (φ : K) :
        ⨆ (χ : ι → K) (_ : χ i = φ), ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊤ := by
      suffices ∀ χ : ι → K, χ i ≠ φ → ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊥ by
        specialize ih φ; rw [iSup_split, biSup_congr this] at ih; simpa using ih
      intro χ hχ
      rw [eq_bot_iff, ← ((f i).maxGenEigenspace φ).ker_subtype, LinearMap.ker,
        ← Submodule.map_le_iff_le_comap, ← Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo,
        ← disjoint_iff_inf_le]
      exact ((f i).disjoint_genEigenspace hχ.symm _ _).mono_right (iInf_le _ i)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
χ : ι → K
hχ : χ i = φ
rw :
  ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
    Submodule.map ((f i).maxGenEigenspace (χ i)).subtype
      (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
rw₁ rw₂ :
  Eq.{u_4 + 1} (α := Submodule K M) (⨅ (j : ι), (f j).maxGenEigenspace (χ j)) (⨅ (j : ι), (f j).maxGenEigenspace (χ j))
⊢ ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
    Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))

Tactic:
rw [← hχ, iInf_maxGenEigenspace_restrict_map_subtype_eq]

Premises used: Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
⊢ ∀ (χ : ι → K) (hχ : χ i = φ),
    ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
      Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))

Tactic:
have (χ : ι → K) (hχ : χ i = φ) : ⨅ j, maxGenEigenspace (f j) (χ j) =
          (⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j)).map
            ((f i).maxGenEigenspace φ).subtype := by
        rw [← hχ, iInf_maxGenEigenspace_restrict_map_subtype_eq]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
φ : K
this :
  ∀ (χ : ι → K) (hχ : χ i = φ),
    ⨅ (j : ι), (f j).maxGenEigenspace (χ j) =
      Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
simp_rw :
  ⨆ (i_1 : ι → K),
      ⨆ (_ : i_1 i = φ),
        Submodule.map ((f i).maxGenEigenspace φ).subtype
          (⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (i_1 j)) =
    (f i).maxGenEigenspace φ
simp_rw₁ :
  Submodule.map ((f i).maxGenEigenspace φ).subtype
      (⨆ (i_1 : ι → K), ⨆ (_ : i_1 i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (i_1 j)) =
    (f i).maxGenEigenspace φ
simp_rw₂ : Submodule.map ((f i).maxGenEigenspace φ).subtype ⊤ = (f i).maxGenEigenspace φ
simp_rw₃ : ((f i).maxGenEigenspace φ).subtype.range = (f i).maxGenEigenspace φ
⊢ ⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ

Tactic:
simp_rw [biSup_congr this, ← Submodule.map_iSup, ih, Submodule.map_top,
        Submodule.range_subtype]

Premises used: Submodule.map_iSup, Submodule.map_top, Submodule.range_subtype, biSup_congr
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
ih :
  ∀ (φ : K),
    Eq.{u_4 + 1} (α := Submodule K ↥((f i).maxGenEigenspace φ))
      (⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j)) ⊤
⊢ ∀ (φ : K), ⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ

Tactic:
replace ih (φ : K) :
        ⨆ (χ : ι → K) (_ : χ i = φ), ⨅ j, maxGenEigenspace (f j) (χ j) =
        maxGenEigenspace (f i) φ := by
      have (χ : ι → K) (hχ : χ i = φ) : ⨅ j, maxGenEigenspace (f j) (χ j) =
          (⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j)).map
            ((f i).maxGenEigenspace φ).subtype := by
        rw [← hχ, iInf_maxGenEigenspace_restrict_map_subtype_eq]
      simp_rw [biSup_congr this, ← Submodule.map_iSup, ih, Submodule.map_top,
        Submodule.range_subtype]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
inst : Field K
n : ℕ
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h :
  ∀ (i j : ι) (φ : K),
    MapsTo (⇑(f i) : (a : M) → M) (↑((f j).maxGenEigenspace φ) : Set M) (↑((f j).maxGenEigenspace φ) : Set M)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank.{u_3, u_4} K ↥((f i).maxGenEigenspace φ) < n
hi :
  ∀ (j : ι) (φ : K),
    MapsTo (⇑(f j) : (a : M) → M) (↑((f i).maxGenEigenspace φ) : Set M) (↑((f i).maxGenEigenspace φ) : Set M)
ih : ∀ (φ : K), ⨆ (χ : ι → K), ⨆ (_ : χ i = φ), ⨅ (j : ι), (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤

Tactic:
simpa only [← ih, iSup_comm (ι := K), iSup_iSup_eq_right] using h' i

Premises used: iSup_comm, iSup_iSup_eq_right
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun (i j : ι) ↦ Commute (f i) (f j)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤

Tactic:
Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo _
    (fun i j ↦ Module.End.mapsTo_maxGenEigenspace_of_comm ?_) h'

Premises used: Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo, Module.End.mapsTo_maxGenEigenspace_of_comm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun (i j : ι) ↦ Commute (f i) (f j)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
refine : ∀ (i j : ι), Commute (f j) (f i)
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤

Tactic:
refine Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo _
    (fun i j ↦ Module.End.mapsTo_maxGenEigenspace_of_comm ?_) h'

Premises used: Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo, Module.End.mapsTo_maxGenEigenspace_of_comm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun (i j : ι) ↦ Commute (f i) (f j)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
i j : ι
inl : Commute (f j) (f j)
inr : ∀ (hij : j ≠ i), Commute (f j) (f i)
⊢ Commute (f j) (f i)

Tactic:
rcases eq_or_ne j i with rfl | hij

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun (i j : ι) ↦ Commute (f i) (f j)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
j : ι
⊢ Commute (f j) (f j)

Tactic:
tauto
-- Module: Mathlib.LinearAlgebra.Eigenspace.Pi
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun (i j : ι) ↦ Commute (f i) (f j)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
i j : ι
hij : j ≠ i
⊢ Commute (f j) (f i)

Tactic:
tauto
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) m
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ m ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker

Tactic:
rw [f.mem_genEigenspace] at hm

Premises used: Module.End.mem_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) m
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
hm₁ : ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ m ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ Commute f g

Tactic:
rw [f.mem_genEigenspace] at hm

Premises used: Module.End.mem_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) m
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
hm₁ : ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ m ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
hfg₁ : Commute f g
⊢ g.IsFinitelySemisimple

Tactic:
rw [f.mem_genEigenspace] at hm

Premises used: Module.End.mem_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) m
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
hm₁ : ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ m ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
hfg₁ : Commute f g
hss₁ : g.IsFinitelySemisimple
⊢ IsNilpotent (f - g)

Tactic:
rw [f.mem_genEigenspace] at hm

Premises used: Module.End.mem_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ m ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
obtain : ∀ (l : ℕ) (hm : m ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker), (g : (a : M) → M) m = μ • m
⊢ (g : (a : M) → M) m = μ • m

Tactic:
obtain ⟨l, -, hm⟩ := hm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
hm : m ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) m

Tactic:
rw [← f.mem_genEigenspace_nat] at hm

Premises used: Module.End.mem_genEigenspace_nat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
hm : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) m
⊢ let p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞);
  m ∈ p

Tactic:
set p := f.genEigenspace μ l

Premises used: Nat.cast, Module.End.genEigenspace, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hm : m ∈ p
⊢ MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)

Tactic:
have h₁ : MapsTo g p p := mapsTo_genEigenspace_of_comm hfg μ l
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hm : m ∈ p
h₁ : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
⊢ MapsTo (⇑(HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)

Tactic:
have h₂ : MapsTo (g - algebraMap R (End R M) μ) p p :=
    mapsTo_genEigenspace_of_comm (hfg.sub_right <| Algebra.commute_algebraMap_right μ f) μ l
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hm : m ∈ p
h₁ : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₂ :
  MapsTo (⇑(HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
⊢ MapsTo (⇑(f - g) : (a : M) → M) (↑p : Set M) (↑p : Set M)

Tactic:
have h₃ : MapsTo (f - g) p p :=
    mapsTo_genEigenspace_of_comm (Commute.sub_right rfl hfg) μ l
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hm : m ∈ p
h₁ : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₂ :
  MapsTo (⇑(HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
h₃ : MapsTo (⇑(f - g) : (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)
    (↑p : Set M) (↑p : Set M)

Tactic:
have h₄ : MapsTo (f - algebraMap R (End R M) μ) p p :=
    mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ l
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hm : m ∈ p
h₁ : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₂ :
  MapsTo (⇑(HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
h₃ : MapsTo (⇑(f - g) : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₄ :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
⊢ Commute (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) (f - g)

Tactic:
replace hfg : Commute (f - algebraMap R (End R M) μ) (f - g) :=
    (Commute.sub_right rfl hfg).sub_left <| Algebra.commute_algebraMap_left μ (f - g)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hm : m ∈ p
h₁ : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₂ :
  MapsTo (⇑(HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
h₃ : MapsTo (⇑(f - g) : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₄ :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
hfg : Commute (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) (f - g)
this :
  IsNilpotent
    (LinearMap.restrict (HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) h₂)
⊢ IsFinitelySemisimple
    (HSub.hSub (β := End R ↥p) (LinearMap.restrict g h₁) ((algebraMap R (End R ↥p) : (a : R) → End R ↥p) μ : End R ↥p))

Tactic:
simpa using hss.restrict _

Premises used: Module.End.IsFinitelySemisimple.restrict
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hm : m ∈ p
h₁ : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₂ :
  MapsTo (⇑(HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
h₃ : MapsTo (⇑(f - g) : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₄ :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
hfg : Commute (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) (f - g)
this :
  IsNilpotent
    (LinearMap.restrict (HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) h₂)
⊢ HSub.hSub (β := End R ↥p) (LinearMap.restrict g h₁) ((algebraMap R (End R ↥p) : (a : R) → End R ↥p) μ : End R ↥p) = 0

Tactic:
replace this : g.restrict h₁ - algebraMap R (End R p) μ = 0 :=
      eq_zero_of_isNilpotent_of_isFinitelySemisimple this (by simpa using hss.restrict _)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hm : m ∈ p
h₁ : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₂ :
  MapsTo (⇑(HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
h₃ : MapsTo (⇑(f - g) : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₄ :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
hfg : Commute (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) (f - g)
this :
  HSub.hSub (β := End R ↥p) (LinearMap.restrict g h₁) ((algebraMap R (End R ↥p) : (a : R) → End R ↥p) μ : End R ↥p) = 0
⊢ (g : (a : M) → M) m = μ • m

Tactic:
simpa [LinearMap.restrict_apply, sub_eq_zero] using LinearMap.congr_fun this ⟨m, hm⟩

Premises used: sub_eq_zero, Subtype.mk, LinearMap.congr_fun, LinearMap.restrict_apply
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hm : m ∈ p
h₁ : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₂ :
  MapsTo (⇑(HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
h₃ : MapsTo (⇑(f - g) : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₄ :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
hfg : Commute (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) (f - g)
suffices :
  IsNilpotent
    (LinearMap.restrict (HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) h₂)
⊢ (g : (a : M) → M) m = μ • m

Tactic:
suffices IsNilpotent ((g - algebraMap R (End R M) μ).restrict h₂) by
    replace this : g.restrict h₁ - algebraMap R (End R p) μ = 0 :=
      eq_zero_of_isNilpotent_of_isFinitelySemisimple this (by simpa using hss.restrict _)
    simpa [LinearMap.restrict_apply, sub_eq_zero] using LinearMap.congr_fun this ⟨m, hm⟩