awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
simp :
  {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1} ⊆
    (↑(Submodule.comap f (Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1})) : Set M)
⊢ p ∈ f.invtSubmodule

Tactic:
simp only [mem_invtSubmodule, p, Submodule.span_le]

Premises used: Module.End.mem_invtSubmodule, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
i : ℕ
hi : i ≤ k
a :
  Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
    ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)
⊢ Membership.mem (α := M)
    (↑(Submodule.comap f (Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1})) : Set M)
    ((f ^ i : (a : M) → M) x : M)

Tactic:
apply Submodule.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
i : ℕ
hi : i ≤ k
a :
  ∀ (hik : i < k),
    Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
      ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)
a₁ :
  ∀ (hk : f ^ i = 0) (hi : i ≤ i),
    Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i_1 : ℕ) (_ : i_1 ≤ i), (f ^ i_1 : (a : M) → M) x = x_1}
      ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)
⊢ Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
    ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)

Tactic:
rcases lt_or_eq_of_le hi with hik | rfl

Premises used: lt_or_eq_of_le, rfl
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
i : ℕ
hi : i ≤ k
hik : i < k
⊢ Eq (α := M) ((f ^ (i + 1) : (a : M) → M) x : M) ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)

Tactic:
simpa [Module.End.pow_apply] using iterate_succ_apply' f i x

Premises used: Function.iterate_succ_apply', Module.End.pow_apply, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
i : ℕ
hi : i ≤ k
hik : i < k
⊢ Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
    ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)

Tactic:
exact ⟨i + 1, hik, by simpa [Module.End.pow_apply] using iterate_succ_apply' f i x⟩
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
i : ℕ
hk : f ^ i = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i_1 : ℕ) (_ : i_1 ≤ i), (f ^ i_1 : (a : M) → M) x = x_1}
hi : i ≤ i
⊢ ∃ (_ : i ≤ i), Eq (α := M) ((f ^ i : (a : M) → M) x : M) ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)

Tactic:
simp [hk]
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
i : ℕ
hk : f ^ i = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i_1 : ℕ) (_ : i_1 ≤ i), (f ^ i_1 : (a : M) → M) x = x_1}
hi : i ≤ i
⊢ Membership.mem (α := M) (γ := Set M) {x_1 : M | ∃ (i_1 : ℕ) (_ : i_1 ≤ i), (f ^ i_1 : (a : M) → M) x = x_1}
    ((f : (a : M) → M) ((f ^ i : (a : M) → M) x : M) : M)

Tactic:
exact ⟨i, by simp [hk]⟩
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
⊢ p ∈ f.invtSubmodule

Tactic:
have hp₁ : p ∈ f.invtSubmodule := by
    simp only [mem_invtSubmodule, p, Submodule.span_le]
    rintro - ⟨i, hi, rfl⟩
    apply Submodule.subset_span
    rcases lt_or_eq_of_le hi with hik | rfl
    · exact ⟨i + 1, hik, by simpa [Module.End.pow_apply] using iterate_succ_apply' f i x⟩
    · exact ⟨i, by simp [hk]⟩
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun (i : ℕ) ↦ (f ^ i : (a : M) → M) x
h :
  ∀ (x_1 : M),
    Membership.mem (γ := Set M) {x_2 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_2} x_1 ↔ x_1 ∈ g '' Iic k
⊢ {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1} = g '' Iic k

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_2 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_2}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun (i : ℕ) ↦ (f ^ i : (a : M) → M) x
x_1 : M
⊢ Membership.mem (γ := Set M) {x_2 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_2} x_1 ↔ x_1 ∈ g '' Iic k

Tactic:
simp [g]
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun (i : ℕ) ↦ (f ^ i : (a : M) → M) x
⊢ {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1} = g '' Iic k

Tactic:
have hg : {(f ^ i) x | (i : ℕ) (_ : i ≤ k)} = g '' Iic k := by ext; simp [g]
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun (i : ℕ) ↦ (f ^ i : (a : M) → M) x
hg : {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1} = g '' Iic k
⊢ Module.Finite.{u_1, u_2} R ↥p

Tactic:
Module.Finite.span_of_finite _ <| hg ▸ toFinite (g '' Iic k)

