Zulip Chat Archive

Stream: mathlib4

Topic: Synthesis failure for LinearEquiv.funUnique

Eric Wieser (Jan 09 2025 at 14:53):

I was rather surprised to see that this times out:

import Mathlib

set_option synthInstance.maxHeartbeats 100000
set_option maxSynthPendingDepth 3 in
example {๐•œ} [RCLike ๐•œ] := LinearEquiv.funUnique Unit ๐•œ ๐•œ

(docs#LinearEquiv.funUnique)

Kevin Buzzard (Jan 09 2025 at 15:07):

example {๐•œ : Type*} [RCLike ๐•œ] := LinearEquiv.funUnique Unit ๐•œ ๐•œ

is immediate

Kevin Buzzard (Jan 09 2025 at 15:14):

import Mathlib

set_option synthInstance.maxHeartbeats 0
set_option maxHeartbeats 0
set_option trace.profiler true
set_option trace.Meta.synthInstance true
example {๐•œ} [RCLike ๐•œ] := LinearEquiv.funUnique Unit ๐•œ ๐•œ

does work eventually:

[Elab.command] [14.435839] example {๐•œ} [RCLike ๐•œ] :=
      LinearEquiv.funUnique Unit ๐•œ ๐•œ โ–ผ
  [step] [14.323702] expected type: (Unit โ†’ ๐•œ) โ‰ƒโ‚—[๐•œ] ๐•œ, term
    LinearEquiv.funUnique Unit ๐•œ ๐•œ โ–ผ
  [Meta.synthInstance] [0.000261] โœ…๏ธ Unique Unit โ–ถ
  [Meta.synthInstance] [0.003494] โœ…๏ธ Semiring ๐•œ โ–ถ
  [Meta.synthInstance] [14.314824] โœ…๏ธ AddCommMonoid ๐•œ โ–ผ
  [] [0.000025] new goal AddCommMonoid ๐•œ โ–ถ
  [] [0.000128] โœ…๏ธ apply @OrderedAddCommMonoid.toAddCommMonoid to AddCommMonoid ๐•œ โ–ถ
  [] [0.000141] โœ…๏ธ apply @OrderedSemiring.toOrderedAddCommMonoid to OrderedAddCommMonoid ๐•œ โ–ถ
  [] [0.000139] โœ…๏ธ apply @OrderedCommSemiring.toOrderedSemiring to OrderedSemiring ๐•œ โ–ถ
  [] [0.000131] โœ…๏ธ apply @CanonicallyOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring ๐•œ โ–ถ
  [] [0.000122] โœ…๏ธ apply @CanonicallyLinearOrderedSemifield.toCanonicallyOrderedCommSemiring to CanonicallyOrderedCommSemiring
      ๐•œ โ–ถ
  [] [0.000113] โœ…๏ธ apply @StrictOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring ๐•œ โ–ถ
  [] [0.000125] โœ…๏ธ apply @LinearOrderedCommSemiring.toStrictOrderedCommSemiring to StrictOrderedCommSemiring ๐•œ โ–ถ
  [] [0.000124] โœ…๏ธ apply @LinearOrderedSemifield.toLinearOrderedCommSemiring to LinearOrderedCommSemiring ๐•œ โ–ถ
  [] [0.000111] โœ…๏ธ apply @CanonicallyLinearOrderedSemifield.toLinearOrderedSemifield to LinearOrderedSemifield ๐•œ โ–ถ
  [] [0.000109] โœ…๏ธ apply @LinearOrderedField.toLinearOrderedSemifield to LinearOrderedSemifield ๐•œ โ–ถ
  [] [0.000111] โœ…๏ธ apply @ConditionallyCompleteLinearOrderedField.toLinearOrderedField to LinearOrderedField ๐•œ โ–ถ
  [] [0.000115] โœ…๏ธ apply @NormedLinearOrderedField.toLinearOrderedField to LinearOrderedField ๐•œ โ–ถ
  [] [0.000129] โœ…๏ธ apply @LinearOrderedCommRing.toLinearOrderedCommSemiring to LinearOrderedCommSemiring ๐•œ โ–ถ
  [] [0.000117] โœ…๏ธ apply @LinearOrderedField.toLinearOrderedCommRing to LinearOrderedCommRing ๐•œ โ–ถ
  [] [0.000140] โœ…๏ธ apply @StrictOrderedCommRing.toStrictOrderedCommSemiring to StrictOrderedCommSemiring ๐•œ โ–ถ
  [] [0.000156] โœ…๏ธ apply @LinearOrderedCommRing.toStrictOrderedCommRing to StrictOrderedCommRing ๐•œ โ–ถ
  [] [0.000169] โœ…๏ธ apply @OrderedCommRing.toOrderedCommSemiring to OrderedCommSemiring ๐•œ โ–ถ
  [] [0.000116] โœ…๏ธ apply @StrictOrderedCommRing.toOrderedCommRing to OrderedCommRing ๐•œ โ–ถ
  [] [0.000134] โœ…๏ธ apply @StrictOrderedSemiring.toOrderedSemiring to OrderedSemiring ๐•œ โ–ถ
  [] [0.000195] โœ…๏ธ apply @LinearOrderedSemiring.toStrictOrderedSemiring to StrictOrderedSemiring ๐•œ โ–ถ
  [] [0.000167] โœ…๏ธ apply @LinearOrderedCommSemiring.toLinearOrderedSemiring to LinearOrderedSemiring ๐•œ โ–ถ
  [] [0.000173] โœ…๏ธ apply @LinearOrderedRing.toLinearOrderedSemiring to LinearOrderedSemiring ๐•œ โ–ถ
  [] [0.000189] โœ…๏ธ apply @LinearOrderedCommRing.toLinearOrderedRing to LinearOrderedRing ๐•œ โ–ถ
  [] [0.000166] โœ…๏ธ apply @StrictOrderedCommSemiring.toStrictOrderedSemiring to StrictOrderedSemiring ๐•œ โ–ถ
  [] [0.000172] โœ…๏ธ apply @StrictOrderedRing.toStrictOrderedSemiring to StrictOrderedSemiring ๐•œ โ–ถ
  [] [0.000147] โœ…๏ธ apply @LinearOrderedRing.toStrictOrderedRing to StrictOrderedRing ๐•œ โ–ถ
  [] [0.000143] โœ…๏ธ apply @StrictOrderedCommRing.toStrictOrderedRing to StrictOrderedRing ๐•œ โ–ถ
  [] [0.000117] โœ…๏ธ apply @OrderedRing.toOrderedSemiring to OrderedSemiring ๐•œ โ–ถ
  [] [0.000115] โœ…๏ธ apply @OrderedCommRing.toOrderedRing to OrderedRing ๐•œ โ–ถ
  [] [0.000094] โœ…๏ธ apply @StrictOrderedRing.toOrderedRing to OrderedRing ๐•œ โ–ถ
  [] [0.000123] โœ…๏ธ apply @CanonicallyOrderedAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ๐•œ โ–ถ
  [] [0.000109] โœ…๏ธ apply @CanonicallyOrderedCommSemiring.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid
      ๐•œ โ–ถ
  [] [0.000113] โœ…๏ธ apply @CanonicallyLinearOrderedAddCommMonoid.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid
      ๐•œ โ–ถ
  [] [0.000122] โœ…๏ธ apply @CanonicallyLinearOrderedSemifield.toCanonicallyLinearOrderedAddCommMonoid to CanonicallyLinearOrderedAddCommMonoid
      ๐•œ โ–ถ
  [] [0.000112] โœ…๏ธ apply @IdemSemiring.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid ๐•œ โ–ถ
  [] [0.000117] โœ…๏ธ apply @KleeneAlgebra.toIdemSemiring to IdemSemiring ๐•œ โ–ถ
  [] [0.000114] โœ…๏ธ apply @IdemCommSemiring.toIdemSemiring to IdemSemiring ๐•œ โ–ถ
  [] [0.000126] โœ…๏ธ apply @LinearOrderedAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ๐•œ โ–ถ
  [] [0.000111] โœ…๏ธ apply @LinearOrderedSemiring.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ๐•œ โ–ถ
  [] [0.000117] โœ…๏ธ apply @LinearOrderedAddCommMonoidWithTop.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ๐•œ โ–ถ
  [] [0.000128] โœ…๏ธ apply @LinearOrderedAddCommGroupWithTop.toLinearOrderedAddCommMonoidWithTop to LinearOrderedAddCommMonoidWithTop
      ๐•œ โ–ถ
  [] [0.000097] โœ…๏ธ apply @CanonicallyLinearOrderedAddCommMonoid.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ๐•œ โ–ถ
  [] [0.000116] โœ…๏ธ apply @LinearOrderedCancelAddCommMonoid.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ๐•œ โ–ถ
  [] [0.000112] โœ…๏ธ apply @LinearOrderedSemiring.toLinearOrderedCancelAddCommMonoid to LinearOrderedCancelAddCommMonoid ๐•œ โ–ถ
  [] [0.000115] โœ…๏ธ apply @LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid to LinearOrderedCancelAddCommMonoid ๐•œ โ–ถ
  [] [0.000120] โœ…๏ธ apply @NormedLinearOrderedAddGroup.toLinearOrderedAddCommGroup to LinearOrderedAddCommGroup ๐•œ โ–ถ
  [] [0.000097] โœ…๏ธ apply @LinearOrderedRing.toLinearOrderedAddCommGroup to LinearOrderedAddCommGroup ๐•œ โ–ถ
  [] [0.000116] โœ…๏ธ apply @OrderedCancelAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ๐•œ โ–ถ
  [] [0.000106] โœ…๏ธ apply @StrictOrderedSemiring.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid ๐•œ โ–ถ
  [] 4453 more entries... โ–ถ
  [Meta.synthInstance] [0.003447] โœ…๏ธ Module ๐•œ ๐•œ โ–ถ
  [def.processPreDef] [0.016145] process pre-definitions โ–ถ

Congratulations on 4453 more entries, I think that might be a new record.

Kevin Buzzard (Jan 09 2025 at 15:20):

The 5 megabyte trace can be viewed in full here.

Matthew Ballard (Jan 09 2025 at 15:20):

If I multiply out 0.0001 by 5000, then I am still pretty far off from 14

Kevin Buzzard (Jan 09 2025 at 15:29):

It occasionally goes completely off the rails and costs far more time. For example once we're into topological ring territory all kinds of fun can happen:

        [Meta.synthInstance.answer] [0.000017] โœ…๏ธ TopologicalRing ๐•œ
      [Meta.synthInstance.resume] [0.000034] propagating TopologicalRing ๐•œ to subgoal TopologicalRing ๐•œ of Finite ๐•œ
        [Meta.synthInstance.resume] size: 16
        [Meta.synthInstance] [0.000022] new goal CompactSpace ๐•œ
          [Meta.synthInstance.instances] #[@Subsingleton.compactSpace, @Finite.compactSpace, @compactSpace_of_completeLinearOrder, TopologicalSpace.NoetherianSpace.compactSpace]
      [Meta.synthInstance] [0.000284] โœ…๏ธ apply TopologicalSpace.NoetherianSpace.compactSpace to CompactSpace ๐•œ
        [Meta.synthInstance.tryResolve] [0.000156] โœ…๏ธ CompactSpace ๐•œ โ‰Ÿ CompactSpace ๐•œ
        [Meta.synthInstance] [0.000093] new goal TopologicalSpace.NoetherianSpace ๐•œ
          [Meta.synthInstance.instances] #[@Finite.to_wellFoundedGT, @TopologicalSpace.Finite.to_noetherianSpace, @IsWellOrder.toIsWellFounded, @instWellFoundedGTOfGradeOrderOrderDualNat]
      [Meta.synthInstance] [0.004712] โœ…๏ธ apply @instWellFoundedGTOfGradeOrderOrderDualNat to TopologicalSpace.NoetherianSpace
            ๐•œ
        [Meta.synthInstance.tryResolve] [0.004581] โœ…๏ธ TopologicalSpace.NoetherianSpace
              ๐•œ โ‰Ÿ IsWellFounded (TopologicalSpace.Opens ๐•œ) fun x1 x2 โ†ฆ x1 > x2
          [Meta.synthInstance] [0.001415] โœ…๏ธ Preorder (TopologicalSpace.Opens ๐•œ)
            [Meta.synthInstance] [0.000021] new goal Preorder (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance.instances] #[@PartialOrder.toPreorder]
            [Meta.synthInstance] [0.000143] โœ…๏ธ apply @PartialOrder.toPreorder to Preorder (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance.tryResolve] [0.000082] โœ…๏ธ Preorder
                    (TopologicalSpace.Opens ๐•œ) โ‰Ÿ Preorder (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance] [0.000026] new goal PartialOrder (TopologicalSpace.Opens ๐•œ)
                [Meta.synthInstance.instances] #[@SetLike.instPartialOrder, @LinearOrder.toPartialOrder, @SemilatticeSup.toPartialOrder, @SemilatticeInf.toPartialOrder, @OrderedAddCommMonoid.toPartialOrder, @OrderedCommMonoid.toPartialOrder, @OrderedAddCommGroup.toPartialOrder, @OrderedCommGroup.toPartialOrder, @CompleteSemilatticeSup.toPartialOrder, @CompleteSemilatticeInf.toPartialOrder, @OmegaCompletePartialOrder.toPartialOrder, @CompletePartialOrder.toPartialOrder]
            [Meta.synthInstance] [0.000146] โœ…๏ธ apply @CompletePartialOrder.toPartialOrder to PartialOrder
                  (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance.tryResolve] [0.000099] โœ…๏ธ PartialOrder
                    (TopologicalSpace.Opens ๐•œ) โ‰Ÿ PartialOrder (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance] [0.000013] new goal CompletePartialOrder (TopologicalSpace.Opens ๐•œ)
                [Meta.synthInstance.instances] #[@CompleteLattice.toCompletePartialOrder]
            [Meta.synthInstance] [0.000155] โœ…๏ธ apply @CompleteLattice.toCompletePartialOrder to CompletePartialOrder
                  (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance.tryResolve] [0.000096] โœ…๏ธ CompletePartialOrder
                    (TopologicalSpace.Opens ๐•œ) โ‰Ÿ CompletePartialOrder (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance] [0.000031] new goal CompleteLattice (TopologicalSpace.Opens ๐•œ)
                [Meta.synthInstance.instances] #[@CompleteLinearOrder.toCompleteLattice, @Order.Frame.MinimalAxioms.toCompleteLattice, @Order.Coframe.MinimalAxioms.toCompleteLattice, @Order.Frame.toCompleteLattice, @Order.Coframe.toCompleteLattice, @CompletelyDistribLattice.toCompleteLattice, @CompleteBooleanAlgebra.toCompleteLattice, @CompleteAtomicBooleanAlgebra.toCompleteLattice, @TopologicalSpace.Opens.instCompleteLattice]
            [Meta.synthInstance] [0.000468] โœ…๏ธ apply @TopologicalSpace.Opens.instCompleteLattice to CompleteLattice
                  (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance.tryResolve] [0.000169] โœ…๏ธ CompleteLattice
                    (TopologicalSpace.Opens ๐•œ) โ‰Ÿ CompleteLattice (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance.answer] [0.000011] โœ…๏ธ CompleteLattice (TopologicalSpace.Opens ๐•œ)
            [Meta.synthInstance.resume] [0.000024] propagating CompleteLattice
                  (TopologicalSpace.Opens
                    ๐•œ) to subgoal CompleteLattice
                  (TopologicalSpace.Opens ๐•œ) of CompletePartialOrder (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance.resume] size: 1
              [Meta.synthInstance.answer] [0.000014] โœ…๏ธ CompletePartialOrder (TopologicalSpace.Opens ๐•œ)
            [Meta.synthInstance.resume] [0.000025] propagating CompletePartialOrder
                  (TopologicalSpace.Opens
                    ๐•œ) to subgoal CompletePartialOrder
                  (TopologicalSpace.Opens ๐•œ) of PartialOrder (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance.resume] size: 2
              [Meta.synthInstance.answer] [0.000019] โœ…๏ธ PartialOrder (TopologicalSpace.Opens ๐•œ)
            [Meta.synthInstance.resume] [0.000032] propagating PartialOrder
                  (TopologicalSpace.Opens
                    ๐•œ) to subgoal PartialOrder (TopologicalSpace.Opens ๐•œ) of Preorder (TopologicalSpace.Opens ๐•œ)
              [Meta.synthInstance.resume] size: 3
              [Meta.synthInstance.answer] [0.000027] โœ…๏ธ Preorder (TopologicalSpace.Opens ๐•œ)
            [Meta.synthInstance] result PartialOrder.toPreorder
        [Meta.synthInstance] [0.000049] new goal GradeOrder โ„•แต’แตˆ (TopologicalSpace.Opens ๐•œ)
          [Meta.synthInstance.instances] #[@GradeMinOrder.toGradeOrder, @GradeMaxOrder.toGradeOrder]
      [Meta.synthInstance] [0.000659] โœ…๏ธ apply @GradeMaxOrder.toGradeOrder to GradeOrder โ„•แต’แตˆ (TopologicalSpace.Opens ๐•œ)
        [Meta.synthInstance.tryResolve] [0.000560] โœ…๏ธ GradeOrder โ„•แต’แตˆ
              (TopologicalSpace.Opens ๐•œ) โ‰Ÿ GradeOrder โ„•แต’แตˆ (TopologicalSpace.Opens ๐•œ)
        [Meta.synthInstance] [0.000033] new goal GradeMaxOrder โ„•แต’แตˆ (TopologicalSpace.Opens ๐•œ)
          [Meta.synthInstance.instances] #[@GradeBoundedOrder.toGradeMaxOrder]
      [Meta.synthInstance] [0.000425] โœ…๏ธ apply @GradeBoundedOrder.toGradeMaxOrder to GradeMaxOrder โ„•แต’แตˆ
            (TopologicalSpace.Opens ๐•œ)
        [Meta.synthInstance.tryResolve] [0.000329] โœ…๏ธ GradeMaxOrder โ„•แต’แตˆ
              (TopologicalSpace.Opens ๐•œ) โ‰Ÿ GradeMaxOrder โ„•แต’แตˆ (TopologicalSpace.Opens ๐•œ)
        [Meta.synthInstance] [0.000033] new goal GradeBoundedOrder โ„•แต’แตˆ (TopologicalSpace.Opens ๐•œ)
          [Meta.synthInstance.instances] #[@Preorder.toGradeBoundedOrder]
      [Meta.synthInstance] [0.000161] โŒ๏ธ apply @Preorder.toGradeBoundedOrder to GradeBoundedOrder โ„•แต’แตˆ
            (TopologicalSpace.Opens ๐•œ)
        [Meta.synthInstance.tryResolve] [0.000135] โŒ๏ธ GradeBoundedOrder โ„•แต’แตˆ
              (TopologicalSpace.Opens ๐•œ) โ‰Ÿ GradeBoundedOrder ?m.1408 ?m.1408
      [Meta.synthInstance] [0.000405] โœ…๏ธ apply @GradeMinOrder.toGradeOrder to GradeOrder โ„•แต’แตˆ (TopologicalSpace.Opens ๐•œ)
        [Meta.synthInstance.tryResolve] [0.000300] โœ…๏ธ GradeOrder โ„•แต’แตˆ
              (TopologicalSpace.Opens ๐•œ) โ‰Ÿ GradeOrder โ„•แต’แตˆ (TopologicalSpace.Opens ๐•œ)
        [Meta.synthInstance] [0.000037] new goal GradeMinOrder โ„•แต’แตˆ (TopologicalSpace.Opens ๐•œ)
          [Meta.synthInstance.instances] #[@GradeBoundedOrder.toGradeMinOrder]
      [Meta.synthInstance] [0.000426] โœ…๏ธ apply @GradeBoundedOrder.toGradeMinOrder to GradeMinOrder โ„•แต’แตˆ
            (TopologicalSpace.Opens ๐•œ)
        [Meta.synthInstance.tryResolve] [0.000366] โœ…๏ธ GradeMinOrder โ„•แต’แตˆ
              (TopologicalSpace.Opens ๐•œ) โ‰Ÿ GradeMinOrder โ„•แต’แตˆ (TopologicalSpace.Opens ๐•œ)
      [Meta.synthInstance] [0.001292] โœ…๏ธ apply @IsWellOrder.toIsWellFounded to TopologicalSpace.NoetherianSpace ๐•œ
        [Meta.synthInstance.tryResolve] [0.001158] โœ…๏ธ TopologicalSpace.NoetherianSpace
              ๐•œ โ‰Ÿ IsWellFounded (TopologicalSpace.Opens ๐•œ) fun x1 x2 โ†ฆ x1 > x2
        [Meta.synthInstance] [0.000035] new goal IsWellOrder (TopologicalSpace.Opens ๐•œ) fun x1 x2 โ†ฆ x1 > x2
          [Meta.synthInstance.instances] #[@instIsWellOrderOfIsEmpty, @isWellOrder_gt]
      [Meta.synthInstance] [0.013369] โŒ๏ธ apply @isWellOrder_gt to IsWellOrder (TopologicalSpace.Opens ๐•œ) fun x1 x2 โ†ฆ
            x1 > x2
        [Meta.synthInstance.tryResolve] [0.013117] โŒ๏ธ IsWellOrder (TopologicalSpace.Opens ๐•œ) fun x1 x2 โ†ฆ
              x1 > x2 โ‰Ÿ IsWellOrder ?m.1445 fun x1 x2 โ†ฆ x1 > x2
          [Meta.isDefEq] [0.013058] โŒ๏ธ IsWellOrder (TopologicalSpace.Opens ๐•œ) fun x1 x2 โ†ฆ
                x1 > x2 =?= IsWellOrder ?m.1445 fun x1 x2 โ†ฆ x1 > x2
            [Meta.isDefEq] [0.012971] โŒ๏ธ fun x1 x2 โ†ฆ x1 > x2 =?= fun x1 x2 โ†ฆ x1 > x2
              [Meta.isDefEq] [0.012953] โŒ๏ธ x1โœ > x2โœ =?= x1โœ > x2โœ
                [Meta.synthInstance] [0.005772] โŒ๏ธ LinearOrder (TopologicalSpace.Opens ๐•œ)
                  [Meta.synthInstance] [0.000030] new goal LinearOrder (TopologicalSpace.Opens ๐•œ)
                    [Meta.synthInstance.instances] #[@LinearOrderedAddCommMonoid.toLinearOrder, @LinearOrderedCommMonoid.toLinearOrder, @LinearOrderedAddCommGroup.toLinearOrder, @LinearOrderedCommGroup.toLinearOrder, @LinearOrderedRing.toLinearOrder, @CompleteLinearOrder.toLinearOrder, @ConditionallyCompleteLinearOrder.toLinearOrder, @NonemptyFiniteLinearOrder.toLinearOrder]
                  [Meta.synthInstance] [0.000144] โœ…๏ธ apply @NonemptyFiniteLinearOrder.toLinearOrder to LinearOrder
                        (TopologicalSpace.Opens ๐•œ)
                    [Meta.synthInstance.tryResolve] [0.000091] โœ…๏ธ LinearOrder
                          (TopologicalSpace.Opens ๐•œ) โ‰Ÿ LinearOrder (TopologicalSpace.Opens ๐•œ)

Kevin Buzzard (Jan 09 2025 at 15:30):

(I could have just quoted the last 15 lines but it was fun to see how it got there)

Kevin Buzzard (Jan 09 2025 at 15:31):

(This is @Andrew Yang 's new instance that a compact topological ring is finite btw, a result I didn't know before and which has a really nice proof)

Kevin Buzzard (Jan 09 2025 at 15:45):

So with timings turned off, the traces are here (over 10000 lines) for {๐•œ} and here (880 lines) for {๐•œ : Type*}. They're identical up until line 686, where for some reason the short one starts working on OrderedAddCommGroup ๐•œ and the long one starts working on NormedField ๐•œ. I find it then difficult to unify them from that point on, but note that we're about 3/4 of the way through the short proof at that point.

Eric Wieser (Jan 09 2025 at 15:57):

Maybe example {๐•œ} [RCLike ๐•œ] : AddCommMonoid ๐•œ := inferInstance is a better test

Last updated: May 02 2025 at 03:31 UTC