awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
have have₁ have₂ :
  ∀ (hds : IsInternal f.maxGenEigenspace),
    Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)
have₃ :
  ∀ (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)
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)

Tactic:
classical
    have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
      f.independent_maxGenEigenspace hf
    have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
      WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
    simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]
-- 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)
suffices :
  ∀ (μ : R),
    Eq.{u_2 + 1} (α := R)
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          ((g ∘ₗ f).restrict ⋯) :
        R)
      (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R) (0 : R)

Tactic:
suffices ∀ μ, trace R _ ((g ∘ₗ f).restrict (hfg μ)) = 0 by
    classical
    have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
      f.independent_maxGenEigenspace hf
    have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
      WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
    simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]
-- 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)
μ : R
⊢ MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)

Tactic:
have hf' := f.mapsTo_maxGenEigenspace_of_comm (Commute.refl _) μ
-- 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)
μ : R
hf' : MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
⊢ MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)

Tactic:
have hg' := f.mapsTo_maxGenEigenspace_of_comm h_comm μ
-- 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)
μ : R
hf' : MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
hg' : MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
⊢ Commute (restrict g ⋯) (restrict f ⋯)

Tactic:
replace h_comm : Commute (g.restrict (f.mapsTo_maxGenEigenspace_of_comm h_comm μ))
      (f.restrict (f.mapsTo_maxGenEigenspace_of_comm rfl μ)) :=
    restrict_commute h_comm.symm _ _
-- 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_1 : 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)
μ : R
hf' : MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
hg' : MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
⊢ IsNilpotent (restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) ⋯)

Tactic:
have := f.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap μ
-- 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_1 : 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)
μ : R
hf' : MapsTo (⇑f : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
hg' : MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) ⋯)
rw :
  Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        (restrict g hg' ∘ₗ restrict f hf') :
      R)
    (0 : R)
rw₁ :
  HMul.hMul (β := R) μ
      ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
          (restrict g ⋯) :
        R) =
    0
rw₂ : μ * 0 = 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R ↥(f.maxGenEigenspace μ) : (a : ↥(f.maxGenEigenspace μ) →ₗ[R] ↥(f.maxGenEigenspace μ)) → R)
        ((g ∘ₗ f).restrict ⋯) :
      R)
    (0 : R)

Tactic:
rw [restrict_comp hf' hg', trace_comp_eq_mul_of_commute_of_isNilpotent μ h_comm this,
    hg, mul_zero]

Premises used: LinearMap.restrict_comp, LinearMap.trace_comp_eq_mul_of_commute_of_isNilpotent, MulZeroClass.mul_zero, Set.MapsTo.comp
-- 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
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
⊢ ∀ (i : ι), Submodule.map f (N i) ≤ N i

Tactic:
replace hf : ∀ i, (N i).map f ≤ N i := fun i ↦ Submodule.map_le_iff_le_comap.mpr (hf i)
-- 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
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : End R M
hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i
suffices : Submodule.map f (⨆ i ∈ s, N i) ≤ ⨆ i ∈ s, N i
⊢ MapsTo (⇑f : (a : M) → M) (↑(⨆ i ∈ s, N i) : Set M) (↑(⨆ i ∈ s, N i) : Set M)

Tactic:
suffices (⨆ i ∈ s, N i).map f ≤ ⨆ i ∈ s, N i from Submodule.map_le_iff_le_comap.mp this
-- 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
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : End R M
hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i
⊢ Submodule.map f (⨆ i ∈ s, N i) ≤ ⨆ i ∈ s, N i

Tactic:
simpa only [Submodule.map_iSup] using iSup₂_mono <| fun i _ ↦ hf i

Premises used: Submodule.map_iSup, iSup₂_mono
-- 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 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_4 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
s : Finset ι
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule R M) fun (i : ↥s) ↦ N (↑i : ι)
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι))
⊢ IsInternal N'

Tactic:
replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_iSupIndep (s : Set ι) h
-- 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 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_4 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι))
h : IsInternal N'
i : ↥s
x : ↥p
hx' : x ∈ (↑(N' i) : Set ↥p)
⊢ Membership.mem (α := ↥p) (↑(N' i) : Set ↥p) ((restrict f hp' : (a : ↥p) → ↥p) x : ↥p)

Tactic:
simpa using hf i hx'

Premises used: Subtype.val
-- 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 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_4 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι))
h : IsInternal N'
⊢ ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p)