Premises used: Set.Mem, Eq.rec, Set.toFinite, Set.image, Set.Iic, Module.Finite.span_of_finite, Eq.symm
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun (i : ℕ) ↦ (f ^ i : (a : M) → M) x
hg : {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1} = g '' Iic k
⊢ Module.Finite.{u_1, u_2} R ↥p

Tactic:
exact Module.Finite.span_of_finite _ <| hg ▸ toFinite (g '' Iic k)

Premises used: Module.Finite.span_of_finite
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
hp₁ : p ∈ f.invtSubmodule
⊢ Module.Finite.{u_1, u_2} R ↥p

Tactic:
have hp₂ : Module.Finite R p := by
    let g : ℕ → M := fun i ↦ (f ^ i) x
    have hg : {(f ^ i) x | (i : ℕ) (_ : i ≤ k)} = g '' Iic k := by ext; simp [g]
    exact Module.Finite.span_of_finite _ <| hg ▸ toFinite (g '' Iic k)
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this :
  ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 : M | ∃ (i : ℕ) (_ : i ≤ k), (f ^ i : (a : M) → M) x = x_1}
hp₁ : p ∈ f.invtSubmodule
hp₂ : Module.Finite.{u_1, u_2} R ↥p
⊢ Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)

Tactic:
simpa [LinearMap.restrict_apply, Subtype.ext_iff] using
    LinearMap.congr_fun (this p hp₁ hp₂) ⟨x, Submodule.subset_span ⟨0, k.zero_le, rfl⟩⟩

Premises used: Nat.zero_le, Subtype.ext_iff, Subtype.mk, LinearMap.congr_fun, Exists.intro, Submodule.subset_span, OfNat.ofNat, rfl, LinearMap.restrict_apply
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
this :
  ∀ (p : Submodule R M),
    p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p ↔
      p ≤ Submodule.comap f p
⊢ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).IsSemisimple ↔ f.IsSemisimple

Tactic:
simp [mem_invtSubmodule, isSemisimple_iff, this]

Premises used: Module.End.mem_invtSubmodule, Module.End.isSemisimple_iff
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
suffices :
  ∀ (p : Submodule R M),
    p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p ↔
      p ≤ Submodule.comap f p
⊢ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).IsSemisimple ↔ f.IsSemisimple

Tactic:
suffices ∀ p : Submodule R M, p ≤ p.comap (f - algebraMap R (Module.End R M) μ) ↔ p ≤ p.comap f by
    simp [mem_invtSubmodule, isSemisimple_iff, this]
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
⊢ ∀ (p : Submodule R M),
    p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p ↔
      p ≤ Submodule.comap f p

Tactic:
fun p ↦ ⟨fun h x hx ↦ ?_, fun h x hx ↦ p.sub_mem (h hx) (p.smul_mem μ hx)⟩

Premises used: Iff.intro, Submodule.sub_mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
refine :
  ∀ (p : Submodule R M)
    (h : p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p)
    (x : M) (hx : x ∈ p), x ∈ Submodule.comap f p
⊢ ∀ (p : Submodule R M),
    p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p ↔
      p ≤ Submodule.comap f p

Tactic:
refine fun p ↦ ⟨fun h x hx ↦ ?_, fun h x hx ↦ p.sub_mem (h hx) (p.smul_mem μ hx)⟩
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
p : Submodule R M
h : p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p
x : M
hx : x ∈ p
⊢ x ∈ Submodule.comap f p

Tactic:
simpa using p.add_mem (h hx) (p.smul_mem μ hx)

Premises used: Submodule.smul_mem, Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsSemisimple
⊢ IsSemisimpleModule.{u_1, u_2} R[X] (AEval' f)

Tactic:
rw [IsSemisimple] at hf ⊢

Premises used: Module.End.IsSemisimple
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : IsSemisimpleModule.{u_1, u_2} R[X] (AEval' f)
e : Submodule.{u_1, u_2} R[X] (AEval' (LinearMap.restrict f hp)) ≃o
  (↑(Iic
          ((AEval.mapSubmodule R M f :
              (a : ↥((Algebra.lsmul R R M : (a : End R M) → End R M) f).invtSubmodule) → Submodule R[X] (AEval R M f))
            (Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := Sublattice (Submodule R M))
                (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) x)
              p hp)) :
        Set (Submodule.{u_1, u_2} R[X] (AEval R M f))) :
    Type u_2) :=
  OrderIso.trans (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp))
    (Submodule.mapIic
      ((AEval.mapSubmodule R M f :
          (a : ↥((Algebra.lsmul R R M : (a : End R M) → End R M) f).invtSubmodule) → Submodule R[X] (AEval R M f))
        (Subtype.mk (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Sublattice (Submodule R M))
            (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) x)
          p hp)))
