Stack Overflow error

Stream: new members

[Coleton Kotch]

In showing that the 0-indexed module of a filtered R-algebra is a sub algebra I have found that Lean crashes upon entering tactic mode to prove that this module contains the image of R under the algebra morphism. VS-code gives the following error message.

Error - 3:18:14 PM] Request textDocument/codeAction failed.
  Message: Server process for file:///home/coleton/Lean/USRA24/Main/MWE.lean crashed, likely due to a stack overflow or a bug.
  Code: -32902
libc++abi: terminating due to uncaught exception of type lean::stack_space_exception: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
[Error - 3:18:23 PM] Request textDocument/documentSymbol failed.

I have a MWE setup as follows

import Mathlib.Algebra.Algebra.Subalgebra.Basic

universe u v w

variable {R : Type u} {M : Type v} {ι : Type w}
[CommRing R] [AddCommGroup M] [Module R M] [OrderedAddCommMonoid ι]

class FilteredModule (𝓜 : ι → Submodule R M) where
  whole : iSup 𝓜 = ⊤
  mono : Monotone 𝓜

variable {R : Type u} {A : Type v} {ι : Type w}
[CommRing R] [Ring A] [Algebra R A] [OrderedAddCommMonoid ι]

class FilteredAlgebra (𝓐 : ι → Submodule R A) extends FilteredModule 𝓐 where
  mul_compat' : ∀ i j, 𝓐 i * 𝓐 j ≤ 𝓐 (i + j)
  one' : 1 ∈ 𝓐 0

namespace FilteredAlgebra

lemma mul_compat {𝓐 : ι → Submodule R A} [FilteredAlgebra 𝓐] :
  ∀ i j, a ∈ 𝓐 i → b ∈ 𝓐 j → a * b ∈ 𝓐 (i + j) := fun i j h₁ h₂ =>
    mul_compat' i j <| Submodule.mul_mem_mul h₁ h₂

def instSubAlgebraZero (𝓐 : ι → Submodule R A) [FilteredAlgebra 𝓐] : Subalgebra R A where
  carrier := 𝓐 0
  mul_mem' a b := by
    let h := mul_compat 0 0 a b
    simp only [add_zero] at h
    exact h
  add_mem' := Submodule.add_mem (𝓐 0)
  algebraMap_mem' r := by
    sorry

end FilteredAlgebra

If we remove by to simply get algebraMap_mem' := sorry there is no issue.

On a related note, I was wondering if there were any nice tools one could use to run a stack trace. The manual mentions using gdb or lldb, but I was wondering about other options.

[Coleton Kotch]

I am able to complete the prove as follows, however I am still curious as to what is causing the error

import Mathlib.Algebra.Algebra.Subalgebra.Basic

universe u v w

variable {R : Type u} {M : Type v} {ι : Type w}
[CommRing R] [AddCommGroup M] [Module R M] [OrderedAddCommMonoid ι]

class FilteredModule (𝓜 : ι → Submodule R M) where
  whole : iSup 𝓜 = ⊤
  mono : Monotone 𝓜

variable {R : Type u} {A : Type v} {ι : Type w}
[CommRing R] [Ring A] [Algebra R A] [OrderedAddCommMonoid ι]

class FilteredAlgebra (𝓐 : ι → Submodule R A) extends FilteredModule 𝓐 where
  mul_compat' : ∀ i j, 𝓐 i * 𝓐 j ≤ 𝓐 (i + j)
  one' : 1 ∈ 𝓐 0

namespace FilteredAlgebra

lemma r_in_zero (𝓐 : ι → Submodule R A) [FilteredAlgebra 𝓐] (r : R) : algebraMap R A r ∈ (𝓐 0) := by
    simp only [Algebra.algebraMap_eq_smul_one]
    exact Submodule.smul_mem (𝓐 0) r one'

lemma mul_compat {𝓐 : ι → Submodule R A} [FilteredAlgebra 𝓐] :
  ∀ i j, a ∈ 𝓐 i → b ∈ 𝓐 j → a * b ∈ 𝓐 (i + j) := fun i j h₁ h₂ =>
    mul_compat' i j <| Submodule.mul_mem_mul h₁ h₂

def instSubAlgebraZero (𝓐 : ι → Submodule R A) [FilteredAlgebra 𝓐] : Subalgebra R A where
  carrier := 𝓐 0
  mul_mem' a b := by
    let h := mul_compat 0 0 a b
    simp only [add_zero] at h
    exact h
  add_mem' := Submodule.add_mem (𝓐 0)
  algebraMap_mem' r := (r_in_zero 𝓐 r)

end FilteredAlgebra