awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) J x y
hJI : J ≤ I
⊢ Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)

Tactic:
have h₁ := idealQuotientMk.mp <| h.mono hJI
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) J x y
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
rw :
  ∀ (h : x - y ∈ J) (hJI : J ≤ I)
    (h₁ :
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)),
    x ^ p - y ^ p ∈ J * I
⊢ SModEq (R := R) (J * I) (x ^ p) (y ^ p)

Tactic:
rw [SModEq.sub_mem] at h ⊢

Premises used: SModEq.sub_mem
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
rw : (x - y) * ∑ i ∈ Finset.range p, y ^ i * x ^ (p - 1 - i) ∈ J * I
⊢ x ^ p - y ^ p ∈ J * I

Tactic:
rw [← Commute.mul_neg_geom_sum₂ (.all _ _)]

Premises used: Commute.mul_neg_geom_sum₂
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ (x - y) * ∑ i ∈ Finset.range p, y ^ i * x ^ (p - 1 - i) ∈ J * I

Tactic:
Ideal.mul_mem_mul h ?_

Premises used: Set.Mem, Ideal.mul_mem_mul
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
refine : ∑ i ∈ Finset.range p, y ^ i * x ^ (p - 1 - i) ∈ I
⊢ (x - y) * ∑ i ∈ Finset.range p, y ^ i * x ^ (p - 1 - i) ∈ J * I

Tactic:
refine Ideal.mul_mem_mul h ?_

Premises used: Ideal.mul_mem_mul
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (↑p : R ⧸ I) 0

Tactic:
simpa using Ideal.Quotient.eq_zero_iff_mem.mpr hpI

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (↑p : R ⧸ I) 0

Tactic:
have h₂ : (p : R ⧸ I) = 0 := by simpa using Ideal.Quotient.eq_zero_iff_mem.mpr hpI
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
h₂ : Eq.{u_1 + 1} (α := R ⧸ I) (↑p : R ⧸ I) 0
simp :
  Eq.{u_1 + 1} (α := R ⧸ I)
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (x + (p - 1 - x)))
    0
⊢ ∑ i ∈ Finset.range p, y ^ i * x ^ (p - 1 - i) ∈ I

Tactic:
simp only [← Ideal.Quotient.eq_zero_iff_mem, map_sum, map_mul, map_pow, h₁, ← pow_add]

Premises used: pow_add, map_pow, map_sum, Ideal.Quotient.eq_zero_iff_mem, map_mul
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
h₂ : Eq.{u_1 + 1} (α := R ⧸ I) (↑p : R ⧸ I) 0
trans :
  Eq.{u_1 + 1} (α := R ⧸ I)
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (x + (p - 1 - x)))
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (p - 1))
trans₁ :
  Eq.{u_1 + 1} (α := R ⧸ I)
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (p - 1)) 0
⊢ Eq.{u_1 + 1} (α := R ⧸ I)
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (x + (p - 1 - x)))
    0

Tactic:
trans ∑ x ∈ Finset.range p, Ideal.Quotient.mk I y ^ (p - 1)

Premises used: Ideal.Quotient.mk, HSub.hSub, Finset.range, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
h₂ : Eq.{u_1 + 1} (α := R ⧸ I) (↑p : R ⧸ I) 0
x_1 : ℕ
h_1 : x_1 ∈ Finset.range p
⊢ HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (x_1 + (p - 1 - x_1)) =
    HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (p - 1)

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
h₂ : Eq.{u_1 + 1} (α := R ⧸ I) (↑p : R ⧸ I) 0
⊢ Eq.{u_1 + 1} (α := R ⧸ I)
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (x + (p - 1 - x)))
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (p - 1))

Tactic:
exact Finset.sum_congr rfl fun _ _ ↦ by grind

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
h₂ : Eq.{u_1 + 1} (α := R ⧸ I) (↑p : R ⧸ I) 0
⊢ Eq.{u_1 + 1} (α := R ⧸ I)
    (∑ x ∈ Finset.range p, HPow.hPow (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I) (p - 1)) 0

Tactic:
simp [h₂]
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
m : ℕ
hm : m ≠ 0
h : SModEq (R := R) (I ^ m) x y
⊢ SModEq (R := R) (I ^ (m + 1)) (x ^ p) (y ^ p)

Tactic:
h.pow_mul_of_le hpI <| I.pow_le_self hm

Premises used: Set.Mem, SModEq.pow_mul_of_le, Ideal.pow_le_self, npowRec
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) I x y
⊢ SModEq (R := R) (I ^ HAdd.hAdd (α := ℕ) 0 1) (x ^ HPow.hPow (β := ℕ) p 0) (y ^ HPow.hPow (β := ℕ) p 0)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) I x y
m : ℕ
ih : SModEq (R := R) (I ^ (m + 1)) (x ^ p ^ m) (y ^ p ^ m)
succ : SModEq (R := R) (I ^ (m + 1 + 1)) ((x ^ p ^ m) ^ p) ((y ^ p ^ m) ^ p)
⊢ SModEq (R := R) (I ^ (m + 1 + 1)) (x ^ p ^ (m + 1)) (y ^ p ^ (m + 1))

Tactic:
simp_rw [pow_succ _ m, pow_mul]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) I x y
m : ℕ
ih : SModEq (R := R) (I ^ (m + 1)) (x ^ p ^ m) (y ^ p ^ m)
⊢ SModEq (R := R) (I ^ (m + 1 + 1)) ((x ^ p ^ m) ^ p) ((y ^ p ^ m) ^ p)

Tactic:
ih.pow_add_one hpI m.succ_ne_zero

Premises used: SModEq.pow_add_one, Nat.succ_ne_zero
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) I x y
m : ℕ
ih : SModEq (R := R) (I ^ (m + 1)) (x ^ p ^ m) (y ^ p ^ m)
⊢ SModEq (R := R) (I ^ (m + 1 + 1)) ((x ^ p ^ m) ^ p) ((y ^ p ^ m) ^ p)

Tactic:
exact ih.pow_add_one hpI m.succ_ne_zero

Premises used: SModEq.pow_add_one, Nat.succ_ne_zero
-- Module: Mathlib.LinearAlgebra.SModEq.Pow
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
p : ℕ
hpI : (↑p : R) ∈ I
x y : R
h : SModEq (R := R) I x y
m : ℕ
zero : SModEq (R := R) (I ^ HAdd.hAdd (α := ℕ) 0 1) (x ^ HPow.hPow (β := ℕ) p 0) (y ^ HPow.hPow (β := ℕ) p 0)
succ :
  ∀ (m : ℕ) (ih : SModEq (R := R) (I ^ (m + 1)) (x ^ p ^ m) (y ^ p ^ m)),
    SModEq (R := R) (I ^ (m + 1 + 1)) (x ^ p ^ (m + 1)) (y ^ p ^ (m + 1))
⊢ SModEq (R := R) (I ^ (m + 1)) (x ^ p ^ m) (y ^ p ^ m)

Tactic:
induction m with
  | zero => simpa
  | succ m ih =>
    simp_rw [pow_succ _ m, pow_mul]
    exact ih.pow_add_one hpI m.succ_ne_zero

Premises used: SModEq.zero, pow_succ, pow_mul
-- 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
rw :
  (∀ (a : ↥(invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f))),
      ∃ (b : ↥(invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f))), IsCompl a b) ↔
    ∀ (p : ↥f.invtSubmodule), ∃ (q : ↥f.invtSubmodule), IsCompl p q
⊢ f.IsSemisimple ↔ ∀ (p : ↥f.invtSubmodule), ∃ (q : ↥f.invtSubmodule), IsCompl p q

Tactic:
rw [IsSemisimple, isSemisimpleModule_iff, (AEval.mapSubmodule R M f).symm.complementedLattice_iff,
    complementedLattice_iff]

Premises used: OrderIso.complementedLattice_iff, Module.AEval.mapSubmodule, complementedLattice_iff, isSemisimpleModule_iff, OrderIso.symm, 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
⊢ (∀ (a : ↥(invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f))),
      ∃ (b : ↥(invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f))), IsCompl a b) ↔
    ∀ (p : ↥f.invtSubmodule), ∃ (q : ↥f.invtSubmodule), IsCompl p q

Tactic:
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
⊢ f.IsSemisimple ↔ ∀ p ∈ f.invtSubmodule, ∃ q ∈ f.invtSubmodule, IsCompl p q