⊢ IsSemisimpleModule.{u_1, u_2} R[X] (AEval' (LinearMap.restrict f hp))

Tactic:
(isSemisimpleModule_iff ..).mpr (e.complementedLattice_iff.mpr inferInstance)

Premises used: OrderIso.complementedLattice_iff, Iff.mpr, inferInstance, isSemisimpleModule_iff
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : IsSemisimpleModule.{u_1, u_2} R[X] (AEval' f)
e : Submodule.{u_1, u_2} R[X] (AEval' (LinearMap.restrict f hp)) ≃o
  (↑(Iic
          ((AEval.mapSubmodule R M f :
              (a : ↥((Algebra.lsmul R R M : (a : End R M) → End R M) f).invtSubmodule) → Submodule R[X] (AEval R M f))
            (Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := Sublattice (Submodule R M))
                (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) x)
              p hp)) :
        Set (Submodule.{u_1, u_2} R[X] (AEval R M f))) :
    Type u_2) :=
  OrderIso.trans (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp))
    (Submodule.mapIic
      ((AEval.mapSubmodule R M f :
          (a : ↥((Algebra.lsmul R R M : (a : End R M) → End R M) f).invtSubmodule) → Submodule R[X] (AEval R M f))
        (Subtype.mk (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Sublattice (Submodule R M))
            (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) x)
          p hp)))
⊢ IsSemisimpleModule.{u_1, u_2} R[X] (AEval' (LinearMap.restrict f hp))

Tactic:
exact (isSemisimpleModule_iff ..).mpr (e.complementedLattice_iff.mpr inferInstance)

Premises used: OrderIso.complementedLattice_iff, Iff.mpr, inferInstance, isSemisimpleModule_iff
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hf : f.IsSemisimple
⊢ f.IsFinitelySemisimple

Tactic:
isFinitelySemisimple_iff'.mp fun _ _ _ ↦ hf.restrict _

Premises used: Module.End.IsSemisimple.restrict, Module.End.isFinitelySemisimple_iff', Iff.mp, Module.End.IsFinitelySemisimple
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : Module.Finite R M
⊢ f.IsFinitelySemisimple ↔ f.IsSemisimple

Tactic:
⟨fun hf ↦ isSemisimple_iff.mpr fun p hp ↦ ?_, IsSemisimple.isFinitelySemisimple⟩

Premises used: Iff.mpr, Iff.intro, Module.End.IsSemisimple.isFinitelySemisimple, Module.End.isSemisimple_iff
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : Module.Finite R M
refine :
  ∀ (hf : f.IsFinitelySemisimple) (p : Submodule R M) (hp : p ∈ f.invtSubmodule), ∃ q ∈ f.invtSubmodule, IsCompl p q
⊢ f.IsFinitelySemisimple ↔ f.IsSemisimple

Tactic:
refine ⟨fun hf ↦ isSemisimple_iff.mpr fun p hp ↦ ?_, IsSemisimple.isFinitelySemisimple⟩
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : Module.Finite R M
hf : f.IsFinitelySemisimple
p : Submodule R M
hp : p ∈ f.invtSubmodule
obtain :
  ∀ (q : Submodule R M) (hq₁ : q ∈ f.invtSubmodule) (hq₂ : Disjoint p q) (hq₃ : p ⊔ q = ⊤),
    ∃ q ∈ f.invtSubmodule, IsCompl p q
⊢ ∃ q ∈ f.invtSubmodule, IsCompl p q

Tactic:
obtain ⟨q, -, hq₁, hq₂, hq₃⟩ :=
    isFinitelySemisimple_iff.mp hf ⊤ (invtSubmodule.top_mem f) inferInstance p hp le_top

Premises used: inferInstance, Module.End.isFinitelySemisimple_iff, le_top, Module.End.invtSubmodule.top_mem, Iff.mp, Top.top
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : Module.Finite R M
hf : f.IsFinitelySemisimple
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq₁ : q ∈ f.invtSubmodule
hq₂ : Disjoint p q
hq₃ : p ⊔ q = ⊤
⊢ ∃ q ∈ f.invtSubmodule, IsCompl p q

Tactic:
⟨q, hq₁, hq₂, codisjoint_iff.mpr hq₃⟩

Premises used: Iff.mpr, codisjoint_iff, And.intro, Exists.intro, IsCompl.mk
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
inst_3 : Module.Finite R M
hf : f.IsFinitelySemisimple
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq₁ : q ∈ f.invtSubmodule
hq₂ : Disjoint p q
hq₃ : p ⊔ q = ⊤
⊢ ∃ q ∈ f.invtSubmodule, IsCompl p q

Tactic:
exact ⟨q, hq₁, hq₂, codisjoint_iff.mpr hq₃⟩
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
this :
  ∀ (p : Submodule R M),
    p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p ↔
      p ≤ Submodule.comap f p
simp_rw :
  (∀ p ∈ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).invtSubmodule,
      Module.Finite.{u_1, u_2} R ↥p →
        ∀ q ∈ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).invtSubmodule,
          q ≤ p →
            ∃ r ≤ p,
              r ∈
                  (HSub.hSub (β := End R M) f
                      ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).invtSubmodule ∧
                Disjoint q r ∧ q ⊔ r = p) ↔
    ∀ p ∈ f.invtSubmodule,
      Module.Finite.{u_1, u_2} R ↥p →
        ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p
