Avoiding deterministic timeout

Stream: new members

[Hanting Zhang]

Hi, I've been struggling with this deterministic timeout problem. I've gotten around some of them by adding convert anywhere I could, but I seem to have hit a dead end now. I somewhat suspect that casting submodules to modules and taking their direct sum makes Lean slow and confused, but I'm not sure why.
How do I fix this deterministic timeout error? (And if possible, how can I make Lean faster here?) Thanks in advance!

import ring_theory.simple_module
import linear_algebra.matrix
import linear_algebra.direct_sum_module

open_locale direct_sum classical big_operators
open classical linear_map
noncomputable theory

variables {ι : Type*} {R : Type*} [ring R] {M : Type*} [add_comm_group M] [module R M]

def submodule.inclusion (N P : submodule R M) (h : N ≤ P) : N →ₗ[R] P :=
{ to_fun := λ x, ⟨x.1, h x.2⟩, map_add' := λ ⟨x, hx⟩ ⟨y, hy⟩, rfl, map_smul' := λ r ⟨x, hx⟩, rfl }

def terrible_map (p : ι → submodule R M) :=
(direct_sum.to_module R ι _ (λ i, (p i).inclusion (supr p) (le_supr p i)))

lemma terrible_map_ker (p : ι → submodule R M) (h : complete_lattice.independent p) :
  (terrible_map p).ker = ⊥ := sorry

lemma terrible_map_range (p : ι → submodule R M) (h : complete_lattice.independent p) :
  (terrible_map p).range = ⊤ := sorry

def submodule.prod_equiv_of_independent
  (p : ι → submodule R M) (h : complete_lattice.independent p) :
  (⨁ i, p i) ≃ₗ[R] (supr p : submodule R M) :=
begin
  letI : add_comm_group (⨁ (i : ι), (p i)) := direct_sum.add_comm_group (λ i, p i),
  convert @linear_equiv.of_bijective R (⨁ i, p i) (supr p : submodule R M) _ _ _ _ _ _ _ _,
  convert terrible_map p,
  -- If I remove the last two lines, it works.
  -- Even weirder,  `by convert ...` works on my main file. The proof can be completed. But it doesn't work if I move it into a scratch file.
  dsimp,
  convert terrible_map_ker p h,
end

[Hanting Zhang]

Ah I figured it out. I wrote ⊤ instead of ⊥ for terrible_map_ker...

[Eric Wieser]

I think your submodule.inclusion is docs#submodule.of_le

[Eric Wieser]

(deleted)

[Eric Wieser]

Also, I should warn you that the breadcrumbs you appear to be following in the module doc of direct_sum_graded may not actually lead where I said they would.