!4#4707 Algebra.Module.PID

Stream: PR reviews

[Ruben Van de Velde]

How could I not share this...

failed to synthesize instance
  Module
    ((AddMonoid.End N ×
        AddMonoid.End N ×
          AddMonoid.End N ×
            AddMonoid.End N ×
              AddMonoid.End N ×
                AddMonoid.End N ×
                  AddMonoid.End N ×
                    AddMonoid.End N ×
                      AddMonoid.End N ×
                        AddMonoid.End N ×
                          AddMonoid.End N ×
                            AddMonoid.End N ×
                              AddMonoid.End N ×
                                AddMonoid.End N ×
                                  AddMonoid.End N ×
                                    AddMonoid.End N ×
                                      AddMonoid.End N ×
                                        AddMonoid.End N ×
                                          AddMonoid.End N ×
                                            AddMonoid.End N ×
                                              AddMonoid.End N ×
                                                AddMonoid.End N ×
                                                  AddMonoid.End N ×
                                                    AddMonoid.End N ×
                                                      AddMonoid.End N ×
                                                        AddMonoid.End N ×
                                                          AddMonoid.End N ×
                                                            AddMonoid.End N ×
                                                              AddMonoid.End N ×
                                                                AddMonoid.End N ×
                                                                  AddMonoid.End N ×
                                                                    AddMonoid.End N ×
                                                                      AddMonoid.End N ×
                                                                        AddMonoid.End N ×
                                                                          AddMonoid.End N ×
                                                                            AddMonoid.End N ×
                                                                              AddMonoid.End N ×
                                                                                AddMonoid.End N ×
                                                                                  AddMonoid.End N ×
                                                                                    AddMonoid.End N ×
                                                                                      AddMonoid.End N ×
                                                                                        AddMonoid.End N) ×
      AddMonoid.End N)
    N

[Kevin Buzzard]

Yeah I've seen something like this before, but this was before lean4#2210 . How did it happen? User error or is it the typeclass system going wrong?

[Ruben Van de Velde]

This is the code:

      refine'
        ⟨_,
          ⟨(((@lequivProdOfRightSplitExact _ _ _ _ _ _ _ _ _ _ _ _
                            ((f.trans ULift.moduleEquiv.{u, u, v}.symm).toLinearMap.comp <| mkQ _)
                            ((DirectSum.toModule _ _ _ fun i =>
                                  (liftQSpanSingleton.{u, u} (p ^ k i)
                                      (LinearMap.toSpanSingleton _ _ _) (this i).choose_spec.left :
                                    R ⧸ _ →ₗ[R] _)).comp
                              ULift.moduleEquiv.toLinearMap)
                            (R ∙ s j).injective_subtype _ _).symm.trans <|
                      ((quotTorsionOfEquivSpanSingleton _ _ _).symm.trans <|
                            quotEquivOfEqBot _ _ <|
                              Ideal.torsionOf_eq_span_pow_pOrder hp hN _).prod <|
                        ULift.moduleEquiv).trans <|
                  (@DirectSum.lequivProdDirectSum R _ _ _
                      (fun i => R ⧸ R ∙ p ^ @Option.rec _ (fun _ => ℕ) (pOrder hN <| s j) k i) _
                      _).symm).trans <|
              DirectSum.lequivCongrLeft R (finSuccEquiv d).symm⟩⟩

[Ruben Van de Velde]

Your guess is as good as mine (probably better)

[Kevin Buzzard]

All those trans and comps make me think that calc mode could be useful, however I failed to get it working with linear isos before and I'm not sure there's an easy fix :-/

[Ruben Van de Velde]

In any case, I'm stepping away from this file for a while, in case someone wants to look into it

[Mario Carneiro]

also reminds me of:
the-end.jpg