Tactic:
have hf' : ∀ i, MapsTo (restrict f hp') (N' i) (N' i) := fun i x hx' ↦ by simpa using hf i hx'
-- 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 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_4 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι))
h : IsInternal N'
hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p)
e : (i : ↥s) → ↥(N' i) ≃ₗ[R] ↥(N (↑i : ι)) :=
  fun (x : ↥s) ↦
    match (motive := (x : ↥s) → ↥(N' x) ≃ₗ[R] ↥(N (↑x : ι))) x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
⊢ ∀ (i : ↥s), Module.Finite.{u_2, u_3} R ↥(N' i)

Tactic:
have _i1 : ∀ i, Module.Finite R (N' i) := fun i ↦ Module.Finite.equiv (e i).symm
-- 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 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_4 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι))
h : IsInternal N'
hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p)
e : (i : ↥s) → ↥(N' i) ≃ₗ[R] ↥(N (↑i : ι)) :=
  fun (x : ↥s) ↦
    match (motive := (x : ↥s) → ↥(N' x) ≃ₗ[R] ↥(N (↑x : ι))) x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : ↥s), Module.Finite.{u_2, u_3} R ↥(N' i)
⊢ ∀ (i : ↥s), Free.{u_2, u_3} R ↥(N' i)

Tactic:
have _i2 : ∀ i, Module.Free R (N' i) := fun i ↦ Module.Free.of_equiv (e i).symm
-- 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 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_4 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι))
h : IsInternal N'
hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p)
e : (i : ↥s) → ↥(N' i) ≃ₗ[R] ↥(N (↑i : ι)) :=
  fun (x : ↥s) ↦
    match (motive := (x : ↥s) → ↥(N' x) ≃ₗ[R] ↥(N (↑x : ι))) x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : ↥s), Module.Finite.{u_2, u_3} R ↥(N' i)
_i2 : ∀ (i : ↥s), Free.{u_2, u_3} R ↥(N' i)
rw :
  Eq.{u_2 + 1} (α := R) (∑ i : ↥s, (trace R ↥(N' i) : (a : ↥(N' i) →ₗ[R] ↥(N' i)) → R) ((restrict f hp').restrict ⋯))
    (∑ i : ↥s, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (restrict f ⋯))
⊢ Eq.{u_2 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (restrict f hp') : R)
    (∑ i ∈ s, (trace R ↥(N i) : (a : ↥(N i) →ₗ[R] ↥(N i)) → R) (restrict f ⋯) : R)

Tactic:
rw [trace_eq_sum_trace_restrict h hf', ← s.sum_coe_sort]

Premises used: LinearMap.trace_eq_sum_trace_restrict, 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 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_4 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι))
h : IsInternal N'
hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p)
e : (i : ↥s) → ↥(N' i) ≃ₗ[R] ↥(N (↑i : ι)) :=
  fun (x : ↥s) ↦
    match (motive := (x : ↥s) → ↥(N' x) ≃ₗ[R] ↥(N (↑x : ι))) x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : ↥s), Module.Finite.{u_2, u_3} R ↥(N' i)
_i2 : ∀ (i : ↥s), Free.{u_2, u_3} R ↥(N' i)
⊢ ∀ (i : ↥s),
    Eq (α := ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) (restrict f ⋯)
      (((e i).conj : (a : End R ↥(N' i)) → End R ↥(N (↑i : ι))) ((restrict f hp').restrict ⋯))

Tactic:
have : ∀ i : s, f.restrict (hf i) = (e i).conj ((f.restrict hp').restrict (hf' i)) := fun _ ↦ 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 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(N i)
inst_4 : ∀ (i : ι), Free.{u_2, u_3} R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo (⇑f : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
N' : ↥s → Submodule R ↥p := fun (i : ↥s) ↦ Submodule.comap p.subtype (N (↑i : ι))
h : IsInternal N'
hf' : ∀ (i : ↥s), MapsTo (⇑(restrict f hp') : (a : ↥p) → ↥p) (↑(N' i) : Set ↥p) (↑(N' i) : Set ↥p)
e : (i : ↥s) → ↥(N' i) ≃ₗ[R] ↥(N (↑i : ι)) :=
  fun (x : ↥s) ↦
    match (motive := (x : ↥s) → ↥(N' x) ≃ₗ[R] ↥(N (↑x : ι))) x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : ↥s), Module.Finite.{u_2, u_3} R ↥(N' i)
_i2 : ∀ (i : ↥s), Free.{u_2, u_3} R ↥(N' i)
this :
  ∀ (i : ↥s),
    Eq (α := ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) (restrict f ⋯)
      (((e i).conj : (a : End R ↥(N' i)) → End R ↥(N (↑i : ι))) ((restrict f hp').restrict ⋯))
⊢ Eq.{u_2 + 1} (α := R) (∑ i : ↥s, (trace R ↥(N' i) : (a : ↥(N' i) →ₗ[R] ↥(N' i)) → R) ((restrict f hp').restrict ⋯))
    (∑ i : ↥s, (trace R ↥(N (↑i : ι)) : (a : ↥(N (↑i : ι)) →ₗ[R] ↥(N (↑i : ι))) → R) (restrict f ⋯))

Tactic:
simp [this]
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
S : Type u_1
inst_3 : Semiring S
inst_4 : (i : ι) → Module.{u_1, w} S (M i)
inst_5 : ∀ (i : ι), SMulCommClass.{u, u_1, w} R S (M i)
⊢ SMulCommClass R S (⨁ (i : ι), M i)

Tactic:
inferInstanceAs <| SMulCommClass R S (Π₀ i, M i)

Premises used: _private.0.DirectSum.instSMulCommClass._proof_1
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
S : Type u_1
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : (i : ι) → Module.{u_1, w} S (M i)
inst_6 : ∀ (i : ι), IsScalarTower.{u, u_1, w} R S (M i)
⊢ IsScalarTower R S (⨁ (i : ι), M i)

Tactic:
inferInstanceAs <| IsScalarTower R S (Π₀ i, M i)

Premises used: _private.0.DirectSum.instIsScalarTower._proof_1
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : (i : ι) → Module.{u, w} Rᵐᵒᵖ (M i)
inst_4 : ∀ (i : ι), IsCentralScalar.{u, w} R (M i)
⊢ IsCentralScalar R (⨁ (i : ι), M i)

Tactic:
inferInstanceAs <| IsCentralScalar R (Π₀ i, M i)

Premises used: _private.0.DirectSum.instIsCentralScalar._proof_1
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
b : R
v : ⨁ (i : ι), M i
i : ι
⊢ (b • v : (a : ι) → M a) i = b • (v : (a : ι) → M a) i

Tactic:
DFinsupp.smul_apply _ _ _

Premises used: DFinsupp.smul_apply
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
v : ⨁ (i : ι), M i
⊢ (coeFnLinearMap R (M := M) : (a : ⨁ (i : ι), M i) → (i : ι) → M i) v = (⇑v : (a : ι) → M a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
i : ι
b : M i
⊢ Eq (α := ⨁ (i : ι), M i) ((lof R ι M i : (a : M i) → ⨁ (i : ι), M i) b : ⨁ (i : ι), M i)
    ((of M i : (a : M i) → ⨁ (i : ι), M i) b : ⨁ (i : ι), M i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
i : ι
b : M i
⊢ Eq (α := Π₀ (i : ι), M i) (DFinsupp.single (β := M) i b) ((lof R ι M i : (a : M i) → ⨁ (i : ι), M i) b)

Tactic:
rfl

Premises used: DFinsupp.single, rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
s : Finset ι
c : R
x : (i : (↑(↑s : Set ι) : Type v)) → M (↑i : ι)
⊢ (mk M s : (a : (i : (↑(↑s : Set ι) : Type v)) → M (↑i : ι)) → ⨁ (i : ι), M i) (c • x) =
    HSMul.hSMul (β := ⨁ (i : ι), M i) c
      ((mk M s : (a : (i : (↑(↑s : Set ι) : Type v)) → M (↑i : ι)) → ⨁ (i : ι), M i) x : ⨁ (i : ι), M i)

Tactic:
(lmk R ι M s).map_smul c x

Premises used: LinearMap.map_smul, DirectSum.lmk
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
i : ι
c : R
x : M i
⊢ (of M i : (a : M i) → ⨁ (i : ι), M i) (c • x) =
    HSMul.hSMul (β := ⨁ (i : ι), M i) c ((of M i : (a : M i) → ⨁ (i : ι), M i) x : ⨁ (i : ι), M i)

Tactic:
(lof R ι M i).map_smul c x

Premises used: LinearMap.map_smul, DirectSum.lof
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
inst_4 : (i : ι) → (x : M i) → Decidable (x ≠ 0)
c : R
v : ⨁ (i : ι), M i
⊢ DFinsupp.support (β := fun (i : ι) ↦ M i) (c • v) ⊆ DFinsupp.support (β := fun (i : ι) ↦ M i) v

Tactic:
DFinsupp.support_smul _ _

Premises used: Set.Mem, setOf, DFinsupp.support_smul
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
N : Type u₁
inst_4 : AddCommMonoid N
inst_5 : Module R N
φ : (i : ι) → LinearMap.{u, u, w, u₁} (RingHom.id R) (M i) N
⊢ Eq (α := (a : ⨁ (i : ι), M i) → N) (⇑(toModule R ι (M := M) N φ) : (a : ⨁ (i : ι), M i) → N)
    (⇑(toAddMonoid (β := M) fun (i : ι) ↦ (φ i).toAddMonoidHom) : (a : ⨁ (i : ι), M i) → N)

Tactic:
rfl

Premises used: rfl, Trunc.lift
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
N : Type u₁
inst_4 : AddCommMonoid N
inst_5 : Module R N
φ : (i : ι) → LinearMap.{u, u, w, u₁} (RingHom.id R) (M i) N
i : ι
x : M i
⊢ Eq.{u₁ + 1} (α := N)
    ((toModule R ι (M := M) N φ : (a : ⨁ (i : ι), M i) → N)
        ((lof R ι M i : (a : M i) → ⨁ (i : ι), M i) x : ⨁ (i : ι), M i) :
      N)
    ((φ i : (a : M i) → N) x : N)

Tactic:
toAddMonoid_of (fun i ↦ (φ i).toAddMonoidHom) i x

Premises used: LinearMap.toAddMonoidHom, Multiset.sum, Multiset.foldr, List.foldr, DirectSum.toAddMonoid_of, Finset.sum, Trunc.lift