awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
κ : ι → Type u_4
inst_4 : (i : ι) → Fintype (κ i)
inst_5 : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
b : (i : ↥s) → Basis.{u_4, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι))
σ : ι → ι
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ (↑i : ι)
hi : σ (↑i : ι) ∈ s
j : ↥s := Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (σ (↑i : ι)) hi
hσ : j ≠ i
⊢ Eq.{u_2 + 1} (α := R)
    (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
              ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
            (i : ↥s) × κ (↑i : ι) →₀ R) :
          (a : (i : ↥s) × κ (↑i : ι)) → R)
        (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
      R)
    (0 : R)

Tactic:
h.collectedBasis_repr_of_mem_ne b hσ <| hf _ <| Subtype.mem (b i k)

Premises used: DirectSum.IsInternal.collectedBasis_repr_of_mem_ne, Subtype.mem, DFunLike.coe
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
κ : ι → Type u_4
inst_4 : (i : ι) → Fintype (κ i)
inst_5 : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
b : (i : ↥s) → Basis.{u_4, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι))
σ : ι → ι
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ (↑i : ι)
hi : σ (↑i : ι) ∈ s
j : ↥s := Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (σ (↑i : ι)) hi
hσ : j ≠ i
⊢ Eq.{u_2 + 1} (α := R)
    (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
              ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
            (i : ↥s) × κ (↑i : ι) →₀ R) :
          (a : (i : ↥s) × κ (↑i : ι)) → R)
        (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
      R)
    (0 : R)

Tactic:
exact h.collectedBasis_repr_of_mem_ne b hσ <| hf _ <| Subtype.mem (b i k)

Premises used: DirectSum.IsInternal.collectedBasis_repr_of_mem_ne, Subtype.mem, DFunLike.coe
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
κ : ι → Type u_4
inst_4 : (i : ι) → Fintype (κ i)
inst_5 : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
b : (i : ↥s) → Basis.{u_4, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι))
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ (↑i : ι)
hi : σ (↑i : ι) ∉ s
this : Eq (α := M) ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M) : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := R)
    (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
              ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
            (i : ↥s) × κ (↑i : ι) →₀ R) :
          (a : (i : ↥s) × κ (↑i : ι)) → R)
        (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
      R)
    (0 : R)

Tactic:
simp [this]
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
κ : ι → Type u_4
inst_4 : (i : ι) → Fintype (κ i)
inst_5 : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
b : (i : ↥s) → Basis.{u_4, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι))
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ (↑i : ι)
hi : σ (↑i : ι) ∉ s
neg : Eq (α := M) ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M) : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := R)
    (((((h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b).repr : (a : M) → (i : ↥s) × κ (↑i : ι) →₀ R)
              ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M)) :
            (i : ↥s) × κ (↑i : ι) →₀ R) :
          (a : (i : ↥s) × κ (↑i : ι)) → R)
        (Sigma.mk (β := fun (i : ↥s) ↦ κ (↑i : ι)) i k) :
      R)
    (0 : R)

Tactic:
suffices f (b i k) = 0 by simp [this]
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
κ : ι → Type u_4
inst_4 : (i : ι) → Fintype (κ i)
inst_5 : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
b : (i : ↥s) → Basis.{u_4, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι))
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ (↑i : ι)
hi : σ (↑i : ι) ∉ s
⊢ Eq (α := M) ((f : (a : M) → M) (↑((b i : (a : κ (↑i : ι)) → ↥(N (↑i : ι))) k) : M) : M) (0 : M)

Tactic:
simpa [hN _ hi] using hf i <| Subtype.mem (b i k)

Premises used: Subtype.mem, Subtype.val, DFunLike.coe
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
b : (i : ι) → Basis.{u_3, u_2, u_3} (Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun (i : ι) ↦ Free.chooseBasis R ↥(N i)
simp_rw :
  Eq.{u_2 + 1} (α := R)
    (Matrix.trace (n := (i : ι) × Free.ChooseBasisIndex R ↥(N i))
      ((toMatrix (h.collectedBasis (α := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)) b)
            (h.collectedBasis (α := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)) b) :
          (a : M →ₗ[R] M) →
            Matrix ((i : ι) × Free.ChooseBasisIndex R ↥(N i)) ((i : ι) × Free.ChooseBasisIndex R ↥(N i)) R)
        f))
    (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯))
simp_rw₁ :
  Eq.{u_2 + 1} (α := R)
    (Matrix.trace (n := (i : ι) × Free.ChooseBasisIndex R ↥(N i))
      (Matrix.blockDiagonal' (m' := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)) (n' := fun (i : ι) ↦
        Free.ChooseBasisIndex R ↥(N i)) fun (i : ι) ↦
        (toMatrix (b i) (b i) :
            (a : ↥(N i) →ₗ[R] ↥(N i)) → Matrix (Free.ChooseBasisIndex R ↥(N i)) (Free.ChooseBasisIndex R ↥(N i)) R)
          (f.restrict ⋯)))
    (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯))
simp_rw₂ :
  Eq.{u_2 + 1} (α := R)
    (∑ i : ι,
      Matrix.trace.{u_3, u_2} (n := Free.ChooseBasisIndex R ↥(N i))
        ((toMatrix (b i) (b i) :
            (a : ↥(N i) →ₗ[R] ↥(N i)) → Matrix (Free.ChooseBasisIndex R ↥(N i)) (Free.ChooseBasisIndex R ↥(N i)) R)
          (f.restrict ⋯)))
    (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯))
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
    (∑ i : ι, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯) : R)

Tactic:
simp_rw [trace_eq_matrix_trace R (h.collectedBasis b),
    toMatrix_directSum_collectedBasis_eq_blockDiagonal' h h b b hf, Matrix.trace_blockDiagonal',
    ← trace_eq_matrix_trace]

Premises used: Matrix.trace_blockDiagonal', DirectSum.IsInternal.collectedBasis, LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal', LinearMap.trace_eq_matrix_trace
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
x : Fintype { i : ι // N i ≠ ⊥ } := hN.fintype (s := {i : ι | N i ≠ ⊥})
x_1 : Fintype (↑{i : ι | N i ≠ ⊥} : Type u_1) := hN.fintype (s := {i : ι | N i ≠ ⊥})
rw :
  Eq.{u_2 + 1} (α := R)
    (∑ i : { i : ι // N i ≠ ⊥ }, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (f.restrict ⋯))
    (∑ i : ↥hN.toFinset, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (f.restrict ⋯))
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
    (∑ i ∈ hN.toFinset (s := {i : ι | N i ≠ ⊥}), (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (f.restrict ⋯) : R)

Tactic:
rw [← Finset.sum_coe_sort, trace_eq_sum_trace_restrict (isInternal_ne_bot_iff.mpr h) (hf ·)]

Premises used: Iff.mpr, DirectSum.isInternal_ne_bot_iff, LinearMap.trace_eq_sum_trace_restrict, Subtype.val, Finset.sum_coe_sort
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
x : Fintype { i : ι // N i ≠ ⊥ } := hN.fintype (s := {i : ι | N i ≠ ⊥})
x_1 : Fintype (↑{i : ι | N i ≠ ⊥} : Type u_1) := hN.fintype (s := {i : ι | N i ≠ ⊥})
⊢ Eq.{u_2 + 1} (α := R)
    (∑ i : { i : ι // N i ≠ ⊥ }, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (f.restrict ⋯))
    (∑ i : ↥hN.toFinset, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (f.restrict ⋯))

Tactic:
Fintype.sum_equiv hN.subtypeEquivToFinset _ _ (fun i ↦ rfl)

Premises used: Set.Mem, setOf, Set.Finite.subtypeEquivToFinset, Fintype.sum_equiv, Not, rfl
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
x : Fintype { i : ι // N i ≠ ⊥ } := hN.fintype (s := {i : ι | N i ≠ ⊥})
x_1 : Fintype (↑{i : ι | N i ≠ ⊥} : Type u_1) := hN.fintype (s := {i : ι | N i ≠ ⊥})
⊢ Eq.{u_2 + 1} (α := R)
    (∑ i : { i : ι // N i ≠ ⊥ }, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (f.restrict ⋯))
    (∑ i : ↥hN.toFinset, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (f.restrict ⋯))

Tactic:
exact Fintype.sum_equiv hN.subtypeEquivToFinset _ _ (fun i ↦ rfl)

Premises used: Set.Finite.subtypeEquivToFinset, Fintype.sum_equiv, rfl
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
⊢ Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}

Tactic:
have hN : {i | N i ≠ ⊥}.Finite := WellFoundedGT.finite_ne_bot_of_iSupIndep
    h.submodule_iSupIndep
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
⊢ IsInternal (S := Submodule R M) fun (i : { i : ι // N i ≠ ⊥ }) ↦ N (↑i : ι)

Tactic:
DirectSum.isInternal_ne_bot_iff.mpr h

Premises used: Iff.mpr, DirectSum.isInternal_ne_bot_iff
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
h₁ : ∀ (x : ι), x ∈ s ↔ N x ≠ ⊥
h₂ : ↥s = { i : ι // N i ≠ ⊥ } → ∀ (a : ↥s) (a' : { i : ι // N i ≠ ⊥ }), a ≍ a' → ∀ (x : ι), x ∈ s ↔ N x ≠ ⊥
⊢ IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)

Tactic:
convert! DirectSum.isInternal_ne_bot_iff.mpr h

Premises used: Iff.mpr, DirectSum.isInternal_ne_bot_iff
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
x : ι
⊢ x ∈ s ↔ N x ≠ ⊥

Tactic:
simp [s]
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
e_1 : ↥s = { i : ι // N i ≠ ⊥ }
a : ↥s
a' : { i : ι // N i ≠ ⊥ }
h_1 : a ≍ a'
x : ι
⊢ x ∈ s ↔ N x ≠ ⊥

Tactic:
simp [s]
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
h : IsInternal N
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
⊢ IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)

Tactic:
replace h : IsInternal fun i : s ↦ N i := by
    convert! DirectSum.isInternal_ne_bot_iff.mpr h <;> simp [s]
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
⊢ ∀ i ∉ s, N i = ⊥

Tactic:
simp [s]
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : ι → Submodule R M
inst_3 : DecidableEq ι
inst_4 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_5 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
inst_6 : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N (σ i)) : Set M)
hN : Set.Finite.{u_1} (α := ι) {i : ι | N i ≠ ⊥}
s : Finset ι := hN.toFinset (s := {i : ι | N i ≠ ⊥})
κ : (i : ι) → Type u_3 := fun (i : ι) ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis.{u_3, u_2, u_3} (κ (↑i : ι)) R ↥(N (↑i : ι)) := fun (i : ↥s) ↦ Free.chooseBasis R ↥(N (↑i : ι))
h : IsInternal (S := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
simp_rw :
  Eq.{u_2 + 1} (α := R)
    (Matrix.trace (n := (i : ↥s) × κ (↑i : ι))
      ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
            (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
          (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
        f))
    0
simp_rw₁ :
  Eq.{u_2 + 1} (α := R)
    (∑ i : (i : ↥s) × κ (↑i : ι),
      Matrix.diag
        ((toMatrix (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b)
              (h.collectedBasis (α := fun (i : ↥s) ↦ κ (↑i : ι)) b) :
            (a : M →ₗ[R] M) → Matrix ((i : ↥s) × κ (↑i : ι)) ((i : ↥s) × κ (↑i : ι)) R)
          f)
        i)
    0
simp_rw₂ : Eq.{u_2 + 1} (α := R) (∑ x : (i : ↥s) × κ (↑i : ι), 0 x) 0
simp_rw₃ : Eq.{u_2 + 1} (α := R) (∑ x : (i : ↥s) × κ (↑i : ι), 0) 0
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) (0 : R)

Tactic:
simp_rw [trace_eq_matrix_trace R (h.collectedBasis b), Matrix.trace,
    diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne h b σ hσ hf (by simp [s]),
    Pi.zero_apply, Finset.sum_const_zero]

Premises used: Pi.zero_apply, Matrix.trace, DirectSum.IsInternal.collectedBasis, Finset.sum_const_zero, LinearMap.trace_eq_matrix_trace, LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Free R M
inst_6 : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : Eq.{u_3 + 1} (α := Submodule R M) (⨆ (μ : R), f.maxGenEigenspace μ) ⊤
hg :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R)
      (0 : R)
⊢ ∀ (μ : R), MapsTo (⇑(g ∘ₗ f) : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)

Tactic:
have hfg : ∀ μ,
      MapsTo (g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ) :=
    fun μ ↦ (f.mapsTo_maxGenEigenspace_of_comm h_comm μ).comp
      (f.mapsTo_maxGenEigenspace_of_comm rfl μ)
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Free R M
inst_6 : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : Eq.{u_3 + 1} (α := Submodule R M) (⨆ (μ : R), f.maxGenEigenspace μ) ⊤
hg :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R)
      (0 : R)
hfg : ∀ (μ : R), MapsTo (⇑(g ∘ₗ f) : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
this :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          ((g ∘ₗ f).restrict ⋯) :
        R)
      (0 : R)
⊢ IsInternal f.maxGenEigenspace

Tactic:
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
      f.independent_maxGenEigenspace hf
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Free R M
inst_6 : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : Eq.{u_3 + 1} (α := Submodule R M) (⨆ (μ : R), f.maxGenEigenspace μ) ⊤
hg :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R)
      (0 : R)
hfg : ∀ (μ : R), MapsTo (⇑(g ∘ₗ f) : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
this :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          ((g ∘ₗ f).restrict ⋯) :
        R)
      (0 : R)
hds : IsInternal f.maxGenEigenspace
⊢ Set.Finite.{u_2} (α := R) {μ : R | f.maxGenEigenspace μ ≠ ⊥}

Tactic:
have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
      WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
-- Module: Mathlib.Algebra.DirectSum.LinearMap
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
inst_5 : Free R M
inst_6 : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : Eq.{u_3 + 1} (α := Submodule R M) (⨆ (μ : R), f.maxGenEigenspace μ) ⊤
hg :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R)
      (0 : R)
hfg : ∀ (μ : R), MapsTo (⇑(g ∘ₗ f) : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
this :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          ((g ∘ₗ f).restrict ⋯) :
        R)
      (0 : R)
hds : IsInternal f.maxGenEigenspace
h_fin : Set.Finite.{u_2} (α := R) {μ : R | f.maxGenEigenspace μ ≠ ⊥}
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)

Tactic:
simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]

Premises used: LinearMap.trace_eq_sum_trace_restrict'