Tactic:
simp [isSemisimple_iff']

Premises used: 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
p : Submodule R M
hp : p ∈ f.invtSubmodule
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)))
simp_rw :
  (∀ (a : Submodule R M)
      (b :
        Membership.mem (γ := Sublattice (Submodule R M))
          (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) a),
      a ≤ p →
        ∃ a_2 ≤ p,
          Membership.mem (γ := Sublattice (Submodule R M))
              (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) a_2 ∧
            a ⊓ a_2 = ⊥ ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p
⊢ IsSemisimple (LinearMap.restrict f hp) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Tactic:
simp_rw [IsSemisimple, isSemisimpleModule_iff, e.complementedLattice_iff, disjoint_iff,
    ← (OrderIso.Iic _ _).complementedLattice_iff, Iic.complementedLattice_iff, Subtype.forall,
    Subtype.exists, Subtype.mk_le_mk, Sublattice.mk_inf_mk, Sublattice.mk_sup_mk, Subtype.mk.injEq,
    exists_and_left, exists_and_right, invtSubmodule.mk_eq_bot_iff, exists_prop, and_assoc]

Premises used: OrderIso.complementedLattice_iff, disjoint_iff, Subtype.exists, Sublattice.mk_inf_mk, exists_and_left, OrderIso.Iic, Set.Iic.complementedLattice_iff, Subtype.forall, isSemisimpleModule_iff, exists_and_right, exists_prop, and_assoc, Subtype.mk.injEq, Module.End.IsSemisimple, Sublattice.mk_sup_mk, Subtype.mk_le_mk, Module.End.invtSubmodule.mk_eq_bot_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
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)))
⊢ (∀ (a : Submodule R M)
      (b :
        Membership.mem (γ := Sublattice (Submodule R M))
          (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) a),
      a ≤ p →
        ∃ a_2 ≤ p,
          Membership.mem (γ := Sublattice (Submodule R M))
              (invtSubmodule ((Algebra.lsmul R R M : (a : End R M) → End R M) f)) a_2 ∧
            a ⊓ a_2 = ⊥ ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p

Tactic:
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
⊢ f.IsFinitelySemisimple ↔
    ∀ (p : Submodule R M) (hp : p ∈ f.invtSubmodule),
      Module.Finite.{u_1, u_2} R ↥p → IsSemisimple (LinearMap.restrict f hp)

Tactic:
Iff.rfl

Premises used: Iff.rfl, 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
inst_3 : IsSemisimpleModule R M
⊢ IsSemisimple.{u_1, u_2} (R := R) (M := M) 0

Tactic:
simpa [isSemisimple_iff] using exists_isCompl

Premises used: ComplementedLattice.exists_isCompl, 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
inst_3 : IsSemisimpleModule R M
⊢ IsSemisimple.{u_1, u_2} (R := R) (M := M) LinearMap.id

Tactic:
simpa [isSemisimple_iff] using exists_isCompl

Premises used: ComplementedLattice.exists_isCompl, 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
⊢ (-f).IsSemisimple ↔ f.IsSemisimple

Tactic:
simp [isSemisimple_iff, mem_invtSubmodule]

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
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
g : End R M₂
e : M ≃ₗ[R] M₂
he : (↑e : M →ₗ[R] M₂) ∘ₗ f = g ∘ₗ (↑e : M →ₗ[R] M₂)
x : M
⊢ ((e ≪≫ₗ AEval'.of g : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) M (AEval' g)) : (a : M) → AEval' g) (f • x) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R[X]) (β := AEval' g) X
      (((e ≪≫ₗ AEval'.of g : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) M (AEval' g)) : (a : M) → AEval' g) x :
        AEval' g)

Tactic:
simpa [AEval'.X_smul_of] using LinearMap.congr_fun he x

Premises used: Module.AEval'.X_smul_of, LinearMap.congr_fun
-- 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
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
g : End R M₂
e_1 : M ≃ₗ[R] M₂
he : (↑e_1 : M →ₗ[R] M₂) ∘ₗ f = g ∘ₗ (↑e_1 : M →ₗ[R] M₂)
e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R[X]) (AEval' f) (AEval' g) :=
  LinearEquiv.ofAEval f (e_1 ≪≫ₗ AEval'.of g) ⋯
simp_rw : IsSemisimpleModule.{u_1, u_2} R[X] (AEval' f) ↔ IsSemisimpleModule.{u_1, u_3} R[X] (AEval' g)
simp_rw₁ :
  ComplementedLattice.{u_2} (Submodule.{u_1, u_2} R[X] (AEval' f)) ↔
    ComplementedLattice.{u_3} (Submodule.{u_1, u_3} R[X] (AEval' g))
⊢ f.IsSemisimple ↔ g.IsSemisimple

Tactic:
simp_rw [IsSemisimple, isSemisimpleModule_iff,
    (Submodule.orderIsoMapComap e).complementedLattice_iff]

Premises used: OrderIso.complementedLattice_iff, isSemisimpleModule_iff, Submodule.orderIsoMapComap, 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
hn : IsNilpotent f
hs : f.IsSemisimple
have : ∀ (n : ℕ) (h0 : f ^ n = 0), f = 0
⊢ f = 0

Tactic:
have ⟨n, h0⟩ := hn
-- 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
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
rw : Eq.{u_2 + 1} (α := End R M) ((aeval f : (a : R[X]) → End R M) X : End R M) (0 : End R M)
⊢ f = 0

Tactic:
rw [← aeval_X (R := R) f]

Premises used: Polynomial.aeval_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
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
⊢ Eq.{u_2 + 1} (α := End R M) ((aeval f : (a : R[X]) → End R M) (HPow.hPow (α := R[X]) X n) : End R M) (0 : End R M)

Tactic:
rw [← aeval_X_pow (R := R) f] at h0

Premises used: Polynomial.aeval_X_pow
-- 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
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : Eq.{u_2 + 1} (α := End R M) ((aeval f : (a : R[X]) → End R M) (HPow.hPow (α := R[X]) X n) : End R M) (0 : End R M)
rw :
  ∀ (h0 : Membership.mem (γ := Ideal R[X]) (annihilator.{u_1, u_2} R[X] (AEval R M f)) (HPow.hPow (α := R[X]) X n)),
    Membership.mem (γ := Ideal R[X]) (annihilator.{u_1, u_2} R[X] (AEval R M f)) X
⊢ Eq.{u_2 + 1} (α := End R M) ((aeval f : (a : R[X]) → End R M) X : End R M) (0 : End R M)

Tactic:
rw [← RingHom.mem_ker, ← AEval.annihilator_eq_ker_aeval (M := M)] at h0 ⊢

Premises used: RingHom.mem_ker, Module.AEval.annihilator_eq_ker_aeval
-- 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
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : Membership.mem (γ := Ideal R[X]) (annihilator.{u_1, u_2} R[X] (AEval R M f)) (HPow.hPow (α := R[X]) X n)
⊢ Membership.mem (γ := Ideal R[X]) (annihilator.{u_1, u_2} R[X] (AEval R M f)) X

Tactic:
hs.annihilator_isRadical _ _ ⟨n, h0⟩

Premises used: Module.AEval.instAddCommMonoid._aux_4, Set.Mem, IsSemisimpleModule.annihilator_isRadical, Module.AEval, Exists.intro, Module.AEval.instAddCommMonoid._aux_1
-- 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
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : Membership.mem (γ := Ideal R[X]) (annihilator.{u_1, u_2} R[X] (AEval R M f)) (HPow.hPow (α := R[X]) X n)
⊢ Membership.mem (γ := Ideal R[X]) (annihilator.{u_1, u_2} R[X] (AEval R M f)) X

Tactic:
exact hs.annihilator_isRadical _ _ ⟨n, h0⟩

Premises used: IsSemisimpleModule.annihilator_isRadical, Exists.intro
-- 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
hn : IsNilpotent f
hs : f.IsFinitelySemisimple
p : Submodule R M
hp₁ : p ∈ f.invtSubmodule
hp₂ : Module.Finite.{u_1, u_2} R ↥p
⊢ IsSemisimple (LinearMap.restrict f hp₁)

Tactic:
specialize hs p hp₁ hp₂
-- 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
hn : IsNilpotent f
p : Submodule R M
hp₁ : p ∈ f.invtSubmodule
hp₂ : Module.Finite.{u_1, u_2} R ↥p
hs : IsSemisimple (LinearMap.restrict f hp₁)
⊢ IsNilpotent (LinearMap.restrict f hp₁)

Tactic:
replace hn : IsNilpotent (f.restrict hp₁) := isNilpotent.restrict hp₁ hn
-- 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
hp₂ : Module.Finite.{u_1, u_2} R ↥p
hs : IsSemisimple (LinearMap.restrict f hp₁)
hn : IsNilpotent (LinearMap.restrict f hp₁)
⊢ LinearMap.restrict f hp₁ = 0

Tactic:
eq_zero_of_isNilpotent_isSemisimple hn hs

Premises used: Set.Mem, Module.End.eq_zero_of_isNilpotent_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
hp₂ : Module.Finite.{u_1, u_2} R ↥p
hs : IsSemisimple (LinearMap.restrict f hp₁)
hn : IsNilpotent (LinearMap.restrict f hp₁)
⊢ LinearMap.restrict f hp₁ = 0

Tactic:
exact eq_zero_of_isNilpotent_isSemisimple hn hs

Premises used: Module.End.eq_zero_of_isNilpotent_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
hn : IsNilpotent f
hs : f.IsFinitelySemisimple
⊢ ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite.{u_1, u_2} R ↥p), LinearMap.restrict f hp₁ = 0

Tactic:
have (p) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite R p) : f.restrict hp₁ = 0 := by
    specialize hs p hp₁ hp₂
    replace hn : IsNilpotent (f.restrict hp₁) := isNilpotent.restrict hp₁ hn
    exact eq_zero_of_isNilpotent_isSemisimple hn hs
-- 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
hn : IsNilpotent f
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
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
⊢ f = 0

Tactic:
ext 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
hn : IsNilpotent f
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
h : ∀ (k : ℕ) (hk : f ^ k = 0), Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
⊢ Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)

Tactic:
obtain ⟨k : ℕ, hk : f ^ k = 0⟩ := hn