CharZero instance

gistfile1.txt

‘#synth CharZero ℕ’: StrictOrderedSemiring.to_charZero
‘#synth CharZero ℕ’: [Elab.command] [0.047845s] #synth CharZero ℕ
  [Meta.synthInstance] ✅ AddMonoidWithOne ℕ
    [Meta.synthInstance] new goal AddMonoidWithOne ℕ
      [Meta.synthInstance.instances] #[@AddCommMonoidWithOne.toAddMonoidWithOne, @AddGroupWithOne.toAddMonoidWithOne]
    [Meta.synthInstance] ✅ apply @AddGroupWithOne.toAddMonoidWithOne to AddMonoidWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddMonoidWithOne ℕ ≟ AddMonoidWithOne ℕ
      [Meta.synthInstance] new goal AddGroupWithOne ℕ
        [Meta.synthInstance.instances] #[@AddCommGroupWithOne.toAddGroupWithOne, @Ring.toAddGroupWithOne]
    [Meta.synthInstance] ✅ apply @Ring.toAddGroupWithOne to AddGroupWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddGroupWithOne ℕ ≟ AddGroupWithOne ℕ
      [Meta.synthInstance] new goal Ring ℕ
        [Meta.synthInstance.instances] #[@CommRing.toRing, @OrderedRing.toRing, @StrictOrderedRing.toRing, @DivisionRing.toRing]
    [Meta.synthInstance] ✅ apply @DivisionRing.toRing to Ring ℕ
      [Meta.synthInstance.tryResolve] ✅ Ring ℕ ≟ Ring ℕ
      [Meta.synthInstance] new goal DivisionRing ℕ
        [Meta.synthInstance.instances] #[@Field.toDivisionRing]
    [Meta.synthInstance] ✅ apply @Field.toDivisionRing to DivisionRing ℕ
      [Meta.synthInstance.tryResolve] ✅ DivisionRing ℕ ≟ DivisionRing ℕ
      [Meta.synthInstance] new goal Field ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedField.toField]
    [Meta.synthInstance] ✅ apply @LinearOrderedField.toField to Field ℕ
      [Meta.synthInstance.tryResolve] ✅ Field ℕ ≟ Field ℕ
      [Meta.synthInstance] no instances for LinearOrderedField ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @StrictOrderedRing.toRing to Ring ℕ
      [Meta.synthInstance.tryResolve] ✅ Ring ℕ ≟ Ring ℕ
      [Meta.synthInstance] new goal StrictOrderedRing ℕ
        [Meta.synthInstance.instances] #[@StrictOrderedCommRing.toStrictOrderedRing, @LinearOrderedRing.toStrictOrderedRing]
    [Meta.synthInstance] ✅ apply @LinearOrderedRing.toStrictOrderedRing to StrictOrderedRing ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedRing ℕ ≟ StrictOrderedRing ℕ
      [Meta.synthInstance] new goal LinearOrderedRing ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedCommRing.toLinearOrderedRing]
    [Meta.synthInstance] ✅ apply @LinearOrderedCommRing.toLinearOrderedRing to LinearOrderedRing ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedRing ℕ ≟ LinearOrderedRing ℕ
      [Meta.synthInstance] new goal LinearOrderedCommRing ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedField.toLinearOrderedCommRing]
    [Meta.synthInstance] ✅ apply @LinearOrderedField.toLinearOrderedCommRing to LinearOrderedCommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCommRing ℕ ≟ LinearOrderedCommRing ℕ
      [Meta.synthInstance] no instances for LinearOrderedField ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @StrictOrderedCommRing.toStrictOrderedRing to StrictOrderedRing ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedRing ℕ ≟ StrictOrderedRing ℕ
      [Meta.synthInstance] new goal StrictOrderedCommRing ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedCommRing.toStrictOrderedCommRing]
    [Meta.synthInstance] ✅ apply @LinearOrderedCommRing.toStrictOrderedCommRing to StrictOrderedCommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedCommRing ℕ ≟ StrictOrderedCommRing ℕ
    [Meta.synthInstance] ✅ apply @OrderedRing.toRing to Ring ℕ
      [Meta.synthInstance.tryResolve] ✅ Ring ℕ ≟ Ring ℕ
      [Meta.synthInstance] new goal OrderedRing ℕ
        [Meta.synthInstance.instances] #[@StrictOrderedRing.toOrderedRing, @OrderedCommRing.toOrderedRing]
    [Meta.synthInstance] ✅ apply @OrderedCommRing.toOrderedRing to OrderedRing ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedRing ℕ ≟ OrderedRing ℕ
      [Meta.synthInstance] new goal OrderedCommRing ℕ
        [Meta.synthInstance.instances] #[@StrictOrderedCommRing.toOrderedCommRing]
    [Meta.synthInstance] ✅ apply @StrictOrderedCommRing.toOrderedCommRing to OrderedCommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCommRing ℕ ≟ OrderedCommRing ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedRing.toOrderedRing to OrderedRing ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedRing ℕ ≟ OrderedRing ℕ
    [Meta.synthInstance] ✅ apply @CommRing.toRing to Ring ℕ
      [Meta.synthInstance.tryResolve] ✅ Ring ℕ ≟ Ring ℕ
      [Meta.synthInstance] new goal CommRing ℕ
        [Meta.synthInstance.instances] #[@OrderedCommRing.toCommRing, @StrictOrderedCommRing.toCommRing, @Field.toCommRing]
    [Meta.synthInstance] ✅ apply @Field.toCommRing to CommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ CommRing ℕ ≟ CommRing ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedCommRing.toCommRing to CommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ CommRing ℕ ≟ CommRing ℕ
    [Meta.synthInstance] ✅ apply @OrderedCommRing.toCommRing to CommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ CommRing ℕ ≟ CommRing ℕ
    [Meta.synthInstance] ✅ apply @AddCommGroupWithOne.toAddGroupWithOne to AddGroupWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddGroupWithOne ℕ ≟ AddGroupWithOne ℕ
      [Meta.synthInstance] new goal AddCommGroupWithOne ℕ
        [Meta.synthInstance.instances] #[@CommRing.toAddCommGroupWithOne, @NonAssocRing.toAddCommGroupWithOne]
    [Meta.synthInstance] ✅ apply @NonAssocRing.toAddCommGroupWithOne to AddCommGroupWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddCommGroupWithOne ℕ ≟ AddCommGroupWithOne ℕ
      [Meta.synthInstance] new goal NonAssocRing ℕ
        [Meta.synthInstance.instances] #[@Ring.toNonAssocRing]
    [Meta.synthInstance] ✅ apply @Ring.toNonAssocRing to NonAssocRing ℕ
      [Meta.synthInstance.tryResolve] ✅ NonAssocRing ℕ ≟ NonAssocRing ℕ
    [Meta.synthInstance] ✅ apply @CommRing.toAddCommGroupWithOne to AddCommGroupWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddCommGroupWithOne ℕ ≟ AddCommGroupWithOne ℕ
    [Meta.synthInstance] ✅ apply @AddCommMonoidWithOne.toAddMonoidWithOne to AddMonoidWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddMonoidWithOne ℕ ≟ AddMonoidWithOne ℕ
      [Meta.synthInstance] new goal AddCommMonoidWithOne ℕ
        [Meta.synthInstance.instances] #[@AddCommGroupWithOne.toAddCommMonoidWithOne, @NonAssocSemiring.toAddCommMonoidWithOne]
    [Meta.synthInstance] ✅ apply @NonAssocSemiring.toAddCommMonoidWithOne to AddCommMonoidWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddCommMonoidWithOne ℕ ≟ AddCommMonoidWithOne ℕ
      [Meta.synthInstance] new goal NonAssocSemiring ℕ
        [Meta.synthInstance.instances] #[@NonAssocRing.toNonAssocSemiring, @Semiring.toNonAssocSemiring]
    [Meta.synthInstance] ✅ apply @Semiring.toNonAssocSemiring to NonAssocSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ NonAssocSemiring ℕ ≟ NonAssocSemiring ℕ
      [Meta.synthInstance] new goal Semiring ℕ
        [Meta.synthInstance.instances] #[@instSemiring, @Ring.toSemiring, @CommSemiring.toSemiring, @OrderedSemiring.toSemiring, @StrictOrderedSemiring.toSemiring, @DivisionSemiring.toSemiring, @IdemSemiring.toSemiring, Nat.semiring]
    [Meta.synthInstance] ✅ apply Nat.semiring to Semiring ℕ
      [Meta.synthInstance.tryResolve] ✅ Semiring ℕ ≟ Semiring ℕ
    [Meta.synthInstance.resume] propagating Semiring ℕ to subgoal Semiring ℕ of NonAssocSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.resume] propagating NonAssocSemiring ℕ to subgoal NonAssocSemiring ℕ of AddCommMonoidWithOne ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.resume] propagating AddCommMonoidWithOne
          ℕ to subgoal AddCommMonoidWithOne ℕ of AddMonoidWithOne ℕ
      [Meta.synthInstance.resume] size: 3
    [Meta.synthInstance] result AddCommMonoidWithOne.toAddMonoidWithOne
  [Meta.synthInstance] [0.040901s] ✅ CharZero ℕ
    [Meta.synthInstance] new goal CharZero ℕ
      [Meta.synthInstance.instances] #[@StrictOrderedSemiring.to_charZero, charZero_of_expChar_one']
    [Meta.synthInstance] ✅ apply charZero_of_expChar_one' to CharZero ℕ
      [Meta.synthInstance.tryResolve] ✅ CharZero ℕ ≟ CharZero ℕ
      [Meta.synthInstance] new goal Nontrivial ℕ
        [Meta.synthInstance.instances] #[Infinite.instNontrivial, @GroupWithZero.toNontrivial, @CommGroupWithZero.toNontrivial, @LinearOrderedAddCommGroupWithTop.toNontrivial, @IsDomain.toNontrivial, @StrictOrderedSemiring.toNontrivial, @StrictOrderedRing.toNontrivial, @LinearOrderedCommGroupWithZero.toNontrivial, @instNontrivial, @DivisionSemiring.toNontrivial, @DivisionRing.toNontrivial, @Semifield.toNontrivial, @Field.toNontrivial, @IsSimpleOrder.toNontrivial, Nat.nontrivial]
    [Meta.synthInstance] ✅ apply Nat.nontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
    [Meta.synthInstance.resume] propagating Nontrivial ℕ to subgoal Nontrivial ℕ of CharZero ℕ
      [Meta.synthInstance.resume] size: 1
      [Meta.synthInstance] no instances for ExpChar ℕ 1
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @IsSimpleOrder.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
      [Meta.synthInstance] new goal LE ℕ
        [Meta.synthInstance.instances] #[@Preorder.toLE, instLENat]
    [Meta.synthInstance] ✅ apply instLENat to LE ℕ
      [Meta.synthInstance.tryResolve] ✅ LE ℕ ≟ LE ℕ
    [Meta.synthInstance.resume] propagating LE ℕ to subgoal LE ℕ of Nontrivial ℕ
      [Meta.synthInstance.resume] size: 1
      [Meta.synthInstance] new goal BoundedOrder ℕ
        [Meta.synthInstance.instances] #[@HeytingAlgebra.toBoundedOrder, @CoheytingAlgebra.toBoundedOrder, @BooleanAlgebra.toBoundedOrder, @CompleteLattice.toBoundedOrder]
    [Meta.synthInstance] ❌ apply @CompleteLattice.toBoundedOrder to BoundedOrder ℕ
      [Meta.synthInstance.tryResolve] ❌ BoundedOrder ℕ ≟ BoundedOrder ?m.169
        [Meta.synthInstance] ❌ CompleteLattice ℕ
          [Meta.synthInstance] new goal CompleteLattice ℕ
            [Meta.synthInstance.instances] #[@CompleteLinearOrder.toCompleteLattice, @Order.Frame.toCompleteLattice, @Order.Coframe.toCompleteLattice, @CompletelyDistribLattice.toCompleteLattice]
          [Meta.synthInstance] ✅ apply @CompletelyDistribLattice.toCompleteLattice to CompleteLattice ℕ
            [Meta.synthInstance.tryResolve] ✅ CompleteLattice ℕ ≟ CompleteLattice ℕ
            [Meta.synthInstance] new goal CompletelyDistribLattice ℕ
              [Meta.synthInstance.instances] #[@CompleteLinearOrder.toCompletelyDistribLattice, @CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice]
          [Meta.synthInstance] ✅ apply @CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice to CompletelyDistribLattice
                ℕ
            [Meta.synthInstance.tryResolve] ✅ CompletelyDistribLattice ℕ ≟ CompletelyDistribLattice ℕ
            [Meta.synthInstance] no instances for CompleteAtomicBooleanAlgebra ℕ
              [Meta.synthInstance.instances] #[]
          [Meta.synthInstance] ✅ apply @CompleteLinearOrder.toCompletelyDistribLattice to CompletelyDistribLattice ℕ
            [Meta.synthInstance.tryResolve] ✅ CompletelyDistribLattice ℕ ≟ CompletelyDistribLattice ℕ
            [Meta.synthInstance] no instances for CompleteLinearOrder ℕ
              [Meta.synthInstance.instances] #[]
          [Meta.synthInstance] ✅ apply @Order.Coframe.toCompleteLattice to CompleteLattice ℕ
            [Meta.synthInstance.tryResolve] ✅ CompleteLattice ℕ ≟ CompleteLattice ℕ
            [Meta.synthInstance] new goal Order.Coframe ℕ
              [Meta.synthInstance.instances] #[@CompleteDistribLattice.toCoframe]
          [Meta.synthInstance] ✅ apply @CompleteDistribLattice.toCoframe to Order.Coframe ℕ
            [Meta.synthInstance.tryResolve] ✅ Order.Coframe ℕ ≟ Order.Coframe ℕ
            [Meta.synthInstance] new goal CompleteDistribLattice ℕ
              [Meta.synthInstance.instances] #[@CompletelyDistribLattice.toCompleteDistribLattice, @CompleteBooleanAlgebra.toCompleteDistribLattice]
          [Meta.synthInstance] ✅ apply @CompleteBooleanAlgebra.toCompleteDistribLattice to CompleteDistribLattice ℕ
            [Meta.synthInstance.tryResolve] ✅ CompleteDistribLattice ℕ ≟ CompleteDistribLattice ℕ
            [Meta.synthInstance] new goal CompleteBooleanAlgebra ℕ
              [Meta.synthInstance.instances] #[@CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra]
          [Meta.synthInstance] ✅ apply @CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra to CompleteBooleanAlgebra
                ℕ
            [Meta.synthInstance.tryResolve] ✅ CompleteBooleanAlgebra ℕ ≟ CompleteBooleanAlgebra ℕ
            [Meta.synthInstance] no instances for CompleteAtomicBooleanAlgebra ℕ
              [Meta.synthInstance.instances] #[]
          [Meta.synthInstance] ✅ apply @CompletelyDistribLattice.toCompleteDistribLattice to CompleteDistribLattice ℕ
            [Meta.synthInstance.tryResolve] ✅ CompleteDistribLattice ℕ ≟ CompleteDistribLattice ℕ
          [Meta.synthInstance] ✅ apply @Order.Frame.toCompleteLattice to CompleteLattice ℕ
            [Meta.synthInstance.tryResolve] ✅ CompleteLattice ℕ ≟ CompleteLattice ℕ
            [Meta.synthInstance] new goal Order.Frame ℕ
              [Meta.synthInstance.instances] #[@CompleteDistribLattice.toFrame]
          [Meta.synthInstance] ✅ apply @CompleteDistribLattice.toFrame to Order.Frame ℕ
            [Meta.synthInstance.tryResolve] ✅ Order.Frame ℕ ≟ Order.Frame ℕ
          [Meta.synthInstance] ✅ apply @CompleteLinearOrder.toCompleteLattice to CompleteLattice ℕ
            [Meta.synthInstance.tryResolve] ✅ CompleteLattice ℕ ≟ CompleteLattice ℕ
            [Meta.synthInstance] no instances for CompleteLinearOrder ℕ
              [Meta.synthInstance.instances] #[]
        [Meta.synthInstance] ❌ CompleteLattice ℕ
          [Meta.synthInstance] result <not-available> (cached)
    [Meta.synthInstance] ❌ apply @BooleanAlgebra.toBoundedOrder to BoundedOrder ℕ
      [Meta.synthInstance.tryResolve] ❌ BoundedOrder ℕ ≟ BoundedOrder ?m.224
        [Meta.synthInstance] ❌ BooleanAlgebra ℕ
          [Meta.synthInstance] new goal BooleanAlgebra ℕ
            [Meta.synthInstance.instances] #[@CompleteBooleanAlgebra.toBooleanAlgebra]
          [Meta.synthInstance] ✅ apply @CompleteBooleanAlgebra.toBooleanAlgebra to BooleanAlgebra ℕ
            [Meta.synthInstance.tryResolve] ✅ BooleanAlgebra ℕ ≟ BooleanAlgebra ℕ
            [Meta.synthInstance] new goal CompleteBooleanAlgebra ℕ
              [Meta.synthInstance.instances] #[@CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra]
          [Meta.synthInstance] ✅ apply @CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra to CompleteBooleanAlgebra
                ℕ
            [Meta.synthInstance.tryResolve] ✅ CompleteBooleanAlgebra ℕ ≟ CompleteBooleanAlgebra ℕ
            [Meta.synthInstance] no instances for CompleteAtomicBooleanAlgebra ℕ
              [Meta.synthInstance.instances] #[]
        [Meta.synthInstance] ❌ BooleanAlgebra ℕ
          [Meta.synthInstance] result <not-available> (cached)
    [Meta.synthInstance] ❌ apply @CoheytingAlgebra.toBoundedOrder to BoundedOrder ℕ
      [Meta.synthInstance.tryResolve] ❌ BoundedOrder ℕ ≟ BoundedOrder ?m.240
        [Meta.synthInstance] ❌ CoheytingAlgebra ℕ
          [Meta.synthInstance] new goal CoheytingAlgebra ℕ
            [Meta.synthInstance.instances] #[@BiheytingAlgebra.toCoheytingAlgebra]
          [Meta.synthInstance] ✅ apply @BiheytingAlgebra.toCoheytingAlgebra to CoheytingAlgebra ℕ
            [Meta.synthInstance.tryResolve] ✅ CoheytingAlgebra ℕ ≟ CoheytingAlgebra ℕ
            [Meta.synthInstance] new goal BiheytingAlgebra ℕ
              [Meta.synthInstance.instances] #[@BooleanAlgebra.toBiheytingAlgebra]
          [Meta.synthInstance] ✅ apply @BooleanAlgebra.toBiheytingAlgebra to BiheytingAlgebra ℕ
            [Meta.synthInstance.tryResolve] ✅ BiheytingAlgebra ℕ ≟ BiheytingAlgebra ℕ
            [Meta.synthInstance] new goal BooleanAlgebra ℕ
              [Meta.synthInstance.instances] #[@CompleteBooleanAlgebra.toBooleanAlgebra]
          [Meta.synthInstance] ✅ apply @CompleteBooleanAlgebra.toBooleanAlgebra to BooleanAlgebra ℕ
            [Meta.synthInstance.tryResolve] ✅ BooleanAlgebra ℕ ≟ BooleanAlgebra ℕ
            [Meta.synthInstance] new goal CompleteBooleanAlgebra ℕ
              [Meta.synthInstance.instances] #[@CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra]
          [Meta.synthInstance] ✅ apply @CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra to CompleteBooleanAlgebra
                ℕ
            [Meta.synthInstance.tryResolve] ✅ CompleteBooleanAlgebra ℕ ≟ CompleteBooleanAlgebra ℕ
            [Meta.synthInstance] no instances for CompleteAtomicBooleanAlgebra ℕ
              [Meta.synthInstance.instances] #[]
        [Meta.synthInstance] ❌ CoheytingAlgebra ℕ
          [Meta.synthInstance] result <not-available> (cached)
    [Meta.synthInstance] ❌ apply @HeytingAlgebra.toBoundedOrder to BoundedOrder ℕ
      [Meta.synthInstance.tryResolve] ❌ BoundedOrder ℕ ≟ BoundedOrder ?m.265
        [Meta.synthInstance] ❌ HeytingAlgebra ℕ
          [Meta.synthInstance] new goal HeytingAlgebra ℕ
            [Meta.synthInstance.instances] #[@BiheytingAlgebra.toHeytingAlgebra]
          [Meta.synthInstance] ✅ apply @BiheytingAlgebra.toHeytingAlgebra to HeytingAlgebra ℕ
            [Meta.synthInstance.tryResolve] ✅ HeytingAlgebra ℕ ≟ HeytingAlgebra ℕ
            [Meta.synthInstance] new goal BiheytingAlgebra ℕ
              [Meta.synthInstance.instances] #[@BooleanAlgebra.toBiheytingAlgebra]
          [Meta.synthInstance] ✅ apply @BooleanAlgebra.toBiheytingAlgebra to BiheytingAlgebra ℕ
            [Meta.synthInstance.tryResolve] ✅ BiheytingAlgebra ℕ ≟ BiheytingAlgebra ℕ
            [Meta.synthInstance] new goal BooleanAlgebra ℕ
              [Meta.synthInstance.instances] #[@CompleteBooleanAlgebra.toBooleanAlgebra]
          [Meta.synthInstance] ✅ apply @CompleteBooleanAlgebra.toBooleanAlgebra to BooleanAlgebra ℕ
            [Meta.synthInstance.tryResolve] ✅ BooleanAlgebra ℕ ≟ BooleanAlgebra ℕ
            [Meta.synthInstance] new goal CompleteBooleanAlgebra ℕ
              [Meta.synthInstance.instances] #[@CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra]
          [Meta.synthInstance] ✅ apply @CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra to CompleteBooleanAlgebra
                ℕ
            [Meta.synthInstance.tryResolve] ✅ CompleteBooleanAlgebra ℕ ≟ CompleteBooleanAlgebra ℕ
            [Meta.synthInstance] no instances for CompleteAtomicBooleanAlgebra ℕ
              [Meta.synthInstance.instances] #[]
        [Meta.synthInstance] ❌ HeytingAlgebra ℕ
          [Meta.synthInstance] result <not-available> (cached)
    [Meta.synthInstance] ✅ apply @Preorder.toLE to LE ℕ
      [Meta.synthInstance.tryResolve] ✅ LE ℕ ≟ LE ℕ
      [Meta.synthInstance] new goal Preorder ℕ
        [Meta.synthInstance.instances] #[@PartialOrder.toPreorder]
    [Meta.synthInstance] ✅ apply @PartialOrder.toPreorder to Preorder ℕ
      [Meta.synthInstance.tryResolve] ✅ Preorder ℕ ≟ Preorder ℕ
      [Meta.synthInstance] new goal PartialOrder ℕ
        [Meta.synthInstance.instances] #[@SetLike.instPartialOrder, @LinearOrder.toPartialOrder, @SemilatticeSup.toPartialOrder, @SemilatticeInf.toPartialOrder, @OrderedCommMonoid.toPartialOrder, @OrderedAddCommMonoid.toPartialOrder, @OrderedCancelAddCommMonoid.toPartialOrder, @OrderedCancelCommMonoid.toPartialOrder, @OrderedAddCommGroup.toPartialOrder, @OrderedCommGroup.toPartialOrder, @OrderedSemiring.toPartialOrder, @OrderedRing.toPartialOrder, @StrictOrderedSemiring.toPartialOrder, @StrictOrderedRing.toPartialOrder, @CompleteSemilatticeSup.toPartialOrder, @CompleteSemilatticeInf.toPartialOrder, @OmegaCompletePartialOrder.toPartialOrder]
    [Meta.synthInstance] ✅ apply @OmegaCompletePartialOrder.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal OmegaCompletePartialOrder ℕ
        [Meta.synthInstance.instances] #[CompleteLattice.instOmegaCompletePartialOrder]
    [Meta.synthInstance] ✅ apply CompleteLattice.instOmegaCompletePartialOrder to OmegaCompletePartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ OmegaCompletePartialOrder ℕ ≟ OmegaCompletePartialOrder ℕ
      [Meta.synthInstance] new goal CompleteLattice ℕ
        [Meta.synthInstance.instances] #[@CompleteLinearOrder.toCompleteLattice, @Order.Frame.toCompleteLattice, @Order.Coframe.toCompleteLattice, @CompletelyDistribLattice.toCompleteLattice]
    [Meta.synthInstance] ✅ apply @CompletelyDistribLattice.toCompleteLattice to CompleteLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ CompleteLattice ℕ ≟ CompleteLattice ℕ
      [Meta.synthInstance] new goal CompletelyDistribLattice ℕ
        [Meta.synthInstance.instances] #[@CompleteLinearOrder.toCompletelyDistribLattice, @CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice]
    [Meta.synthInstance] ✅ apply @CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice to CompletelyDistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ CompletelyDistribLattice ℕ ≟ CompletelyDistribLattice ℕ
      [Meta.synthInstance] no instances for CompleteAtomicBooleanAlgebra ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @CompleteLinearOrder.toCompletelyDistribLattice to CompletelyDistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ CompletelyDistribLattice ℕ ≟ CompletelyDistribLattice ℕ
      [Meta.synthInstance] no instances for CompleteLinearOrder ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @Order.Coframe.toCompleteLattice to CompleteLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ CompleteLattice ℕ ≟ CompleteLattice ℕ
      [Meta.synthInstance] new goal Order.Coframe ℕ
        [Meta.synthInstance.instances] #[@CompleteDistribLattice.toCoframe]
    [Meta.synthInstance] ✅ apply @CompleteDistribLattice.toCoframe to Order.Coframe ℕ
      [Meta.synthInstance.tryResolve] ✅ Order.Coframe ℕ ≟ Order.Coframe ℕ
      [Meta.synthInstance] new goal CompleteDistribLattice ℕ
        [Meta.synthInstance.instances] #[@CompletelyDistribLattice.toCompleteDistribLattice, @CompleteBooleanAlgebra.toCompleteDistribLattice]
    [Meta.synthInstance] ✅ apply @CompleteBooleanAlgebra.toCompleteDistribLattice to CompleteDistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ CompleteDistribLattice ℕ ≟ CompleteDistribLattice ℕ
      [Meta.synthInstance] new goal CompleteBooleanAlgebra ℕ
        [Meta.synthInstance.instances] #[@CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra]
    [Meta.synthInstance] ✅ apply @CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra to CompleteBooleanAlgebra ℕ
      [Meta.synthInstance.tryResolve] ✅ CompleteBooleanAlgebra ℕ ≟ CompleteBooleanAlgebra ℕ
      [Meta.synthInstance] no instances for CompleteAtomicBooleanAlgebra ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @CompletelyDistribLattice.toCompleteDistribLattice to CompleteDistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ CompleteDistribLattice ℕ ≟ CompleteDistribLattice ℕ
    [Meta.synthInstance] ✅ apply @Order.Frame.toCompleteLattice to CompleteLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ CompleteLattice ℕ ≟ CompleteLattice ℕ
      [Meta.synthInstance] new goal Order.Frame ℕ
        [Meta.synthInstance.instances] #[@CompleteDistribLattice.toFrame]
    [Meta.synthInstance] ✅ apply @CompleteDistribLattice.toFrame to Order.Frame ℕ
      [Meta.synthInstance.tryResolve] ✅ Order.Frame ℕ ≟ Order.Frame ℕ
    [Meta.synthInstance] ✅ apply @CompleteLinearOrder.toCompleteLattice to CompleteLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ CompleteLattice ℕ ≟ CompleteLattice ℕ
      [Meta.synthInstance] no instances for CompleteLinearOrder ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @CompleteSemilatticeInf.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal CompleteSemilatticeInf ℕ
        [Meta.synthInstance.instances] #[@CompleteLattice.toCompleteSemilatticeInf]
    [Meta.synthInstance] ✅ apply @CompleteLattice.toCompleteSemilatticeInf to CompleteSemilatticeInf ℕ
      [Meta.synthInstance.tryResolve] ✅ CompleteSemilatticeInf ℕ ≟ CompleteSemilatticeInf ℕ
    [Meta.synthInstance] ✅ apply @CompleteSemilatticeSup.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal CompleteSemilatticeSup ℕ
        [Meta.synthInstance.instances] #[@CompleteLattice.toCompleteSemilatticeSup]
    [Meta.synthInstance] ✅ apply @CompleteLattice.toCompleteSemilatticeSup to CompleteSemilatticeSup ℕ
      [Meta.synthInstance.tryResolve] ✅ CompleteSemilatticeSup ℕ ≟ CompleteSemilatticeSup ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedRing.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal StrictOrderedRing ℕ
        [Meta.synthInstance.instances] #[@StrictOrderedCommRing.toStrictOrderedRing, @LinearOrderedRing.toStrictOrderedRing]
    [Meta.synthInstance] ✅ apply @LinearOrderedRing.toStrictOrderedRing to StrictOrderedRing ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedRing ℕ ≟ StrictOrderedRing ℕ
      [Meta.synthInstance] new goal LinearOrderedRing ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedCommRing.toLinearOrderedRing]
    [Meta.synthInstance] ✅ apply @LinearOrderedCommRing.toLinearOrderedRing to LinearOrderedRing ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedRing ℕ ≟ LinearOrderedRing ℕ
      [Meta.synthInstance] new goal LinearOrderedCommRing ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedField.toLinearOrderedCommRing]
    [Meta.synthInstance] ✅ apply @LinearOrderedField.toLinearOrderedCommRing to LinearOrderedCommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCommRing ℕ ≟ LinearOrderedCommRing ℕ
      [Meta.synthInstance] no instances for LinearOrderedField ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @StrictOrderedCommRing.toStrictOrderedRing to StrictOrderedRing ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedRing ℕ ≟ StrictOrderedRing ℕ
      [Meta.synthInstance] new goal StrictOrderedCommRing ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedCommRing.toStrictOrderedCommRing]
    [Meta.synthInstance] ✅ apply @LinearOrderedCommRing.toStrictOrderedCommRing to StrictOrderedCommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedCommRing ℕ ≟ StrictOrderedCommRing ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedSemiring.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal StrictOrderedSemiring ℕ
        [Meta.synthInstance.instances] #[@StrictOrderedRing.toStrictOrderedSemiring, @StrictOrderedCommSemiring.toStrictOrderedSemiring, @LinearOrderedSemiring.toStrictOrderedSemiring, Nat.strictOrderedSemiring]
    [Meta.synthInstance] ✅ apply Nat.strictOrderedSemiring to StrictOrderedSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedSemiring ℕ ≟ StrictOrderedSemiring ℕ
    [Meta.synthInstance.resume] propagating StrictOrderedSemiring ℕ to subgoal StrictOrderedSemiring ℕ of PartialOrder ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.resume] propagating PartialOrder ℕ to subgoal PartialOrder ℕ of Preorder ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.resume] propagating Preorder ℕ to subgoal Preorder ℕ of LE ℕ
      [Meta.synthInstance.resume] size: 3
    [Meta.synthInstance] ✅ apply @LinearOrderedSemiring.toStrictOrderedSemiring to StrictOrderedSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedSemiring ℕ ≟ StrictOrderedSemiring ℕ
      [Meta.synthInstance] new goal LinearOrderedSemiring ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedRing.toLinearOrderedSemiring, @LinearOrderedCommSemiring.toLinearOrderedSemiring, Nat.linearOrderedSemiring]
    [Meta.synthInstance] ✅ apply Nat.linearOrderedSemiring to LinearOrderedSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedSemiring ℕ ≟ LinearOrderedSemiring ℕ
    [Meta.synthInstance.resume] propagating LinearOrderedSemiring
          ℕ to subgoal LinearOrderedSemiring ℕ of StrictOrderedSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @LinearOrderedCommSemiring.toLinearOrderedSemiring to LinearOrderedSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedSemiring ℕ ≟ LinearOrderedSemiring ℕ
      [Meta.synthInstance] new goal LinearOrderedCommSemiring ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedCommRing.toLinearOrderedCommSemiring, @LinearOrderedSemifield.toLinearOrderedCommSemiring, Nat.linearOrderedCommSemiring]
    [Meta.synthInstance] ✅ apply Nat.linearOrderedCommSemiring to LinearOrderedCommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCommSemiring ℕ ≟ LinearOrderedCommSemiring ℕ
    [Meta.synthInstance.resume] propagating LinearOrderedCommSemiring
          ℕ to subgoal LinearOrderedCommSemiring ℕ of LinearOrderedSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @LinearOrderedSemifield.toLinearOrderedCommSemiring to LinearOrderedCommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCommSemiring ℕ ≟ LinearOrderedCommSemiring ℕ
      [Meta.synthInstance] new goal LinearOrderedSemifield ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedField.toLinearOrderedSemifield]
    [Meta.synthInstance] ✅ apply @LinearOrderedField.toLinearOrderedSemifield to LinearOrderedSemifield ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedSemifield ℕ ≟ LinearOrderedSemifield ℕ
      [Meta.synthInstance] no instances for LinearOrderedField ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @LinearOrderedCommRing.toLinearOrderedCommSemiring to LinearOrderedCommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCommSemiring ℕ ≟ LinearOrderedCommSemiring ℕ
    [Meta.synthInstance] ✅ apply @LinearOrderedRing.toLinearOrderedSemiring to LinearOrderedSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedSemiring ℕ ≟ LinearOrderedSemiring ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedCommSemiring.toStrictOrderedSemiring to StrictOrderedSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedSemiring ℕ ≟ StrictOrderedSemiring ℕ
      [Meta.synthInstance] new goal StrictOrderedCommSemiring ℕ
        [Meta.synthInstance.instances] #[@StrictOrderedCommRing.toStrictOrderedCommSemiring, @LinearOrderedCommSemiring.toStrictOrderedCommSemiring, Nat.strictOrderedCommSemiring]
    [Meta.synthInstance] ✅ apply Nat.strictOrderedCommSemiring to StrictOrderedCommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedCommSemiring ℕ ≟ StrictOrderedCommSemiring ℕ
    [Meta.synthInstance.resume] propagating StrictOrderedCommSemiring
          ℕ to subgoal StrictOrderedCommSemiring ℕ of StrictOrderedSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @LinearOrderedCommSemiring.toStrictOrderedCommSemiring to StrictOrderedCommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedCommSemiring ℕ ≟ StrictOrderedCommSemiring ℕ
    [Meta.synthInstance.resume] propagating LinearOrderedCommSemiring
          ℕ to subgoal LinearOrderedCommSemiring ℕ of StrictOrderedCommSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @StrictOrderedCommRing.toStrictOrderedCommSemiring to StrictOrderedCommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedCommSemiring ℕ ≟ StrictOrderedCommSemiring ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedRing.toStrictOrderedSemiring to StrictOrderedSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ StrictOrderedSemiring ℕ ≟ StrictOrderedSemiring ℕ
    [Meta.synthInstance] ✅ apply @OrderedRing.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal OrderedRing ℕ
        [Meta.synthInstance.instances] #[@StrictOrderedRing.toOrderedRing, @OrderedCommRing.toOrderedRing]
    [Meta.synthInstance] ✅ apply @OrderedCommRing.toOrderedRing to OrderedRing ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedRing ℕ ≟ OrderedRing ℕ
      [Meta.synthInstance] new goal OrderedCommRing ℕ
        [Meta.synthInstance.instances] #[@StrictOrderedCommRing.toOrderedCommRing]
    [Meta.synthInstance] ✅ apply @StrictOrderedCommRing.toOrderedCommRing to OrderedCommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCommRing ℕ ≟ OrderedCommRing ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedRing.toOrderedRing to OrderedRing ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedRing ℕ ≟ OrderedRing ℕ
    [Meta.synthInstance] ✅ apply @OrderedSemiring.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal OrderedSemiring ℕ
        [Meta.synthInstance.instances] #[@OrderedRing.toOrderedSemiring, @StrictOrderedSemiring.toOrderedSemiring, @OrderedCommSemiring.toOrderedSemiring, Nat.orderedSemiring]
    [Meta.synthInstance] ✅ apply Nat.orderedSemiring to OrderedSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedSemiring ℕ ≟ OrderedSemiring ℕ
    [Meta.synthInstance.resume] propagating OrderedSemiring ℕ to subgoal OrderedSemiring ℕ of PartialOrder ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @OrderedCommSemiring.toOrderedSemiring to OrderedSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedSemiring ℕ ≟ OrderedSemiring ℕ
      [Meta.synthInstance] new goal OrderedCommSemiring ℕ
        [Meta.synthInstance.instances] #[@OrderedCommRing.toOrderedCommSemiring, @StrictOrderedCommSemiring.toOrderedCommSemiring, @CanonicallyOrderedCommSemiring.toOrderedCommSemiring, Nat.orderedCommSemiring]
    [Meta.synthInstance] ✅ apply Nat.orderedCommSemiring to OrderedCommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCommSemiring ℕ ≟ OrderedCommSemiring ℕ
    [Meta.synthInstance.resume] propagating OrderedCommSemiring ℕ to subgoal OrderedCommSemiring ℕ of OrderedSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @CanonicallyOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCommSemiring ℕ ≟ OrderedCommSemiring ℕ
      [Meta.synthInstance] new goal CanonicallyOrderedCommSemiring ℕ
        [Meta.synthInstance.instances] #[Nat.canonicallyOrderedCommSemiring]
    [Meta.synthInstance] ✅ apply Nat.canonicallyOrderedCommSemiring to CanonicallyOrderedCommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ CanonicallyOrderedCommSemiring ℕ ≟ CanonicallyOrderedCommSemiring ℕ
    [Meta.synthInstance.resume] propagating CanonicallyOrderedCommSemiring
          ℕ to subgoal CanonicallyOrderedCommSemiring ℕ of OrderedCommSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @StrictOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCommSemiring ℕ ≟ OrderedCommSemiring ℕ
    [Meta.synthInstance.resume] propagating StrictOrderedCommSemiring
          ℕ to subgoal StrictOrderedCommSemiring ℕ of OrderedCommSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @OrderedCommRing.toOrderedCommSemiring to OrderedCommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCommSemiring ℕ ≟ OrderedCommSemiring ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedSemiring.toOrderedSemiring to OrderedSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedSemiring ℕ ≟ OrderedSemiring ℕ
    [Meta.synthInstance.resume] propagating StrictOrderedSemiring
          ℕ to subgoal StrictOrderedSemiring ℕ of OrderedSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @OrderedRing.toOrderedSemiring to OrderedSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedSemiring ℕ ≟ OrderedSemiring ℕ
    [Meta.synthInstance] ✅ apply @OrderedCommGroup.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal OrderedCommGroup ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedCommGroup.toOrderedCommGroup]
    [Meta.synthInstance] ✅ apply @LinearOrderedCommGroup.toOrderedCommGroup to OrderedCommGroup ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCommGroup ℕ ≟ OrderedCommGroup ℕ
      [Meta.synthInstance] no instances for LinearOrderedCommGroup ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @OrderedAddCommGroup.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal OrderedAddCommGroup ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedAddCommGroup.toOrderedAddCommGroup, @OrderedRing.toOrderedAddCommGroup, @StrictOrderedRing.toOrderedAddCommGroup]
    [Meta.synthInstance] ✅ apply @StrictOrderedRing.toOrderedAddCommGroup to OrderedAddCommGroup ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedAddCommGroup ℕ ≟ OrderedAddCommGroup ℕ
    [Meta.synthInstance] ✅ apply @OrderedRing.toOrderedAddCommGroup to OrderedAddCommGroup ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedAddCommGroup ℕ ≟ OrderedAddCommGroup ℕ
    [Meta.synthInstance] ✅ apply @LinearOrderedAddCommGroup.toOrderedAddCommGroup to OrderedAddCommGroup ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedAddCommGroup ℕ ≟ OrderedAddCommGroup ℕ
      [Meta.synthInstance] new goal LinearOrderedAddCommGroup ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedRing.toLinearOrderedAddCommGroup]
    [Meta.synthInstance] ✅ apply @LinearOrderedRing.toLinearOrderedAddCommGroup to LinearOrderedAddCommGroup ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedAddCommGroup ℕ ≟ LinearOrderedAddCommGroup ℕ
    [Meta.synthInstance] ✅ apply @OrderedCancelCommMonoid.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal OrderedCancelCommMonoid ℕ
        [Meta.synthInstance.instances] #[@OrderedCommGroup.toOrderedCancelCommMonoid, @LinearOrderedCancelCommMonoid.toOrderedCancelCommMonoid]
    [Meta.synthInstance] ✅ apply @LinearOrderedCancelCommMonoid.toOrderedCancelCommMonoid to OrderedCancelCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCancelCommMonoid ℕ ≟ OrderedCancelCommMonoid ℕ
      [Meta.synthInstance] new goal LinearOrderedCancelCommMonoid ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedCommGroup.toLinearOrderedCancelCommMonoid]
    [Meta.synthInstance] ✅ apply @LinearOrderedCommGroup.toLinearOrderedCancelCommMonoid to LinearOrderedCancelCommMonoid
          ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCancelCommMonoid ℕ ≟ LinearOrderedCancelCommMonoid ℕ
      [Meta.synthInstance] no instances for LinearOrderedCommGroup ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @OrderedCommGroup.toOrderedCancelCommMonoid to OrderedCancelCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCancelCommMonoid ℕ ≟ OrderedCancelCommMonoid ℕ
    [Meta.synthInstance] ✅ apply @OrderedCancelAddCommMonoid.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal OrderedCancelAddCommMonoid ℕ
        [Meta.synthInstance.instances] #[@OrderedAddCommGroup.toOrderedCancelAddCommMonoid, @LinearOrderedCancelAddCommMonoid.toOrderedCancelAddCommMonoid, @StrictOrderedSemiring.toOrderedCancelAddCommMonoid]
    [Meta.synthInstance] ✅ apply @StrictOrderedSemiring.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCancelAddCommMonoid ℕ ≟ OrderedCancelAddCommMonoid ℕ
    [Meta.synthInstance.resume] propagating StrictOrderedSemiring
          ℕ to subgoal StrictOrderedSemiring ℕ of OrderedCancelAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.resume] propagating OrderedCancelAddCommMonoid
          ℕ to subgoal OrderedCancelAddCommMonoid ℕ of PartialOrder ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance] ✅ apply @LinearOrderedCancelAddCommMonoid.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid
          ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCancelAddCommMonoid ℕ ≟ OrderedCancelAddCommMonoid ℕ
      [Meta.synthInstance] new goal LinearOrderedCancelAddCommMonoid ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid, @LinearOrderedCommSemiring.toLinearOrderedCancelAddCommMonoid, Nat.linearOrderedCancelAddCommMonoid]
    [Meta.synthInstance] ✅ apply Nat.linearOrderedCancelAddCommMonoid to LinearOrderedCancelAddCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCancelAddCommMonoid ℕ ≟ LinearOrderedCancelAddCommMonoid ℕ
    [Meta.synthInstance.resume] propagating LinearOrderedCancelAddCommMonoid
          ℕ to subgoal LinearOrderedCancelAddCommMonoid ℕ of OrderedCancelAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @LinearOrderedCommSemiring.toLinearOrderedCancelAddCommMonoid to LinearOrderedCancelAddCommMonoid
          ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCancelAddCommMonoid ℕ ≟ LinearOrderedCancelAddCommMonoid ℕ
    [Meta.synthInstance.resume] propagating LinearOrderedCommSemiring
          ℕ to subgoal LinearOrderedCommSemiring ℕ of LinearOrderedCancelAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid to LinearOrderedCancelAddCommMonoid
          ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCancelAddCommMonoid ℕ ≟ LinearOrderedCancelAddCommMonoid ℕ
    [Meta.synthInstance] ✅ apply @OrderedAddCommGroup.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCancelAddCommMonoid ℕ ≟ OrderedCancelAddCommMonoid ℕ
    [Meta.synthInstance] ✅ apply @OrderedAddCommMonoid.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal OrderedAddCommMonoid ℕ
        [Meta.synthInstance.instances] #[@OrderedCancelAddCommMonoid.toOrderedAddCommMonoid, @LinearOrderedAddCommMonoid.toOrderedAddCommMonoid, @CanonicallyOrderedAddCommMonoid.toOrderedAddCommMonoid, @OrderedSemiring.toOrderedAddCommMonoid]
    [Meta.synthInstance] ✅ apply @OrderedSemiring.toOrderedAddCommMonoid to OrderedAddCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedAddCommMonoid ℕ ≟ OrderedAddCommMonoid ℕ
    [Meta.synthInstance.resume] propagating OrderedSemiring ℕ to subgoal OrderedSemiring ℕ of OrderedAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.resume] propagating OrderedAddCommMonoid ℕ to subgoal OrderedAddCommMonoid ℕ of PartialOrder ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance] ✅ apply @CanonicallyOrderedAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedAddCommMonoid ℕ ≟ OrderedAddCommMonoid ℕ
      [Meta.synthInstance] new goal CanonicallyOrderedAddCommMonoid ℕ
        [Meta.synthInstance.instances] #[@IdemSemiring.toCanonicallyOrderedAddCommMonoid, @CanonicallyLinearOrderedAddCommMonoid.toCanonicallyOrderedAddCommMonoid, @CanonicallyOrderedCommSemiring.toCanonicallyOrderedAddCommMonoid]
    [Meta.synthInstance] ✅ apply @CanonicallyOrderedCommSemiring.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid
          ℕ
      [Meta.synthInstance.tryResolve] ✅ CanonicallyOrderedAddCommMonoid ℕ ≟ CanonicallyOrderedAddCommMonoid ℕ
    [Meta.synthInstance.resume] propagating CanonicallyOrderedCommSemiring
          ℕ to subgoal CanonicallyOrderedCommSemiring ℕ of CanonicallyOrderedAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.resume] propagating CanonicallyOrderedAddCommMonoid
          ℕ to subgoal CanonicallyOrderedAddCommMonoid ℕ of OrderedAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid
          ℕ
      [Meta.synthInstance.tryResolve] ✅ CanonicallyOrderedAddCommMonoid ℕ ≟ CanonicallyOrderedAddCommMonoid ℕ
      [Meta.synthInstance] new goal CanonicallyLinearOrderedAddCommMonoid ℕ
        [Meta.synthInstance.instances] #[Nat.canonicallyLinearOrderedAddCommMonoid]
    [Meta.synthInstance] ✅ apply Nat.canonicallyLinearOrderedAddCommMonoid to CanonicallyLinearOrderedAddCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ CanonicallyLinearOrderedAddCommMonoid
            ℕ ≟ CanonicallyLinearOrderedAddCommMonoid ℕ
    [Meta.synthInstance.resume] propagating CanonicallyLinearOrderedAddCommMonoid
          ℕ to subgoal CanonicallyLinearOrderedAddCommMonoid ℕ of CanonicallyOrderedAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @IdemSemiring.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ CanonicallyOrderedAddCommMonoid ℕ ≟ CanonicallyOrderedAddCommMonoid ℕ
      [Meta.synthInstance] new goal IdemSemiring ℕ
        [Meta.synthInstance.instances] #[@IdemCommSemiring.toIdemSemiring, @KleeneAlgebra.toIdemSemiring]
    [Meta.synthInstance] ✅ apply @KleeneAlgebra.toIdemSemiring to IdemSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ IdemSemiring ℕ ≟ IdemSemiring ℕ
      [Meta.synthInstance] no instances for KleeneAlgebra ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @IdemCommSemiring.toIdemSemiring to IdemSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ IdemSemiring ℕ ≟ IdemSemiring ℕ
      [Meta.synthInstance] no instances for IdemCommSemiring ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @LinearOrderedAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedAddCommMonoid ℕ ≟ OrderedAddCommMonoid ℕ
      [Meta.synthInstance] new goal LinearOrderedAddCommMonoid ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedAddCommMonoidWithTop.toLinearOrderedAddCommMonoid, @LinearOrderedCancelAddCommMonoid.toLinearOrderedAddCommMonoid, @CanonicallyLinearOrderedAddCommMonoid.toLinearOrderedAddCommMonoid, @LinearOrderedSemiring.toLinearOrderedAddCommMonoid]
    [Meta.synthInstance] ✅ apply @LinearOrderedSemiring.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedAddCommMonoid ℕ ≟ LinearOrderedAddCommMonoid ℕ
    [Meta.synthInstance.resume] propagating LinearOrderedSemiring
          ℕ to subgoal LinearOrderedSemiring ℕ of LinearOrderedAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.resume] propagating LinearOrderedAddCommMonoid
          ℕ to subgoal LinearOrderedAddCommMonoid ℕ of OrderedAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid
          ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedAddCommMonoid ℕ ≟ LinearOrderedAddCommMonoid ℕ
    [Meta.synthInstance.resume] propagating CanonicallyLinearOrderedAddCommMonoid
          ℕ to subgoal CanonicallyLinearOrderedAddCommMonoid ℕ of LinearOrderedAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @LinearOrderedCancelAddCommMonoid.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid
          ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedAddCommMonoid ℕ ≟ LinearOrderedAddCommMonoid ℕ
    [Meta.synthInstance.resume] propagating LinearOrderedCancelAddCommMonoid
          ℕ to subgoal LinearOrderedCancelAddCommMonoid ℕ of LinearOrderedAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @LinearOrderedAddCommMonoidWithTop.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid
          ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedAddCommMonoid ℕ ≟ LinearOrderedAddCommMonoid ℕ
      [Meta.synthInstance] new goal LinearOrderedAddCommMonoidWithTop ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedAddCommGroupWithTop.toLinearOrderedAddCommMonoidWithTop]
    [Meta.synthInstance] ✅ apply @LinearOrderedAddCommGroupWithTop.toLinearOrderedAddCommMonoidWithTop to LinearOrderedAddCommMonoidWithTop
          ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedAddCommMonoidWithTop ℕ ≟ LinearOrderedAddCommMonoidWithTop ℕ
      [Meta.synthInstance] no instances for LinearOrderedAddCommGroupWithTop ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @OrderedCancelAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedAddCommMonoid ℕ ≟ OrderedAddCommMonoid ℕ
    [Meta.synthInstance.resume] propagating OrderedCancelAddCommMonoid
          ℕ to subgoal OrderedCancelAddCommMonoid ℕ of OrderedAddCommMonoid ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance] ✅ apply @OrderedCommMonoid.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal OrderedCommMonoid ℕ
        [Meta.synthInstance.instances] #[@OrderedCancelCommMonoid.toOrderedCommMonoid, @CanonicallyOrderedCommSemiring.toOrderedCommMonoid, @LinearOrderedCommMonoid.toOrderedCommMonoid, @CanonicallyOrderedCommMonoid.toOrderedCommMonoid]
    [Meta.synthInstance] ✅ apply @CanonicallyOrderedCommMonoid.toOrderedCommMonoid to OrderedCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCommMonoid ℕ ≟ OrderedCommMonoid ℕ
      [Meta.synthInstance] new goal CanonicallyOrderedCommMonoid ℕ
        [Meta.synthInstance.instances] #[@CanonicallyLinearOrderedCommMonoid.toCanonicallyOrderedCommMonoid]
    [Meta.synthInstance] ✅ apply @CanonicallyLinearOrderedCommMonoid.toCanonicallyOrderedCommMonoid to CanonicallyOrderedCommMonoid
          ℕ
      [Meta.synthInstance.tryResolve] ✅ CanonicallyOrderedCommMonoid ℕ ≟ CanonicallyOrderedCommMonoid ℕ
      [Meta.synthInstance] no instances for CanonicallyLinearOrderedCommMonoid ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @LinearOrderedCommMonoid.toOrderedCommMonoid to OrderedCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCommMonoid ℕ ≟ OrderedCommMonoid ℕ
      [Meta.synthInstance] new goal LinearOrderedCommMonoid ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedCancelCommMonoid.toLinearOrderedCommMonoid, @CanonicallyLinearOrderedCommMonoid.toLinearOrderedCommMonoid, @LinearOrderedCommMonoidWithZero.toLinearOrderedCommMonoid]
    [Meta.synthInstance] ✅ apply @LinearOrderedCommMonoidWithZero.toLinearOrderedCommMonoid to LinearOrderedCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCommMonoid ℕ ≟ LinearOrderedCommMonoid ℕ
      [Meta.synthInstance] new goal LinearOrderedCommMonoidWithZero ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero, Nat.linearOrderedCommMonoidWithZero]
    [Meta.synthInstance] ✅ apply Nat.linearOrderedCommMonoidWithZero to LinearOrderedCommMonoidWithZero ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCommMonoidWithZero ℕ ≟ LinearOrderedCommMonoidWithZero ℕ
    [Meta.synthInstance.resume] propagating LinearOrderedCommMonoidWithZero
          ℕ to subgoal LinearOrderedCommMonoidWithZero ℕ of LinearOrderedCommMonoid ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.resume] propagating LinearOrderedCommMonoid
          ℕ to subgoal LinearOrderedCommMonoid ℕ of OrderedCommMonoid ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.resume] propagating OrderedCommMonoid ℕ to subgoal OrderedCommMonoid ℕ of PartialOrder ℕ
      [Meta.synthInstance.resume] size: 3
    [Meta.synthInstance] ✅ apply @LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero to LinearOrderedCommMonoidWithZero
          ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCommMonoidWithZero ℕ ≟ LinearOrderedCommMonoidWithZero ℕ
      [Meta.synthInstance] no instances for LinearOrderedCommGroupWithZero ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @CanonicallyLinearOrderedCommMonoid.toLinearOrderedCommMonoid to LinearOrderedCommMonoid
          ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCommMonoid ℕ ≟ LinearOrderedCommMonoid ℕ
      [Meta.synthInstance] no instances for CanonicallyLinearOrderedCommMonoid ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @LinearOrderedCancelCommMonoid.toLinearOrderedCommMonoid to LinearOrderedCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrderedCommMonoid ℕ ≟ LinearOrderedCommMonoid ℕ
    [Meta.synthInstance] ✅ apply @CanonicallyOrderedCommSemiring.toOrderedCommMonoid to OrderedCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCommMonoid ℕ ≟ OrderedCommMonoid ℕ
    [Meta.synthInstance.resume] propagating CanonicallyOrderedCommSemiring
          ℕ to subgoal CanonicallyOrderedCommSemiring ℕ of OrderedCommMonoid ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @OrderedCancelCommMonoid.toOrderedCommMonoid to OrderedCommMonoid ℕ
      [Meta.synthInstance.tryResolve] ✅ OrderedCommMonoid ℕ ≟ OrderedCommMonoid ℕ
    [Meta.synthInstance] ✅ apply @SemilatticeInf.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal SemilatticeInf ℕ
        [Meta.synthInstance.instances] #[@Lattice.toSemilatticeInf]
    [Meta.synthInstance] ✅ apply @Lattice.toSemilatticeInf to SemilatticeInf ℕ
      [Meta.synthInstance.tryResolve] ✅ SemilatticeInf ℕ ≟ SemilatticeInf ℕ
      [Meta.synthInstance] new goal Lattice ℕ
        [Meta.synthInstance.instances] #[@LinearOrder.toLattice, @DistribLattice.toLattice, @GeneralizedHeytingAlgebra.toLattice, @GeneralizedCoheytingAlgebra.toLattice, @CompleteLattice.toLattice, @ConditionallyCompleteLattice.toLattice, Nat.instLatticeNat]
    [Meta.synthInstance] ✅ apply Nat.instLatticeNat to Lattice ℕ
      [Meta.synthInstance.tryResolve] ✅ Lattice ℕ ≟ Lattice ℕ
    [Meta.synthInstance.resume] propagating Lattice ℕ to subgoal Lattice ℕ of SemilatticeInf ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.resume] propagating SemilatticeInf ℕ to subgoal SemilatticeInf ℕ of PartialOrder ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance] ✅ apply @ConditionallyCompleteLattice.toLattice to Lattice ℕ
      [Meta.synthInstance.tryResolve] ✅ Lattice ℕ ≟ Lattice ℕ
      [Meta.synthInstance] new goal ConditionallyCompleteLattice ℕ
        [Meta.synthInstance.instances] #[@CompleteLattice.toConditionallyCompleteLattice, @ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice]
    [Meta.synthInstance] ✅ apply @ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice to ConditionallyCompleteLattice
          ℕ
      [Meta.synthInstance.tryResolve] ✅ ConditionallyCompleteLattice ℕ ≟ ConditionallyCompleteLattice ℕ
      [Meta.synthInstance] new goal ConditionallyCompleteLinearOrder ℕ
        [Meta.synthInstance.instances] #[@ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder]
    [Meta.synthInstance] ✅ apply @ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder to ConditionallyCompleteLinearOrder
          ℕ
      [Meta.synthInstance.tryResolve] ✅ ConditionallyCompleteLinearOrder ℕ ≟ ConditionallyCompleteLinearOrder ℕ
      [Meta.synthInstance] new goal ConditionallyCompleteLinearOrderBot ℕ
        [Meta.synthInstance.instances] #[@CompleteLinearOrder.toConditionallyCompleteLinearOrderBot, Nat.instConditionallyCompleteLinearOrderBotNat]
    [Meta.synthInstance] ✅ apply Nat.instConditionallyCompleteLinearOrderBotNat to ConditionallyCompleteLinearOrderBot ℕ
      [Meta.synthInstance.tryResolve] ✅ ConditionallyCompleteLinearOrderBot ℕ ≟ ConditionallyCompleteLinearOrderBot ℕ
    [Meta.synthInstance.resume] propagating ConditionallyCompleteLinearOrderBot
          ℕ to subgoal ConditionallyCompleteLinearOrderBot ℕ of ConditionallyCompleteLinearOrder ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.resume] propagating ConditionallyCompleteLinearOrder
          ℕ to subgoal ConditionallyCompleteLinearOrder ℕ of ConditionallyCompleteLattice ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.resume] propagating ConditionallyCompleteLattice
          ℕ to subgoal ConditionallyCompleteLattice ℕ of Lattice ℕ
      [Meta.synthInstance.resume] size: 3
    [Meta.synthInstance] ✅ apply @CompleteLinearOrder.toConditionallyCompleteLinearOrderBot to ConditionallyCompleteLinearOrderBot
          ℕ
      [Meta.synthInstance.tryResolve] ✅ ConditionallyCompleteLinearOrderBot ℕ ≟ ConditionallyCompleteLinearOrderBot ℕ
      [Meta.synthInstance] no instances for CompleteLinearOrder ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @CompleteLattice.toConditionallyCompleteLattice to ConditionallyCompleteLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ ConditionallyCompleteLattice ℕ ≟ ConditionallyCompleteLattice ℕ
    [Meta.synthInstance] ✅ apply @CompleteLattice.toLattice to Lattice ℕ
      [Meta.synthInstance.tryResolve] ✅ Lattice ℕ ≟ Lattice ℕ
    [Meta.synthInstance] ✅ apply @GeneralizedCoheytingAlgebra.toLattice to Lattice ℕ
      [Meta.synthInstance.tryResolve] ✅ Lattice ℕ ≟ Lattice ℕ
      [Meta.synthInstance] new goal GeneralizedCoheytingAlgebra ℕ
        [Meta.synthInstance.instances] #[@GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra, @CoheytingAlgebra.toGeneralizedCoheytingAlgebra]
    [Meta.synthInstance] ✅ apply @CoheytingAlgebra.toGeneralizedCoheytingAlgebra to GeneralizedCoheytingAlgebra ℕ
      [Meta.synthInstance.tryResolve] ✅ GeneralizedCoheytingAlgebra ℕ ≟ GeneralizedCoheytingAlgebra ℕ
      [Meta.synthInstance] new goal CoheytingAlgebra ℕ
        [Meta.synthInstance.instances] #[@BiheytingAlgebra.toCoheytingAlgebra]
    [Meta.synthInstance] ✅ apply @BiheytingAlgebra.toCoheytingAlgebra to CoheytingAlgebra ℕ
      [Meta.synthInstance.tryResolve] ✅ CoheytingAlgebra ℕ ≟ CoheytingAlgebra ℕ
      [Meta.synthInstance] new goal BiheytingAlgebra ℕ
        [Meta.synthInstance.instances] #[@BooleanAlgebra.toBiheytingAlgebra]
    [Meta.synthInstance] ✅ apply @BooleanAlgebra.toBiheytingAlgebra to BiheytingAlgebra ℕ
      [Meta.synthInstance.tryResolve] ✅ BiheytingAlgebra ℕ ≟ BiheytingAlgebra ℕ
      [Meta.synthInstance] new goal BooleanAlgebra ℕ
        [Meta.synthInstance.instances] #[@CompleteBooleanAlgebra.toBooleanAlgebra]
    [Meta.synthInstance] ✅ apply @CompleteBooleanAlgebra.toBooleanAlgebra to BooleanAlgebra ℕ
      [Meta.synthInstance.tryResolve] ✅ BooleanAlgebra ℕ ≟ BooleanAlgebra ℕ
    [Meta.synthInstance] ✅ apply @GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra to GeneralizedCoheytingAlgebra
          ℕ
      [Meta.synthInstance.tryResolve] ✅ GeneralizedCoheytingAlgebra ℕ ≟ GeneralizedCoheytingAlgebra ℕ
      [Meta.synthInstance] new goal GeneralizedBooleanAlgebra ℕ
        [Meta.synthInstance.instances] #[@BooleanAlgebra.toGeneralizedBooleanAlgebra]
    [Meta.synthInstance] ✅ apply @BooleanAlgebra.toGeneralizedBooleanAlgebra to GeneralizedBooleanAlgebra ℕ
      [Meta.synthInstance.tryResolve] ✅ GeneralizedBooleanAlgebra ℕ ≟ GeneralizedBooleanAlgebra ℕ
    [Meta.synthInstance] ✅ apply @GeneralizedHeytingAlgebra.toLattice to Lattice ℕ
      [Meta.synthInstance.tryResolve] ✅ Lattice ℕ ≟ Lattice ℕ
      [Meta.synthInstance] new goal GeneralizedHeytingAlgebra ℕ
        [Meta.synthInstance.instances] #[@HeytingAlgebra.toGeneralizedHeytingAlgebra]
    [Meta.synthInstance] ✅ apply @HeytingAlgebra.toGeneralizedHeytingAlgebra to GeneralizedHeytingAlgebra ℕ
      [Meta.synthInstance.tryResolve] ✅ GeneralizedHeytingAlgebra ℕ ≟ GeneralizedHeytingAlgebra ℕ
      [Meta.synthInstance] new goal HeytingAlgebra ℕ
        [Meta.synthInstance.instances] #[@BiheytingAlgebra.toHeytingAlgebra]
    [Meta.synthInstance] ✅ apply @BiheytingAlgebra.toHeytingAlgebra to HeytingAlgebra ℕ
      [Meta.synthInstance.tryResolve] ✅ HeytingAlgebra ℕ ≟ HeytingAlgebra ℕ
    [Meta.synthInstance] ✅ apply @DistribLattice.toLattice to Lattice ℕ
      [Meta.synthInstance.tryResolve] ✅ Lattice ℕ ≟ Lattice ℕ
      [Meta.synthInstance] new goal DistribLattice ℕ
        [Meta.synthInstance.instances] #[@instDistribLattice, @GeneralizedHeytingAlgebra.toDistribLattice, @GeneralizedCoheytingAlgebra.toDistribLattice, @CoheytingAlgebra.toDistribLattice, @Frame.toDistribLattice, @Coframe.toDistribLattice, @GeneralizedBooleanAlgebra.toDistribLattice, @BooleanAlgebra.toDistribLattice, instDistribLatticeNat]
    [Meta.synthInstance] ✅ apply instDistribLatticeNat to DistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ DistribLattice ℕ ≟ DistribLattice ℕ
    [Meta.synthInstance.resume] propagating DistribLattice ℕ to subgoal DistribLattice ℕ of Lattice ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @BooleanAlgebra.toDistribLattice to DistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ DistribLattice ℕ ≟ DistribLattice ℕ
    [Meta.synthInstance] ✅ apply @GeneralizedBooleanAlgebra.toDistribLattice to DistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ DistribLattice ℕ ≟ DistribLattice ℕ
    [Meta.synthInstance] ✅ apply @Coframe.toDistribLattice to DistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ DistribLattice ℕ ≟ DistribLattice ℕ
    [Meta.synthInstance] ✅ apply @Frame.toDistribLattice to DistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ DistribLattice ℕ ≟ DistribLattice ℕ
    [Meta.synthInstance] ✅ apply @CoheytingAlgebra.toDistribLattice to DistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ DistribLattice ℕ ≟ DistribLattice ℕ
    [Meta.synthInstance] ✅ apply @GeneralizedCoheytingAlgebra.toDistribLattice to DistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ DistribLattice ℕ ≟ DistribLattice ℕ
    [Meta.synthInstance] ✅ apply @GeneralizedHeytingAlgebra.toDistribLattice to DistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ DistribLattice ℕ ≟ DistribLattice ℕ
    [Meta.synthInstance] ✅ apply @instDistribLattice to DistribLattice ℕ
      [Meta.synthInstance.tryResolve] ✅ DistribLattice ℕ ≟ DistribLattice ℕ
      [Meta.synthInstance] new goal LinearOrder ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedAddCommMonoid.toLinearOrder, @LinearOrderedCommMonoid.toLinearOrder, @LinearOrderedAddCommGroup.toLinearOrder, @LinearOrderedCommGroup.toLinearOrder, @LinearOrderedRing.toLinearOrder, @CompleteLinearOrder.toLinearOrder, instLinearOrder, Nat.linearOrder]
    [Meta.synthInstance] ✅ apply Nat.linearOrder to LinearOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrder ℕ ≟ LinearOrder ℕ
    [Meta.synthInstance.resume] propagating LinearOrder ℕ to subgoal LinearOrder ℕ of DistribLattice ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply instLinearOrder to LinearOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrder ℕ ≟ LinearOrder ℕ
    [Meta.synthInstance.resume] propagating ConditionallyCompleteLinearOrder
          ℕ to subgoal ConditionallyCompleteLinearOrder ℕ of LinearOrder ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance] ✅ apply @CompleteLinearOrder.toLinearOrder to LinearOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrder ℕ ≟ LinearOrder ℕ
      [Meta.synthInstance] no instances for CompleteLinearOrder ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @LinearOrderedRing.toLinearOrder to LinearOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrder ℕ ≟ LinearOrder ℕ
    [Meta.synthInstance] ✅ apply @LinearOrderedCommGroup.toLinearOrder to LinearOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrder ℕ ≟ LinearOrder ℕ
      [Meta.synthInstance] no instances for LinearOrderedCommGroup ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @LinearOrderedAddCommGroup.toLinearOrder to LinearOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrder ℕ ≟ LinearOrder ℕ
    [Meta.synthInstance] ✅ apply @LinearOrderedCommMonoid.toLinearOrder to LinearOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrder ℕ ≟ LinearOrder ℕ
    [Meta.synthInstance.resume] propagating LinearOrderedCommMonoid
          ℕ to subgoal LinearOrderedCommMonoid ℕ of LinearOrder ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance] ✅ apply @LinearOrderedAddCommMonoid.toLinearOrder to LinearOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ LinearOrder ℕ ≟ LinearOrder ℕ
    [Meta.synthInstance.resume] propagating LinearOrderedAddCommMonoid
          ℕ to subgoal LinearOrderedAddCommMonoid ℕ of LinearOrder ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance] ✅ apply @LinearOrder.toLattice to Lattice ℕ
      [Meta.synthInstance.tryResolve] ✅ Lattice ℕ ≟ Lattice ℕ
    [Meta.synthInstance.resume] propagating LinearOrder ℕ to subgoal LinearOrder ℕ of Lattice ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @SemilatticeSup.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] new goal SemilatticeSup ℕ
        [Meta.synthInstance.instances] #[@CanonicallyLinearOrderedCommMonoid.semilatticeSup, @CanonicallyLinearOrderedAddCommMonoid.semilatticeSup, @Lattice.toSemilatticeSup, @IdemSemiring.toSemilatticeSup, @IdemCommSemiring.toSemilatticeSup]
    [Meta.synthInstance] ✅ apply @IdemCommSemiring.toSemilatticeSup to SemilatticeSup ℕ
      [Meta.synthInstance.tryResolve] ✅ SemilatticeSup ℕ ≟ SemilatticeSup ℕ
      [Meta.synthInstance] no instances for IdemCommSemiring ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @IdemSemiring.toSemilatticeSup to SemilatticeSup ℕ
      [Meta.synthInstance.tryResolve] ✅ SemilatticeSup ℕ ≟ SemilatticeSup ℕ
    [Meta.synthInstance] ✅ apply @Lattice.toSemilatticeSup to SemilatticeSup ℕ
      [Meta.synthInstance.tryResolve] ✅ SemilatticeSup ℕ ≟ SemilatticeSup ℕ
    [Meta.synthInstance.resume] propagating Lattice ℕ to subgoal Lattice ℕ of SemilatticeSup ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.resume] propagating SemilatticeSup ℕ to subgoal SemilatticeSup ℕ of PartialOrder ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.semilatticeSup to SemilatticeSup ℕ
      [Meta.synthInstance.tryResolve] ✅ SemilatticeSup ℕ ≟ SemilatticeSup ℕ
    [Meta.synthInstance.resume] propagating CanonicallyLinearOrderedAddCommMonoid
          ℕ to subgoal CanonicallyLinearOrderedAddCommMonoid ℕ of SemilatticeSup ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @CanonicallyLinearOrderedCommMonoid.semilatticeSup to SemilatticeSup ℕ
      [Meta.synthInstance.tryResolve] ✅ SemilatticeSup ℕ ≟ SemilatticeSup ℕ
      [Meta.synthInstance] no instances for CanonicallyLinearOrderedCommMonoid ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @LinearOrder.toPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
    [Meta.synthInstance.resume] propagating LinearOrder ℕ to subgoal LinearOrder ℕ of PartialOrder ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @SetLike.instPartialOrder to PartialOrder ℕ
      [Meta.synthInstance.tryResolve] ✅ PartialOrder ℕ ≟ PartialOrder ℕ
      [Meta.synthInstance] no instances for SetLike ℕ _tc.1
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @Field.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
      [Meta.synthInstance] new goal Field ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedField.toField]
    [Meta.synthInstance] ✅ apply @LinearOrderedField.toField to Field ℕ
      [Meta.synthInstance.tryResolve] ✅ Field ℕ ≟ Field ℕ
      [Meta.synthInstance] no instances for LinearOrderedField ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @Semifield.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
      [Meta.synthInstance] new goal Semifield ℕ
        [Meta.synthInstance.instances] #[@Field.toSemifield, @LinearOrderedSemifield.toSemifield]
    [Meta.synthInstance] ✅ apply @LinearOrderedSemifield.toSemifield to Semifield ℕ
      [Meta.synthInstance.tryResolve] ✅ Semifield ℕ ≟ Semifield ℕ
    [Meta.synthInstance] ✅ apply @Field.toSemifield to Semifield ℕ
      [Meta.synthInstance.tryResolve] ✅ Semifield ℕ ≟ Semifield ℕ
    [Meta.synthInstance] ✅ apply @DivisionRing.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
      [Meta.synthInstance] new goal DivisionRing ℕ
        [Meta.synthInstance.instances] #[@Field.toDivisionRing]
    [Meta.synthInstance] ✅ apply @Field.toDivisionRing to DivisionRing ℕ
      [Meta.synthInstance.tryResolve] ✅ DivisionRing ℕ ≟ DivisionRing ℕ
    [Meta.synthInstance] ✅ apply @DivisionSemiring.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
      [Meta.synthInstance] new goal DivisionSemiring ℕ
        [Meta.synthInstance.instances] #[@DivisionRing.toDivisionSemiring, @Semifield.toDivisionSemiring]
    [Meta.synthInstance] ✅ apply @Semifield.toDivisionSemiring to DivisionSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ DivisionSemiring ℕ ≟ DivisionSemiring ℕ
    [Meta.synthInstance] ✅ apply @DivisionRing.toDivisionSemiring to DivisionSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ DivisionSemiring ℕ ≟ DivisionSemiring ℕ
    [Meta.synthInstance] ✅ apply @instNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
      [Meta.synthInstance] new goal AddMonoidWithOne ℕ
        [Meta.synthInstance.instances] #[@AddCommMonoidWithOne.toAddMonoidWithOne, @AddGroupWithOne.toAddMonoidWithOne]
    [Meta.synthInstance] ✅ apply @AddGroupWithOne.toAddMonoidWithOne to AddMonoidWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddMonoidWithOne ℕ ≟ AddMonoidWithOne ℕ
      [Meta.synthInstance] new goal AddGroupWithOne ℕ
        [Meta.synthInstance.instances] #[@AddCommGroupWithOne.toAddGroupWithOne, @Ring.toAddGroupWithOne]
    [Meta.synthInstance] ✅ apply @Ring.toAddGroupWithOne to AddGroupWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddGroupWithOne ℕ ≟ AddGroupWithOne ℕ
      [Meta.synthInstance] new goal Ring ℕ
        [Meta.synthInstance.instances] #[@CommRing.toRing, @OrderedRing.toRing, @StrictOrderedRing.toRing, @DivisionRing.toRing]
    [Meta.synthInstance] ✅ apply @DivisionRing.toRing to Ring ℕ
      [Meta.synthInstance.tryResolve] ✅ Ring ℕ ≟ Ring ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedRing.toRing to Ring ℕ
      [Meta.synthInstance.tryResolve] ✅ Ring ℕ ≟ Ring ℕ
    [Meta.synthInstance] ✅ apply @OrderedRing.toRing to Ring ℕ
      [Meta.synthInstance.tryResolve] ✅ Ring ℕ ≟ Ring ℕ
    [Meta.synthInstance] ✅ apply @CommRing.toRing to Ring ℕ
      [Meta.synthInstance.tryResolve] ✅ Ring ℕ ≟ Ring ℕ
      [Meta.synthInstance] new goal CommRing ℕ
        [Meta.synthInstance.instances] #[@OrderedCommRing.toCommRing, @StrictOrderedCommRing.toCommRing, @Field.toCommRing]
    [Meta.synthInstance] ✅ apply @Field.toCommRing to CommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ CommRing ℕ ≟ CommRing ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedCommRing.toCommRing to CommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ CommRing ℕ ≟ CommRing ℕ
    [Meta.synthInstance] ✅ apply @OrderedCommRing.toCommRing to CommRing ℕ
      [Meta.synthInstance.tryResolve] ✅ CommRing ℕ ≟ CommRing ℕ
    [Meta.synthInstance] ✅ apply @AddCommGroupWithOne.toAddGroupWithOne to AddGroupWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddGroupWithOne ℕ ≟ AddGroupWithOne ℕ
      [Meta.synthInstance] new goal AddCommGroupWithOne ℕ
        [Meta.synthInstance.instances] #[@CommRing.toAddCommGroupWithOne, @NonAssocRing.toAddCommGroupWithOne]
    [Meta.synthInstance] ✅ apply @NonAssocRing.toAddCommGroupWithOne to AddCommGroupWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddCommGroupWithOne ℕ ≟ AddCommGroupWithOne ℕ
      [Meta.synthInstance] new goal NonAssocRing ℕ
        [Meta.synthInstance.instances] #[@Ring.toNonAssocRing]
    [Meta.synthInstance] ✅ apply @Ring.toNonAssocRing to NonAssocRing ℕ
      [Meta.synthInstance.tryResolve] ✅ NonAssocRing ℕ ≟ NonAssocRing ℕ
    [Meta.synthInstance] ✅ apply @CommRing.toAddCommGroupWithOne to AddCommGroupWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddCommGroupWithOne ℕ ≟ AddCommGroupWithOne ℕ
    [Meta.synthInstance] ✅ apply @AddCommMonoidWithOne.toAddMonoidWithOne to AddMonoidWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddMonoidWithOne ℕ ≟ AddMonoidWithOne ℕ
      [Meta.synthInstance] new goal AddCommMonoidWithOne ℕ
        [Meta.synthInstance.instances] #[@AddCommGroupWithOne.toAddCommMonoidWithOne, @NonAssocSemiring.toAddCommMonoidWithOne]
    [Meta.synthInstance] ✅ apply @NonAssocSemiring.toAddCommMonoidWithOne to AddCommMonoidWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddCommMonoidWithOne ℕ ≟ AddCommMonoidWithOne ℕ
      [Meta.synthInstance] new goal NonAssocSemiring ℕ
        [Meta.synthInstance.instances] #[@NonAssocRing.toNonAssocSemiring, @Semiring.toNonAssocSemiring]
    [Meta.synthInstance] ✅ apply @Semiring.toNonAssocSemiring to NonAssocSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ NonAssocSemiring ℕ ≟ NonAssocSemiring ℕ
      [Meta.synthInstance] new goal Semiring ℕ
        [Meta.synthInstance.instances] #[@instSemiring, @Ring.toSemiring, @CommSemiring.toSemiring, @OrderedSemiring.toSemiring, @StrictOrderedSemiring.toSemiring, @DivisionSemiring.toSemiring, @IdemSemiring.toSemiring, Nat.semiring]
    [Meta.synthInstance] ✅ apply Nat.semiring to Semiring ℕ
      [Meta.synthInstance.tryResolve] ✅ Semiring ℕ ≟ Semiring ℕ
    [Meta.synthInstance.resume] propagating Semiring ℕ to subgoal Semiring ℕ of NonAssocSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance.resume] propagating NonAssocSemiring ℕ to subgoal NonAssocSemiring ℕ of AddCommMonoidWithOne ℕ
      [Meta.synthInstance.resume] size: 2
    [Meta.synthInstance.resume] propagating AddCommMonoidWithOne
          ℕ to subgoal AddCommMonoidWithOne ℕ of AddMonoidWithOne ℕ
      [Meta.synthInstance.resume] size: 3
    [Meta.synthInstance.resume] propagating AddMonoidWithOne ℕ to subgoal AddMonoidWithOne ℕ of Nontrivial ℕ
      [Meta.synthInstance.resume] size: 4
    [Meta.synthInstance] ✅ apply @IdemSemiring.toSemiring to Semiring ℕ
      [Meta.synthInstance.tryResolve] ✅ Semiring ℕ ≟ Semiring ℕ
    [Meta.synthInstance] ✅ apply @DivisionSemiring.toSemiring to Semiring ℕ
      [Meta.synthInstance.tryResolve] ✅ Semiring ℕ ≟ Semiring ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedSemiring.toSemiring to Semiring ℕ
      [Meta.synthInstance.tryResolve] ✅ Semiring ℕ ≟ Semiring ℕ
    [Meta.synthInstance.resume] propagating StrictOrderedSemiring ℕ to subgoal StrictOrderedSemiring ℕ of Semiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @OrderedSemiring.toSemiring to Semiring ℕ
      [Meta.synthInstance.tryResolve] ✅ Semiring ℕ ≟ Semiring ℕ
    [Meta.synthInstance.resume] propagating OrderedSemiring ℕ to subgoal OrderedSemiring ℕ of Semiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @CommSemiring.toSemiring to Semiring ℕ
      [Meta.synthInstance.tryResolve] ✅ Semiring ℕ ≟ Semiring ℕ
      [Meta.synthInstance] new goal CommSemiring ℕ
        [Meta.synthInstance.instances] #[@CommRing.toCommSemiring, @OrderedCommSemiring.toCommSemiring, @StrictOrderedCommSemiring.toCommSemiring, @CanonicallyOrderedCommSemiring.toCommSemiring, @Semifield.toCommSemiring, @IdemCommSemiring.toCommSemiring, Nat.commSemiring]
    [Meta.synthInstance] ✅ apply Nat.commSemiring to CommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ CommSemiring ℕ ≟ CommSemiring ℕ
    [Meta.synthInstance.resume] propagating CommSemiring ℕ to subgoal CommSemiring ℕ of Semiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @IdemCommSemiring.toCommSemiring to CommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ CommSemiring ℕ ≟ CommSemiring ℕ
      [Meta.synthInstance] no instances for IdemCommSemiring ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @Semifield.toCommSemiring to CommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ CommSemiring ℕ ≟ CommSemiring ℕ
    [Meta.synthInstance] ✅ apply @CanonicallyOrderedCommSemiring.toCommSemiring to CommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ CommSemiring ℕ ≟ CommSemiring ℕ
    [Meta.synthInstance.resume] propagating CanonicallyOrderedCommSemiring
          ℕ to subgoal CanonicallyOrderedCommSemiring ℕ of CommSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @StrictOrderedCommSemiring.toCommSemiring to CommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ CommSemiring ℕ ≟ CommSemiring ℕ
    [Meta.synthInstance.resume] propagating StrictOrderedCommSemiring
          ℕ to subgoal StrictOrderedCommSemiring ℕ of CommSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @OrderedCommSemiring.toCommSemiring to CommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ CommSemiring ℕ ≟ CommSemiring ℕ
    [Meta.synthInstance.resume] propagating OrderedCommSemiring ℕ to subgoal OrderedCommSemiring ℕ of CommSemiring ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @CommRing.toCommSemiring to CommSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ CommSemiring ℕ ≟ CommSemiring ℕ
    [Meta.synthInstance] ✅ apply @Ring.toSemiring to Semiring ℕ
      [Meta.synthInstance.tryResolve] ✅ Semiring ℕ ≟ Semiring ℕ
    [Meta.synthInstance] ✅ apply @instSemiring to Semiring ℕ
      [Meta.synthInstance.tryResolve] ✅ Semiring ℕ ≟ Semiring ℕ
    [Meta.synthInstance] ✅ apply @NonAssocRing.toNonAssocSemiring to NonAssocSemiring ℕ
      [Meta.synthInstance.tryResolve] ✅ NonAssocSemiring ℕ ≟ NonAssocSemiring ℕ
    [Meta.synthInstance] ✅ apply @AddCommGroupWithOne.toAddCommMonoidWithOne to AddCommMonoidWithOne ℕ
      [Meta.synthInstance.tryResolve] ✅ AddCommMonoidWithOne ℕ ≟ AddCommMonoidWithOne ℕ
    [Meta.synthInstance] ✅ apply @LinearOrderedCommGroupWithZero.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
      [Meta.synthInstance] no instances for LinearOrderedCommGroupWithZero ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @StrictOrderedRing.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
    [Meta.synthInstance] ✅ apply @StrictOrderedSemiring.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
    [Meta.synthInstance.resume] propagating StrictOrderedSemiring ℕ to subgoal StrictOrderedSemiring ℕ of Nontrivial ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @IsDomain.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
    [Meta.synthInstance.resume] propagating Semiring ℕ to subgoal Semiring ℕ of Nontrivial ℕ
      [Meta.synthInstance.resume] size: 1
      [Meta.synthInstance] new goal IsDomain ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedRing.isDomain, @DivisionRing.isDomain, @Field.isDomain]
    [Meta.synthInstance] ❌ apply @Field.isDomain to IsDomain ℕ
      [Meta.synthInstance.tryResolve] ❌ IsDomain ℕ ≟ IsDomain ?m.909
        [Meta.synthInstance] ❌ Field ℕ
          [Meta.synthInstance] new goal Field ℕ
            [Meta.synthInstance.instances] #[@LinearOrderedField.toField]
          [Meta.synthInstance] ✅ apply @LinearOrderedField.toField to Field ℕ
            [Meta.synthInstance.tryResolve] ✅ Field ℕ ≟ Field ℕ
            [Meta.synthInstance] no instances for LinearOrderedField ℕ
              [Meta.synthInstance.instances] #[]
        [Meta.synthInstance] ❌ Field ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ Field ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ Field ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ Field ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ Field ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ Field ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ Field ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ Field ℕ
          [Meta.synthInstance] result <not-available> (cached)
    [Meta.synthInstance] ❌ apply @DivisionRing.isDomain to IsDomain ℕ
      [Meta.synthInstance.tryResolve] ❌ IsDomain ℕ ≟ IsDomain ?m.928
        [Meta.synthInstance] ❌ DivisionRing ℕ
          [Meta.synthInstance] new goal DivisionRing ℕ
            [Meta.synthInstance.instances] #[@Field.toDivisionRing]
          [Meta.synthInstance] ✅ apply @Field.toDivisionRing to DivisionRing ℕ
            [Meta.synthInstance.tryResolve] ✅ DivisionRing ℕ ≟ DivisionRing ℕ
            [Meta.synthInstance] new goal Field ℕ
              [Meta.synthInstance.instances] #[@LinearOrderedField.toField]
          [Meta.synthInstance] ✅ apply @LinearOrderedField.toField to Field ℕ
            [Meta.synthInstance.tryResolve] ✅ Field ℕ ≟ Field ℕ
            [Meta.synthInstance] no instances for LinearOrderedField ℕ
              [Meta.synthInstance.instances] #[]
        [Meta.synthInstance] ❌ DivisionRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ DivisionRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ DivisionRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ DivisionRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ DivisionRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ DivisionRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ DivisionRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
    [Meta.synthInstance] ❌ apply @LinearOrderedRing.isDomain to IsDomain ℕ
      [Meta.synthInstance.tryResolve] ❌ IsDomain ℕ ≟ IsDomain ?m.939
        [Meta.synthInstance] ❌ LinearOrderedRing ℕ
          [Meta.synthInstance] new goal LinearOrderedRing ℕ
            [Meta.synthInstance.instances] #[@LinearOrderedCommRing.toLinearOrderedRing]
          [Meta.synthInstance] ✅ apply @LinearOrderedCommRing.toLinearOrderedRing to LinearOrderedRing ℕ
            [Meta.synthInstance.tryResolve] ✅ LinearOrderedRing ℕ ≟ LinearOrderedRing ℕ
            [Meta.synthInstance] new goal LinearOrderedCommRing ℕ
              [Meta.synthInstance.instances] #[@LinearOrderedField.toLinearOrderedCommRing]
          [Meta.synthInstance] ✅ apply @LinearOrderedField.toLinearOrderedCommRing to LinearOrderedCommRing ℕ
            [Meta.synthInstance.tryResolve] ✅ LinearOrderedCommRing ℕ ≟ LinearOrderedCommRing ℕ
            [Meta.synthInstance] no instances for LinearOrderedField ℕ
              [Meta.synthInstance.instances] #[]
        [Meta.synthInstance] ❌ LinearOrderedRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ LinearOrderedRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ LinearOrderedRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ LinearOrderedRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ LinearOrderedRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ LinearOrderedRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
        [Meta.synthInstance] ❌ LinearOrderedRing ℕ
          [Meta.synthInstance] result <not-available> (cached)
    [Meta.synthInstance] ✅ apply @LinearOrderedAddCommGroupWithTop.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
      [Meta.synthInstance] no instances for LinearOrderedAddCommGroupWithTop ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @CommGroupWithZero.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
      [Meta.synthInstance] new goal CommGroupWithZero ℕ
        [Meta.synthInstance.instances] #[@LinearOrderedCommGroupWithZero.toCommGroupWithZero, @Semifield.toCommGroupWithZero]
    [Meta.synthInstance] ✅ apply @Semifield.toCommGroupWithZero to CommGroupWithZero ℕ
      [Meta.synthInstance.tryResolve] ✅ CommGroupWithZero ℕ ≟ CommGroupWithZero ℕ
    [Meta.synthInstance] ✅ apply @LinearOrderedCommGroupWithZero.toCommGroupWithZero to CommGroupWithZero ℕ
      [Meta.synthInstance.tryResolve] ✅ CommGroupWithZero ℕ ≟ CommGroupWithZero ℕ
      [Meta.synthInstance] no instances for LinearOrderedCommGroupWithZero ℕ
        [Meta.synthInstance.instances] #[]
    [Meta.synthInstance] ✅ apply @GroupWithZero.toNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
      [Meta.synthInstance] new goal GroupWithZero ℕ
        [Meta.synthInstance.instances] #[@CommGroupWithZero.toGroupWithZero, @DivisionSemiring.toGroupWithZero]
    [Meta.synthInstance] ✅ apply @DivisionSemiring.toGroupWithZero to GroupWithZero ℕ
      [Meta.synthInstance.tryResolve] ✅ GroupWithZero ℕ ≟ GroupWithZero ℕ
    [Meta.synthInstance] ✅ apply @CommGroupWithZero.toGroupWithZero to GroupWithZero ℕ
      [Meta.synthInstance.tryResolve] ✅ GroupWithZero ℕ ≟ GroupWithZero ℕ
    [Meta.synthInstance] ✅ apply Infinite.instNontrivial to Nontrivial ℕ
      [Meta.synthInstance.tryResolve] ✅ Nontrivial ℕ ≟ Nontrivial ℕ
      [Meta.synthInstance] new goal Infinite ℕ
        [Meta.synthInstance.instances] #[@Denumerable.instInfinite, instInfiniteNat]
    [Meta.synthInstance] ✅ apply instInfiniteNat to Infinite ℕ
      [Meta.synthInstance.tryResolve] ✅ Infinite ℕ ≟ Infinite ℕ
    [Meta.synthInstance.resume] propagating Infinite ℕ to subgoal Infinite ℕ of Nontrivial ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @Denumerable.instInfinite to Infinite ℕ
      [Meta.synthInstance.tryResolve] ✅ Infinite ℕ ≟ Infinite ℕ
      [Meta.synthInstance] new goal Denumerable ℕ
        [Meta.synthInstance.instances] #[Denumerable.nat]
    [Meta.synthInstance] ✅ apply Denumerable.nat to Denumerable ℕ
      [Meta.synthInstance.tryResolve] ✅ Denumerable ℕ ≟ Denumerable ℕ
    [Meta.synthInstance.resume] propagating Denumerable ℕ to subgoal Denumerable ℕ of Infinite ℕ
      [Meta.synthInstance.resume] size: 1
    [Meta.synthInstance] ✅ apply @StrictOrderedSemiring.to_charZero to CharZero ℕ
      [Meta.synthInstance.tryResolve] ✅ CharZero ℕ ≟ CharZero ℕ
        [Meta.synthInstance] ✅ StrictOrderedSemiring ℕ
          [Meta.synthInstance] new goal StrictOrderedSemiring ℕ
            [Meta.synthInstance.instances] #[@StrictOrderedRing.toStrictOrderedSemiring, @StrictOrderedCommSemiring.toStrictOrderedSemiring, @LinearOrderedSemiring.toStrictOrderedSemiring, Nat.strictOrderedSemiring]
          [Meta.synthInstance] ✅ apply Nat.strictOrderedSemiring to StrictOrderedSemiring ℕ
            [Meta.synthInstance.tryResolve] ✅ StrictOrderedSemiring ℕ ≟ StrictOrderedSemiring ℕ
          [Meta.synthInstance] result Nat.strictOrderedSemiring
    [Meta.synthInstance] result StrictOrderedSemiring.to_charZero