simp_rw₁ :
  (∀ p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p,
      Module.Finite.{u_1, u_2} R ↥p →
        ∀ q ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) q,
          q ≤ p →
            ∃ r ≤ p,
              r ≤
                  Submodule.comap
                    (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) r ∧
                Disjoint q r ∧ q ⊔ r = p) ↔
    ∀ p ≤ Submodule.comap f p,
      Module.Finite.{u_1, u_2} R ↥p →
        ∀ q ≤ Submodule.comap f q, q ≤ p → ∃ r ≤ p, r ≤ Submodule.comap f r ∧ Disjoint q r ∧ q ⊔ r = p
⊢ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).IsFinitelySemisimple ↔
    f.IsFinitelySemisimple

Tactic:
simp_rw [isFinitelySemisimple_iff, mem_invtSubmodule, this]

Premises used: Module.End.mem_invtSubmodule, Module.End.isFinitelySemisimple_iff
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
suffices :
  ∀ (p : Submodule R M),
    p ≤ Submodule.comap (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) p ↔
      p ≤ Submodule.comap f p
⊢ (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)).IsFinitelySemisimple ↔
    f.IsFinitelySemisimple

Tactic:
suffices ∀ p : Submodule R M, p ≤ p.comap (f - algebraMap R (Module.End R M) μ) ↔ p ≤ p.comap f by
    simp_rw [isFinitelySemisimple_iff, mem_invtSubmodule, this]
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
q : Submodule R ↥p
hq₁ : q ∈ invtSubmodule (LinearMap.restrict f hp)
hq₂ : Module.Finite.{u_1, u_2} R ↥q
⊢ Submodule.map p.subtype q ∈ f.invtSubmodule

Tactic:
have := invtSubmodule.map_subtype_mem_of_mem_invtSubmodule f hp hq₁
-- Module: Mathlib.LinearAlgebra.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
q : Submodule R ↥p
hq₁ : q ∈ invtSubmodule (LinearMap.restrict f hp)
hq₂ : Module.Finite.{u_1, u_2} R ↥q
this : Submodule.map p.subtype q ∈ f.invtSubmodule
e : ↥q ≃ₗ[R] ↥(Submodule.map p.subtype q) := p.equivSubtypeMap q
rw : IsSemisimple (M := ↥(Submodule.map p.subtype q)) (LinearMap.restrict f this)
⊢ IsSemisimple ((LinearMap.restrict f hp).restrict hq₁)

Tactic:
rw [e.isSemisimple_iff ((LinearMap.restrict f hp).restrict hq₁) (LinearMap.restrict f this) rfl]

Premises used: LinearMap.restrict, LinearEquiv.isSemisimple_iff, rfl