Skip to content

Instantly share code, notes, and snippets.

@collares
Last active October 19, 2023 17:12
Show Gist options
  • Save collares/8590a08c79eed16879a823233b03ba70 to your computer and use it in GitHub Desktop.
Save collares/8590a08c79eed16879a823233b03ba70 to your computer and use it in GitHub Desktop.
CharZero instance
‘#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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment