!4#3001

Stream: mathlib4

[Xavier Roblot]

This PR is almost ready but few problems are left that I do not know how to solve.

A first not-blocking issue is on line 96

exact fun m ↦ @AddSubmonoid.supᵢ_induction _ _ _ ℳ' _ _ (mem m)

Here, it is necessary to use the @ version of the function even though no implicit argument is provided otherwise it fails. I guess that is not really a problem and I just left a porting note.

The real problems are later on in the file.

• Line 133:

@[simps (config := { fullyApplied := false })]
def decomposeAddEquiv : M ≃+ ⨁ i, ℳ i :=
  AddEquiv.symm { (decompose ℳ).symm with map_add' := map_add (DirectSum.coeAddMonoidHom ℳ) }
#align direct_sum.decompose_add_equiv DirectSum.decomposeAddEquiv

The simps is causing a maximum recursion depth has been reached error. Changing simps to simps! as suggested by lint does not fix the problem. Commenting out the simps does fix the error but it is probably not the right solution.

• Lines 233 -242:

@[simps (config := { fullyApplied := false })]
def decomposeLinearEquiv : M ≃ₗ[R] ⨁ i, ℳ i :=
  LinearEquiv.symm
    { (decomposeAddEquiv ℳ).symm with map_smul' := map_smul (DirectSum.coeLinearMap ℳ) }
#align direct_sum.decompose_linear_equiv DirectSum.decomposeLinearEquiv

@[simp]
theorem decompose_smul (r : R) (x : M) : decompose ℳ (r • x) = r • decompose ℳ x :=
  map_smul (decomposeLinearEquiv ℳ) r x
#align direct_sum.decompose_smul DirectSum.decompose_smul

There the errors are multiple timeout at 'whnf' and timeout at 'isDefEq'. Changing the heartbeats to any reasonable value does not fix the problem. The first error for the second lemma decompose_smul actually happens during the statement and is quite confusing:

type mismatch
  ↑(decompose ℳ) (r • x)
has type
  (fun x => DirectSum ι fun i => { x // x ∈ ℳ i }) (r • x) : Type (max ?u.202504 ?u.202498)
but is expected to have type
  (fun x => DirectSum ι fun i => { x // x ∈ ℳ i }) (r • x) : Type (max ?u.202504 ?u.202498)

[Alex J. Best]

if you turn on pp.all is there any difference?

[Xavier Roblot]

Alex J. Best said:

if you turn on pp.all is there any difference?

I am guessing you are interested in the last error I mentioned. It becomes now

type mismatch
  @FunLike.coe.{max (?u.202436 + 1) (?u.202442 + 1), ?u.202442 + 1, max (?u.202436 + 1) (?u.202442 + 1)}
    (Equiv.{?u.202442 + 1, max (?u.202442 + 1) (?u.202436 + 1)} M
      (@DirectSum.{?u.202436, ?u.202442} ι
        (fun (i : ι) =>
          @Subtype.{?u.202442 + 1} M fun (x : M) =>
            @Membership.mem.{?u.202442, ?u.202442} M (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
              (@SetLike.instMembership.{?u.202442, ?u.202442}
                (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) M
                (@Submodule.setLike.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹))
              x (ℳ i))
        fun (i : ι) =>
        @AddSubmonoidClass.toAddCommMonoid.{?u.202442, ?u.202442} M inst✝²
          (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
          (@Submodule.setLike.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
          (@Submodule.addSubmonoidClass.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) (ℳ i)))
    M
    (fun (a : M) =>
      (fun (x : M) =>
          @DirectSum.{?u.202436, ?u.202442} ι
            (fun (i : ι) =>
              @Subtype.{?u.202442 + 1} M fun (x : M) =>
                @Membership.mem.{?u.202442, ?u.202442} M (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
                  (@SetLike.instMembership.{?u.202442, ?u.202442}
                    (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) M
                    (@Submodule.setLike.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹))
                  x (ℳ i))
            fun (i : ι) =>
            @AddSubmonoidClass.toAddCommMonoid.{?u.202442, ?u.202442} M inst✝²
              (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
              (@Submodule.setLike.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
              (@Submodule.addSubmonoidClass.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) (ℳ i))
        a)
    (@Equiv.instFunLikeEquiv.{?u.202442 + 1, max (?u.202436 + 1) (?u.202442 + 1)} M
      (@DirectSum.{?u.202436, ?u.202442} ι
        (fun (i : ι) =>
          @Subtype.{?u.202442 + 1} M fun (x : M) =>
            @Membership.mem.{?u.202442, ?u.202442} M (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
              (@SetLike.instMembership.{?u.202442, ?u.202442}
                (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) M
                (@Submodule.setLike.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹))
              x (ℳ i))
        fun (i : ι) =>
        @AddSubmonoidClass.toAddCommMonoid.{?u.202442, ?u.202442} M inst✝²
          (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
          (@Submodule.setLike.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
          (@Submodule.addSubmonoidClass.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) (ℳ i)))
    (@DirectSum.decompose.{?u.202436, ?u.202442, ?u.202442} ι M
      (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) (fun (a b : ι) => inst✝⁴ a b) inst✝²
      (@Submodule.setLike.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
      (@Submodule.addSubmonoidClass.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) ℳ inst✝)
    (@HSMul.hSMul.{?u.202439, ?u.202442, ?u.202442} R M M
      (@instHSMul.{?u.202439, ?u.202442} R M
        (@SMulZeroClass.toSMul.{?u.202439, ?u.202442} R M
          (@AddMonoid.toZero.{?u.202442} M (@AddCommMonoid.toAddMonoid.{?u.202442} M inst✝²))
          (@SMulWithZero.toSMulZeroClass.{?u.202439, ?u.202442} R M
            (@MonoidWithZero.toZero.{?u.202439} R (@Semiring.toMonoidWithZero.{?u.202439} R inst✝³))
            (@AddMonoid.toZero.{?u.202442} M (@AddCommMonoid.toAddMonoid.{?u.202442} M inst✝²))
            (@MulActionWithZero.toSMulWithZero.{?u.202439, ?u.202442} R M
              (@Semiring.toMonoidWithZero.{?u.202439} R inst✝³)
              (@AddMonoid.toZero.{?u.202442} M (@AddCommMonoid.toAddMonoid.{?u.202442} M inst✝²))
              (@Module.toMulActionWithZero.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)))))
      r x)
has type
  (fun (x : M) =>
      @DirectSum.{?u.202436, ?u.202442} ι
        (fun (i : ι) =>
          @Subtype.{?u.202442 + 1} M fun (x : M) =>
            @Membership.mem.{?u.202442, ?u.202442} M (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
              (@SetLike.instMembership.{?u.202442, ?u.202442}
                (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) M
                (@Submodule.setLike.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹))
              x (ℳ i))
        fun (i : ι) =>
        @AddSubmonoidClass.toAddCommMonoid.{?u.202442, ?u.202442} M inst✝²
          (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
          (@Submodule.setLike.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
          (@Submodule.addSubmonoidClass.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) (ℳ i))
    (@HSMul.hSMul.{?u.202439, ?u.202442, ?u.202442} R M M
      (@instHSMul.{?u.202439, ?u.202442} R M
        (@SMulZeroClass.toSMul.{?u.202439, ?u.202442} R M
          (@AddMonoid.toZero.{?u.202442} M (@AddCommMonoid.toAddMonoid.{?u.202442} M inst✝²))
          (@SMulWithZero.toSMulZeroClass.{?u.202439, ?u.202442} R M
            (@MonoidWithZero.toZero.{?u.202439} R (@Semiring.toMonoidWithZero.{?u.202439} R inst✝³))
            (@AddMonoid.toZero.{?u.202442} M (@AddCommMonoid.toAddMonoid.{?u.202442} M inst✝²))
            (@MulActionWithZero.toSMulWithZero.{?u.202439, ?u.202442} R M
              (@Semiring.toMonoidWithZero.{?u.202439} R inst✝³)
              (@AddMonoid.toZero.{?u.202442} M (@AddCommMonoid.toAddMonoid.{?u.202442} M inst✝²))
              (@Module.toMulActionWithZero.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)))))
      r x) : Type (max ?u.202442 ?u.202436)
but is expected to have type
  (fun (x : M) =>
      @DirectSum.{?u.202436, ?u.202442} ι
        (fun (i : ι) =>
          @Subtype.{?u.202442 + 1} M fun (x : M) =>
            @Membership.mem.{?u.202442, ?u.202442} M (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
              (@SetLike.instMembership.{?u.202442, ?u.202442}
                (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) M
                (@Submodule.setLike.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹))
              x (ℳ i))
        fun (i : ι) =>
        @AddSubmonoidClass.toAddCommMonoid.{?u.202442, ?u.202442} M inst✝²
          (@Submodule.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
          (@Submodule.setLike.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)
          (@Submodule.addSubmonoidClass.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹) (ℳ i))
    (@HSMul.hSMul.{?u.202439, ?u.202442, ?u.202442} R M M
      (@instHSMul.{?u.202439, ?u.202442} R M
        (@SMulZeroClass.toSMul.{?u.202439, ?u.202442} R M
          (@AddMonoid.toZero.{?u.202442} M (@AddCommMonoid.toAddMonoid.{?u.202442} M inst✝²))
          (@SMulWithZero.toSMulZeroClass.{?u.202439, ?u.202442} R M
            (@MonoidWithZero.toZero.{?u.202439} R (@Semiring.toMonoidWithZero.{?u.202439} R inst✝³))
            (@AddMonoid.toZero.{?u.202442} M (@AddCommMonoid.toAddMonoid.{?u.202442} M inst✝²))
            (@MulActionWithZero.toSMulWithZero.{?u.202439, ?u.202442} R M
              (@Semiring.toMonoidWithZero.{?u.202439} R inst✝³)
              (@AddMonoid.toZero.{?u.202442} M (@AddCommMonoid.toAddMonoid.{?u.202442} M inst✝²))
              (@Module.toMulActionWithZero.{?u.202439, ?u.202442} R M inst✝³ inst✝² inst✝¹)))))
      r x) : Type (max ?u.202442 ?u.202436)

[Xavier Roblot]

I fail to see a difference between the type and the expected type (but I guess it is easy to miss if it is a small one).

[Eric Wieser]

Those types are identical according to my diff tool

[Matthew Ballard]

Is this one timing out also?

[Xavier Roblot]

Yes, there is another error for this line:

failed to synthesize
  HSMul R ((fun x => DirectSum ι fun i => { x // x ∈ ℳ i }) x) ?m.204299
(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)