AutomorphicForm/QuaternionAlgebra/Defs is slow

[kbuzzard]

This is not a deal breaker yet but the file FLT/AutomorphicForm/QuaternionAlgebra/Defs.lean compiles quite slowly, and I suspect it's one of those things where if you investigate carefully enough you'll be able to make it much faster. Right now it's full of traces like this (and those 0.1 seconds add up when there are loads of them):

[tryResolve] [0.094204] ✅️ IsScalarTower F (FiniteAdeleRing (𝓞 F) F)
      (FiniteAdeleRing (𝓞 F) F) ≟ IsScalarTower F (FiniteAdeleRing (𝓞 F) F) (FiniteAdeleRing (𝓞 F) F) ▼
  [isDefEq] [0.089920] ✅️ IsScalarTower F (FiniteAdeleRing (𝓞 F) F)
        (FiniteAdeleRing (𝓞 F) F) =?= IsScalarTower ?m.35388 ?m.35389 ?m.35389 ▼
    [synthInstance] [0.085261] ✅️ Algebra F (FiniteAdeleRing (𝓞 F) F) ▼
      [] [0.083833] ✅️ apply FiniteAdeleRing.instAlgebra to Algebra F (FiniteAdeleRing (𝓞 F) F) ▼
        [tryResolve] [0.083706] ✅️ Algebra F (FiniteAdeleRing (𝓞 F) F) ≟ Algebra F (FiniteAdeleRing (𝓞 F) F) ▼
          [isDefEq] [0.044065] ✅️ Algebra F (FiniteAdeleRing (𝓞 F) F) =?= Algebra ?m.35418 (FiniteAdeleRing ?m.35415 ?m.35418) ▼
            [] [0.041087] ✅️ CommSemiring.toSemiring =?= CommSemiring.toSemiring ▼
              [] [0.041081] ✅️ CommSemiring.toSemiring =?= CommSemiring.toSemiring ▼
                [] [0.041044] ✅️ CommRing.toCommSemiring.1 =?= CommRing.toCommSemiring.1 ▼
                  [] [0.041010] ✅️ Ring.toSemiring =?= Ring.toSemiring ▼
                    [] [0.041001] ✅️ CommRing.toRing.1 =?= CommRing.toRing.1 ▼
                      [] [0.040806] ✅️ Function.Injective.semiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
                            ⋯ =?= Function.Injective.semiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ▼
                        [] [0.040776] ✅️ let __spread.0 := Function.Injective.nonAssocSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯;
                            let __spread.1 := Function.Injective.monoidWithZero (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯;
                            let __NonUnitalSemiring :=
                              Function.Injective.nonUnitalSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯;
                            { toNonUnitalSemiring := __NonUnitalSemiring, toOne := NonAssocSemiring.toOne,
                              one_mul := ⋯, mul_one := ⋯, toNatCast := NonAssocSemiring.toNatCast,
                              natCast_zero := ⋯, natCast_succ := ⋯, npow := Monoid.npow, npow_zero := ⋯,
                              npow_succ :=
                                ⋯ } =?= let __spread.0 :=
                              Function.Injective.nonAssocSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯;
                            let __spread.1 := Function.Injective.monoidWithZero (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯;
                            let __NonUnitalSemiring :=
                              Function.Injective.nonUnitalSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯;
                            { toNonUnitalSemiring := __NonUnitalSemiring, toOne := NonAssocSemiring.toOne,
                              one_mul := ⋯, mul_one := ⋯, toNatCast := NonAssocSemiring.toNatCast,
                              natCast_zero := ⋯, natCast_succ := ⋯, npow := Monoid.npow, npow_zero := ⋯,
                              npow_succ := ⋯ } ▼
                          [] [0.040764] ✅️ { toNonUnitalSemiring := Function.Injective.nonUnitalSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯,
                                toOne := NonAssocSemiring.toOne, one_mul := ⋯, mul_one := ⋯,
                                toNatCast := NonAssocSemiring.toNatCast, natCast_zero := ⋯,
                                natCast_succ := ⋯, npow := Monoid.npow, npow_zero := ⋯,
                                npow_succ :=
                                  ⋯ } =?= {
                                toNonUnitalSemiring :=
                                  Function.Injective.nonUnitalSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯,
                                toOne := NonAssocSemiring.toOne, one_mul := ⋯, mul_one := ⋯,
                                toNatCast := NonAssocSemiring.toNatCast, natCast_zero := ⋯,
                                natCast_succ := ⋯, npow := Monoid.npow, npow_zero := ⋯, npow_succ := ⋯ } ▼
                            [] [0.022591] ✅️ Function.Injective.nonUnitalSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯
                                  ⋯ =?= Function.Injective.nonUnitalSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ▼
                              [] [0.022571] ✅️ let __spread.0 := Function.Injective.semigroupWithZero (fun f ↦ ⇑f) ⋯ ⋯ ⋯;
                                  let __NonUnitalNonAssocSemiring :=
                                    Function.Injective.nonUnitalNonAssocSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯;
                                  { toNonUnitalNonAssocSemiring := __NonUnitalNonAssocSemiring,
                                    mul_assoc :=
                                      ⋯ } =?= let __spread.0 :=
                                    Function.Injective.semigroupWithZero (fun f ↦ ⇑f) ⋯ ⋯ ⋯;
                                  let __NonUnitalNonAssocSemiring :=
                                    Function.Injective.nonUnitalNonAssocSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯;
                                  { toNonUnitalNonAssocSemiring := __NonUnitalNonAssocSemiring,
                                    mul_assoc := ⋯ } ▼
                                [] [0.022566] ✅️ { toNonUnitalNonAssocSemiring := Function.Injective.nonUnitalNonAssocSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯,
                                      mul_assoc :=
                                        ⋯ } =?= {
                                      toNonUnitalNonAssocSemiring :=
                                        Function.Injective.nonUnitalNonAssocSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯,
                                      mul_assoc := ⋯ } ▼
                                  [] [0.022515] ✅️ Function.Injective.nonUnitalNonAssocSemiring (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯
                                        ⋯ =?= Function.Injective.nonUnitalNonAssocSemiring (fun f ↦ ⇑f) ⋯ ⋯
                                        ⋯ ⋯ ⋯ ▼
                                    [] [0.022494] ✅️ let __spread.0 := Function.Injective.distrib (fun f ↦ ⇑f) ⋯ ⋯ ⋯;
                                        let __spread.1 :=
                                          Function.Injective.mulZeroClass (fun f ↦ ⇑f) ⋯ ⋯ ⋯;
                                        let __AddCommMonoid :=
                                          Function.Injective.addCommMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯;
                                        { toAddCommMonoid := __AddCommMonoid, toMul := Distrib.toMul,
                                          left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯,
                                          mul_zero :=
                                            ⋯ } =?= let __spread.0 :=
                                          Function.Injective.distrib (fun f ↦ ⇑f) ⋯ ⋯ ⋯;
                                        let __spread.1 :=
                                          Function.Injective.mulZeroClass (fun f ↦ ⇑f) ⋯ ⋯ ⋯;
                                        let __AddCommMonoid :=
                                          Function.Injective.addCommMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯;
                                        { toAddCommMonoid := __AddCommMonoid, toMul := Distrib.toMul,
                                          left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯,
                                          mul_zero := ⋯ } ▼
                                      [] [0.022485] ✅️ { toAddCommMonoid := Function.Injective.addCommMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯, toMul := Distrib.toMul,
                                            left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯,
                                            mul_zero :=
                                              ⋯ } =?= {
                                            toAddCommMonoid :=
                                              Function.Injective.addCommMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯,
                                            toMul := Distrib.toMul, left_distrib := ⋯, right_distrib := ⋯,
                                            zero_mul := ⋯, mul_zero := ⋯ } ▼
                                        [] [0.017077] ✅️ Function.Injective.addCommMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯
                                              ⋯ =?= Function.Injective.addCommMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ▼
                                          [] [0.017059] ✅️ let __src := Function.Injective.addMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯;
                                              let __src_1 :=
                                                Function.Injective.addCommSemigroup (fun f ↦ ⇑f) ⋯ ⋯;
                                              { toAddMonoid := __src,
                                                add_comm :=
                                                  ⋯ } =?= let __src :=
                                                Function.Injective.addMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯;
                                              let __src_1 :=
                                                Function.Injective.addCommSemigroup (fun f ↦ ⇑f) ⋯ ⋯;
                                              { toAddMonoid := __src, add_comm := ⋯ } ▼
                                            [] [0.017054] ✅️ { toAddMonoid := Function.Injective.addMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯,
                                                  add_comm :=
                                                    ⋯ } =?= {
                                                  toAddMonoid :=
                                                    Function.Injective.addMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯,
                                                  add_comm := ⋯ } ▼
                                              [] [0.017026] ✅️ Function.Injective.addMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ =?= Function.Injective.addMonoid (fun f ↦ ⇑f) ⋯ ⋯ ⋯ ⋯ ▼
                                                [] [0.017002] ✅️ let __src := Function.Injective.addZeroClass (fun f ↦ ⇑f) ⋯ ⋯ ⋯;
                                                    let __src_1 :=
                                                      Function.Injective.addSemigroup (fun f ↦ ⇑f) ⋯ ⋯;
                                                    { toAdd := AddZeroClass.toAdd, add_assoc := ⋯,
                                                      toZero := AddZeroClass.toZero, zero_add := ⋯,
                                                      add_zero := ⋯, nsmul := fun n x ↦ n • x,
                                                      nsmul_zero := ⋯,
                                                      nsmul_succ :=
                                                        ⋯ } =?= let __src :=
                                                      Function.Injective.addZeroClass (fun f ↦ ⇑f) ⋯ ⋯ ⋯;
                                                    let __src_1 :=
                                                      Function.Injective.addSemigroup (fun f ↦ ⇑f) ⋯ ⋯;
                                                    { toAdd := AddZeroClass.toAdd, add_assoc := ⋯,
                                                      toZero := AddZeroClass.toZero, zero_add := ⋯,
                                                      add_zero := ⋯, nsmul := fun n x ↦ n • x,
                                                      nsmul_zero := ⋯, nsmul_succ := ⋯ } ▼
                                                  [] [0.016994] ✅️ { toAdd := AddZeroClass.toAdd, add_assoc := ⋯, toZero := AddZeroClass.toZero, zero_add := ⋯,
                                                        add_zero := ⋯, nsmul := fun n x ↦ n • x,
                                                        nsmul_zero := ⋯,
                                                        nsmul_succ :=
                                                          ⋯ } =?= { toAdd := AddZeroClass.toAdd,
                                                        add_assoc := ⋯, toZero := AddZeroClass.toZero,
                                                        zero_add := ⋯, add_zero := ⋯,
                                                        nsmul := fun n x ↦ n • x, nsmul_zero := ⋯,
                                                        nsmul_succ := ⋯ } 

[kbuzzard]

The relevant definitions exposing this injective business are:

abbrev FiniteAdeleRing : Type _ :=
  Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, v.adicCompletionIntegers K]

(with Πʳ notation for RestrictedProduct) and

instance [Π i, Ring (R i)] [∀ i, SubringClass (S i) (R i)] :
    Ring (Πʳ i, [R i, B i]_[𝓕]) :=
  DFunLike.coe_injective.ring _ rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)