Skip to content

Instantly share code, notes, and snippets.

@fpvandoorn

fpvandoorn/out.txt Secret

Created April 26, 2024 12:25
Show Gist options
  • Save fpvandoorn/b255ae141a45151a767594773dc54aa4 to your computer and use it in GitHub Desktop.
Save fpvandoorn/b255ae141a45151a767594773dc54aa4 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
out.txt
[Elab.command] [0.576432s] example (A : Type*) : Subsingleton (Fin 2 → ℝ) := by infer_instance ▼
[Meta.synthInstance] [0.000209s] ✅ OfNat ℕ 2 ▶
[step] [0.572786s] infer_instance ▼
[] [0.572775s] infer_instance ▼
[] [0.572768s] infer_instance ▼
[] [0.572752s] exact inferInstance✝ ▼
[] [0.572719s] expected type: Subsingleton (Fin 2 → ℝ), term
inferInstance✝ ▼
[Meta.synthInstance] [0.572470s] ❌ Subsingleton (Fin 2 → ℝ) ▼
[] [0.000023s] new goal Subsingleton (Fin 2 → ℝ) ▶
[] [0.000148s] ✅ apply @instSubsingletonForAll to Subsingleton (Fin 2 → ℝ) ▶
[] [0.000057s] ❌ apply instSubsingleton to Subsingleton ℝ ▶
[] [0.000107s] ✅ apply @CharP.CharOne.subsingleton to Subsingleton ℝ ▶
[] [0.000105s] ✅ apply @Semiring.toNonAssocSemiring to NonAssocSemiring ℝ ▶
[] [0.000051s] ✅ apply Real.semiring to Semiring ℝ ▶
[resume] [0.000007s] propagating Semiring ℝ to subgoal Semiring ℝ of NonAssocSemiring ℝ ▶
[resume] [0.000032s] propagating NonAssocSemiring ℝ to subgoal NonAssocSemiring ℝ of Subsingleton ℝ ▶
[] [0.000072s] ❌ apply @DirectSum.GradeZero.semiring to Semiring ℝ ▶
[] [0.000067s] ✅ apply @IdemSemiring.toSemiring to Semiring ℝ ▶
[] [0.000084s] ✅ apply @KleeneAlgebra.toIdemSemiring to IdemSemiring ℝ ▶
[] [0.000060s] ✅ apply @IdemCommSemiring.toIdemSemiring to IdemSemiring ℝ ▶
[] [0.000068s] ✅ apply @DivisionSemiring.toSemiring to Semiring ℝ ▶
[] [0.000070s] ✅ apply @Semifield.toDivisionSemiring to DivisionSemiring ℝ ▶
[] [0.000068s] ✅ apply @LinearOrderedSemifield.toSemifield to Semifield ℝ ▶
[] [0.000063s] ✅ apply @CanonicallyLinearOrderedSemifield.toLinearOrderedSemifield to LinearOrderedSemifield ℝ ▶
[] [0.000067s] ✅ apply @LinearOrderedField.toLinearOrderedSemifield to LinearOrderedSemifield ℝ ▶
[] [0.000045s] ✅ apply Real.instLinearOrderedField to LinearOrderedField ℝ ▶
[resume] [0.000006s] propagating LinearOrderedField ℝ to subgoal LinearOrderedField ℝ of LinearOrderedSemifield ℝ ▶
[resume] [0.000004s] propagating LinearOrderedSemifield ℝ to subgoal LinearOrderedSemifield ℝ of Semifield ℝ ▶
[resume] [0.000004s] propagating Semifield ℝ to subgoal Semifield ℝ of DivisionSemiring ℝ ▶
[resume] [0.000004s] propagating DivisionSemiring ℝ to subgoal DivisionSemiring ℝ of Semiring ℝ ▶
[] [0.000063s] ✅ apply @ConditionallyCompleteLinearOrderedField.toLinearOrderedField to LinearOrderedField ℝ ▶
[] [0.000045s] ✅ apply instConditionallyCompleteLinearOrderedFieldReal to ConditionallyCompleteLinearOrderedField ℝ ▶
[resume] [0.000006s] propagating ConditionallyCompleteLinearOrderedField
ℝ to subgoal ConditionallyCompleteLinearOrderedField ℝ of LinearOrderedField ℝ ▶
[] [0.000062s] ✅ apply @NormedLinearOrderedField.toLinearOrderedField to LinearOrderedField ℝ ▶
[] [0.000048s] ✅ apply Real.normedLinearOrderedField to NormedLinearOrderedField ℝ ▶
[resume] [0.000005s] propagating NormedLinearOrderedField ℝ to subgoal NormedLinearOrderedField ℝ of LinearOrderedField ℝ ▶
[] [0.000287s] ✅ apply @Field.toSemifield to Semifield ℝ ▶
[] [0.000056s] ✅ apply Real.field to Field ℝ ▶
[resume] [0.000007s] propagating Field ℝ to subgoal Field ℝ of Semifield ℝ ▶
[] [0.000075s] ✅ apply @NormedField.toField to Field ℝ ▶
[] [0.000045s] ✅ apply Real.normedField to NormedField ℝ ▶
[resume] [0.000008s] propagating NormedField ℝ to subgoal NormedField ℝ of Field ℝ ▶
[] [0.000102s] ✅ apply @DenselyNormedField.toNormedField to NormedField ℝ ▶
[] [0.000051s] ✅ apply Real.denselyNormedField to DenselyNormedField ℝ ▶
[resume] [0.000006s] propagating DenselyNormedField ℝ to subgoal DenselyNormedField ℝ of NormedField ℝ ▶
[] [0.000089s] ✅ apply @RCLike.toDenselyNormedField to DenselyNormedField ℝ ▶
[] [0.000063s] ✅ apply Real.RCLike to RCLike ℝ ▶
[resume] [0.000006s] propagating RCLike ℝ to subgoal RCLike ℝ of DenselyNormedField ℝ ▶
[] [0.000073s] ✅ apply @NontriviallyNormedField.toNormedField to NormedField ℝ ▶
[] [0.000067s] ✅ apply @DenselyNormedField.toNontriviallyNormedField to NontriviallyNormedField ℝ ▶
[resume] [0.000006s] propagating DenselyNormedField ℝ to subgoal DenselyNormedField ℝ of NontriviallyNormedField ℝ ▶
[resume] [0.000005s] propagating NontriviallyNormedField ℝ to subgoal NontriviallyNormedField ℝ of NormedField ℝ ▶
[] [0.000050s] ✅ apply NormedLinearOrderedField.toNormedField to NormedField ℝ ▶
[resume] [0.000005s] propagating NormedLinearOrderedField ℝ to subgoal NormedLinearOrderedField ℝ of NormedField ℝ ▶
[] [0.000052s] ✅ apply @LinearOrderedField.toField to Field ℝ ▶
[resume] [0.000007s] propagating LinearOrderedField ℝ to subgoal LinearOrderedField ℝ of Field ℝ ▶
[] [0.000077s] ✅ apply littleWedderburn to Field ℝ ▶
[] [0.000052s] ✅ apply Real.instDivisionRingReal to DivisionRing ℝ ▶
[] 2136 more entries... ▼
[resume] [0.000026s] propagating DivisionRing ℝ to subgoal DivisionRing ℝ of Field ℝ ▶
[] [0.000121s] ✅ apply @IsAddKleinFour.instFinite to Finite ℝ ▶
[] [0.000048s] ✅ apply Real.instAddGroupReal to AddGroup ℝ ▶
[resume] [0.000016s] propagating AddGroup ℝ to subgoal AddGroup ℝ of Finite ℝ ▶
[] [0.000063s] ✅ apply @NormedAddGroup.toAddGroup to AddGroup ℝ ▶
[] [0.000154s] ✅ apply @NormedAddCommGroup.toNormedAddGroup to NormedAddGroup ℝ ▶
[] [0.000080s] ✅ apply Real.normedAddCommGroup to NormedAddCommGroup ℝ ▶
[resume] [0.000009s] propagating NormedAddCommGroup ℝ to subgoal NormedAddCommGroup ℝ of NormedAddGroup ℝ ▶
[resume] [0.000006s] propagating NormedAddGroup ℝ to subgoal NormedAddGroup ℝ of AddGroup ℝ ▶
[] [0.000082s] ✅ apply @NormedLatticeAddCommGroup.toNormedAddCommGroup to NormedAddCommGroup ℝ ▶
[] [0.000085s] ✅ apply Real.normedLatticeAddCommGroup to NormedLatticeAddCommGroup ℝ ▶
[resume] [0.000012s] propagating NormedLatticeAddCommGroup ℝ to subgoal NormedLatticeAddCommGroup ℝ of NormedAddCommGroup ℝ ▶
[] [0.000100s] ✅ apply @NormedOrderedAddGroup.toNormedAddCommGroup to NormedAddCommGroup ℝ ▶
[] [0.000087s] ✅ apply @NormedLinearOrderedAddGroup.toNormedOrderedAddGroup to NormedOrderedAddGroup ℝ ▶
[] [0.000072s] ✅ apply @NonUnitalNormedRing.toNormedAddCommGroup to NormedAddCommGroup ℝ ▶
[] [0.000081s] ✅ apply @NonUnitalNormedCommRing.toNonUnitalNormedRing to NonUnitalNormedRing ℝ ▶
[] [0.000073s] ✅ apply @NormedCommRing.toNonUnitalNormedCommRing to NonUnitalNormedCommRing ℝ ▶
[] [0.000049s] ✅ apply Real.normedCommRing to NormedCommRing ℝ ▶
[resume] [0.000006s] propagating NormedCommRing ℝ to subgoal NormedCommRing ℝ of NonUnitalNormedCommRing ℝ ▶
[resume] [0.000005s] propagating NonUnitalNormedCommRing ℝ to subgoal NonUnitalNormedCommRing ℝ of NonUnitalNormedRing ℝ ▶
[resume] [0.000006s] propagating NonUnitalNormedRing ℝ to subgoal NonUnitalNormedRing ℝ of NormedAddCommGroup ℝ ▶
[] [0.000054s] ✅ apply @NormedField.toNormedCommRing to NormedCommRing ℝ ▶
[resume] [0.000006s] propagating NormedField ℝ to subgoal NormedField ℝ of NormedCommRing ℝ ▶
[] [0.000162s] ✅ apply @NormedRing.toNonUnitalNormedRing to NonUnitalNormedRing ℝ ▶
[] [0.000083s] ✅ apply @NormedCommRing.toNormedRing to NormedRing ℝ ▶
[resume] [0.000010s] propagating NormedCommRing ℝ to subgoal NormedCommRing ℝ of NormedRing ℝ ▶
[resume] [0.000005s] propagating NormedRing ℝ to subgoal NormedRing ℝ of NonUnitalNormedRing ℝ ▶
[] [0.000071s] ✅ apply @NormedDivisionRing.toNormedRing to NormedRing ℝ ▶
[] [0.000062s] ✅ apply @NormedField.toNormedDivisionRing to NormedDivisionRing ℝ ▶
[resume] [0.000006s] propagating NormedField ℝ to subgoal NormedField ℝ of NormedDivisionRing ℝ ▶
[resume] [0.000005s] propagating NormedDivisionRing ℝ to subgoal NormedDivisionRing ℝ of NormedRing ℝ ▶
[] [0.000066s] ✅ apply @SeminormedAddGroup.toAddGroup to AddGroup ℝ ▶
[] [0.000074s] ✅ apply @SeminormedAddCommGroup.toSeminormedAddGroup to SeminormedAddGroup ℝ ▶
[] [0.000076s] ✅ apply @NonUnitalSeminormedRing.toSeminormedAddCommGroup to SeminormedAddCommGroup ℝ ▶
[] [0.000074s] ✅ apply @NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing to NonUnitalSeminormedRing ℝ ▶
[] [0.000080s] ✅ apply @SeminormedCommRing.toNonUnitalSeminormedCommRing to NonUnitalSeminormedCommRing ℝ ▶
[] [0.000062s] ✅ apply @NormedCommRing.toSeminormedCommRing to SeminormedCommRing ℝ ▶
[resume] [0.000008s] propagating NormedCommRing ℝ to subgoal NormedCommRing ℝ of SeminormedCommRing ℝ ▶
[resume] [0.000005s] propagating SeminormedCommRing ℝ to subgoal SeminormedCommRing ℝ of NonUnitalSeminormedCommRing ℝ ▶
[resume] [0.000005s] propagating NonUnitalSeminormedCommRing
ℝ to subgoal NonUnitalSeminormedCommRing ℝ of NonUnitalSeminormedRing ℝ ▶
[resume] [0.000005s] propagating NonUnitalSeminormedRing ℝ to subgoal NonUnitalSeminormedRing ℝ of SeminormedAddCommGroup ℝ ▶
[resume] [0.000004s] propagating SeminormedAddCommGroup ℝ to subgoal SeminormedAddCommGroup ℝ of SeminormedAddGroup ℝ ▶
[resume] [0.000005s] propagating SeminormedAddGroup ℝ to subgoal SeminormedAddGroup ℝ of AddGroup ℝ ▶
[] [0.000053s] ✅ apply @NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing to NonUnitalSeminormedCommRing ℝ ▶
[resume] [0.000006s] propagating NonUnitalNormedCommRing ℝ to subgoal NonUnitalNormedCommRing ℝ of NonUnitalSeminormedCommRing ℝ ▶
[] [0.000053s] ✅ apply @NonUnitalNormedRing.toNonUnitalSeminormedRing to NonUnitalSeminormedRing ℝ ▶
[resume] [0.000005s] propagating NonUnitalNormedRing ℝ to subgoal NonUnitalNormedRing ℝ of NonUnitalSeminormedRing ℝ ▶
[] [0.000064s] ✅ apply @SeminormedRing.toNonUnitalSeminormedRing to NonUnitalSeminormedRing ℝ ▶
[] [0.000058s] ✅ apply @SeminormedCommRing.toSeminormedRing to SeminormedRing ℝ ▶
[resume] [0.000005s] propagating SeminormedCommRing ℝ to subgoal SeminormedCommRing ℝ of SeminormedRing ℝ ▶
[] 2086 more entries... ▼
[resume] [0.000005s] propagating SeminormedRing ℝ to subgoal SeminormedRing ℝ of NonUnitalSeminormedRing ℝ ▶
[] [0.000051s] ✅ apply @NormedRing.toSeminormedRing to SeminormedRing ℝ ▶
[resume] [0.000005s] propagating NormedRing ℝ to subgoal NormedRing ℝ of SeminormedRing ℝ ▶
[] [0.000046s] ✅ apply @NormedAddCommGroup.toSeminormedAddCommGroup to SeminormedAddCommGroup ℝ ▶
[resume] [0.000005s] propagating NormedAddCommGroup ℝ to subgoal NormedAddCommGroup ℝ of SeminormedAddCommGroup ℝ ▶
[] [0.000047s] ✅ apply @NormedAddGroup.toSeminormedAddGroup to SeminormedAddGroup ℝ ▶
[resume] [0.000005s] propagating NormedAddGroup ℝ to subgoal NormedAddGroup ℝ of SeminormedAddGroup ℝ ▶
[] [0.000071s] ✅ apply @AddGroupWithOne.toAddGroup to AddGroup ℝ ▶
[] [0.000081s] ✅ apply @Ring.toAddGroupWithOne to AddGroupWithOne ℝ ▶
[] [0.000059s] ✅ apply Real.instRingReal to Ring ℝ ▶
[resume] [0.000006s] propagating Ring ℝ to subgoal Ring ℝ of AddGroupWithOne ℝ ▶
[resume] [0.000005s] propagating AddGroupWithOne ℝ to subgoal AddGroupWithOne ℝ of AddGroup ℝ ▶
[] [0.000053s] ✅ apply @NormedRing.toRing to Ring ℝ ▶
[resume] [0.000006s] propagating NormedRing ℝ to subgoal NormedRing ℝ of Ring ℝ ▶
[] [0.000047s] ✅ apply @SeminormedRing.toRing to Ring ℝ ▶
[resume] [0.000005s] propagating SeminormedRing ℝ to subgoal SeminormedRing ℝ of Ring ℝ ▶
[] [0.000074s] ❌ apply @DirectSum.GradeZero.ring to Ring ℝ ▶
[] [0.000073s] ✅ apply @BooleanRing.toRing to Ring ℝ ▶
[] [0.000060s] ✅ apply @DivisionRing.toRing to Ring ℝ ▶
[resume] [0.000007s] propagating DivisionRing ℝ to subgoal DivisionRing ℝ of Ring ℝ ▶
[] [0.000065s] ✅ apply @StrictOrderedRing.toRing to Ring ℝ ▶
[] [0.000050s] ✅ apply Real.strictOrderedRing to StrictOrderedRing ℝ ▶
[resume] [0.000006s] propagating StrictOrderedRing ℝ to subgoal StrictOrderedRing ℝ of Ring ℝ ▶
[] [0.000069s] ✅ apply @LinearOrderedRing.toStrictOrderedRing to StrictOrderedRing ℝ ▶
[] [0.000044s] ✅ apply Real.instLinearOrderedRingReal to LinearOrderedRing ℝ ▶
[resume] [0.000005s] propagating LinearOrderedRing ℝ to subgoal LinearOrderedRing ℝ of StrictOrderedRing ℝ ▶
[] [0.000133s] ✅ apply @LinearOrderedCommRing.toLinearOrderedRing to LinearOrderedRing ℝ ▶
[] [0.000052s] ✅ apply Real.linearOrderedCommRing to LinearOrderedCommRing ℝ ▶
[resume] [0.000007s] propagating LinearOrderedCommRing ℝ to subgoal LinearOrderedCommRing ℝ of LinearOrderedRing ℝ ▶
[] [0.000055s] ✅ apply @LinearOrderedField.toLinearOrderedCommRing to LinearOrderedCommRing ℝ ▶
[resume] [0.000006s] propagating LinearOrderedField ℝ to subgoal LinearOrderedField ℝ of LinearOrderedCommRing ℝ ▶
[] [0.000067s] ✅ apply @StrictOrderedCommRing.toStrictOrderedRing to StrictOrderedRing ℝ ▶
[] [0.000047s] ✅ apply Real.instStrictOrderedCommRingReal to StrictOrderedCommRing ℝ ▶
[resume] [0.000006s] propagating StrictOrderedCommRing ℝ to subgoal StrictOrderedCommRing ℝ of StrictOrderedRing ℝ ▶
[] [0.000054s] ✅ apply @LinearOrderedCommRing.toStrictOrderedCommRing to StrictOrderedCommRing ℝ ▶
[resume] [0.000006s] propagating LinearOrderedCommRing ℝ to subgoal LinearOrderedCommRing ℝ of StrictOrderedCommRing ℝ ▶
[] [0.000094s] ✅ apply @OrderedRing.toRing to Ring ℝ ▶
[] [0.000112s] ✅ apply Real.orderedRing to OrderedRing ℝ ▶
[resume] [0.000009s] propagating OrderedRing ℝ to subgoal OrderedRing ℝ of Ring ℝ ▶
[] [0.000088s] ✅ apply @OrderedCommRing.toOrderedRing to OrderedRing ℝ ▶
[] [0.000068s] ✅ apply @StrictOrderedCommRing.toOrderedCommRing to OrderedCommRing ℝ ▶
[resume] [0.000007s] propagating StrictOrderedCommRing ℝ to subgoal StrictOrderedCommRing ℝ of OrderedCommRing ℝ ▶
[resume] [0.000005s] propagating OrderedCommRing ℝ to subgoal OrderedCommRing ℝ of OrderedRing ℝ ▶
[] [0.000054s] ✅ apply @StrictOrderedRing.toOrderedRing to OrderedRing ℝ ▶
[resume] [0.000005s] propagating StrictOrderedRing ℝ to subgoal StrictOrderedRing ℝ of OrderedRing ℝ ▶
[] [0.000079s] ✅ apply @CommRing.toRing to Ring ℝ ▶
[] [0.000047s] ✅ apply Real.commRing to CommRing ℝ ▶
[resume] [0.000005s] propagating CommRing ℝ to subgoal CommRing ℝ of Ring ℝ ▶
[] [0.000082s] ❌ apply @DirectSum.GradeZero.commRing to CommRing ℝ ▶
[] [0.000069s] ✅ apply @EuclideanDomain.toCommRing to CommRing ℝ ▶
[] 2036 more entries... ▼
[] [0.000063s] ✅ apply @Field.toEuclideanDomain to EuclideanDomain ℝ ▶
[resume] [0.000006s] propagating Field ℝ to subgoal Field ℝ of EuclideanDomain ℝ ▶
[resume] [0.000005s] propagating EuclideanDomain ℝ to subgoal EuclideanDomain ℝ of CommRing ℝ ▶
[] [0.000047s] ✅ apply @Field.toCommRing to CommRing ℝ ▶
[resume] [0.000005s] propagating Field ℝ to subgoal Field ℝ of CommRing ℝ ▶
[] [0.000054s] ✅ apply @StrictOrderedCommRing.toCommRing to CommRing ℝ ▶
[resume] [0.000005s] propagating StrictOrderedCommRing ℝ to subgoal StrictOrderedCommRing ℝ of CommRing ℝ ▶
[] [0.000055s] ✅ apply @OrderedCommRing.toCommRing to CommRing ℝ ▶
[resume] [0.000005s] propagating OrderedCommRing ℝ to subgoal OrderedCommRing ℝ of CommRing ℝ ▶
[] [0.000051s] ✅ apply @SeminormedCommRing.toCommRing to CommRing ℝ ▶
[resume] [0.000005s] propagating SeminormedCommRing ℝ to subgoal SeminormedCommRing ℝ of CommRing ℝ ▶
[] [0.000062s] ✅ apply @BooleanRing.toCommRing to CommRing ℝ ▶
[] [0.000063s] ✅ apply @AddCommGroupWithOne.toAddGroupWithOne to AddGroupWithOne ℝ ▶
[] [0.000079s] ✅ apply @NonAssocRing.toAddCommGroupWithOne to AddCommGroupWithOne ℝ ▶
[] [0.000056s] ✅ apply @Ring.toNonAssocRing to NonAssocRing ℝ ▶
[resume] [0.000006s] propagating Ring ℝ to subgoal Ring ℝ of NonAssocRing ℝ ▶
[resume] [0.000005s] propagating NonAssocRing ℝ to subgoal NonAssocRing ℝ of AddCommGroupWithOne ℝ ▶
[resume] [0.000005s] propagating AddCommGroupWithOne ℝ to subgoal AddCommGroupWithOne ℝ of AddGroupWithOne ℝ ▶
[] [0.000051s] ✅ apply @CommRing.toAddCommGroupWithOne to AddCommGroupWithOne ℝ ▶
[resume] [0.000005s] propagating CommRing ℝ to subgoal CommRing ℝ of AddCommGroupWithOne ℝ ▶
[] [0.000074s] ✅ apply @AddCommGroup.toAddGroup to AddGroup ℝ ▶
[] [0.000045s] ✅ apply Real.instAddCommGroupReal to AddCommGroup ℝ ▶
[resume] [0.000005s] propagating AddCommGroup ℝ to subgoal AddCommGroup ℝ of AddGroup ℝ ▶
[] [0.000050s] ✅ apply @NormedAddCommGroup.toAddCommGroup to AddCommGroup ℝ ▶
[resume] [0.000005s] propagating NormedAddCommGroup ℝ to subgoal NormedAddCommGroup ℝ of AddCommGroup ℝ ▶
[] [0.000048s] ✅ apply @SeminormedAddCommGroup.toAddCommGroup to AddCommGroup ℝ ▶
[resume] [0.000005s] propagating SeminormedAddCommGroup ℝ to subgoal SeminormedAddCommGroup ℝ of AddCommGroup ℝ ▶
[] [0.000071s] ✅ apply @LieRing.toAddCommGroup to AddCommGroup ℝ ▶
[] [0.000061s] ✅ apply @LieRing.ofAssociativeRing to LieRing ℝ ▶
[resume] [0.000007s] propagating Ring ℝ to subgoal Ring ℝ of LieRing ℝ ▶
[resume] [0.000005s] propagating LieRing ℝ to subgoal LieRing ℝ of AddCommGroup ℝ ▶
[] [0.000070s] ✅ apply @OrderedAddCommGroup.toAddCommGroup to AddCommGroup ℝ ▶
[] [0.000044s] ✅ apply Real.orderedAddCommGroup to OrderedAddCommGroup ℝ ▶
[resume] [0.000006s] propagating OrderedAddCommGroup ℝ to subgoal OrderedAddCommGroup ℝ of AddCommGroup ℝ ▶
[] [0.000053s] ✅ apply @NormedOrderedAddGroup.toOrderedAddCommGroup to OrderedAddCommGroup ℝ ▶
[] [0.000049s] ✅ apply @StrictOrderedRing.toOrderedAddCommGroup to OrderedAddCommGroup ℝ ▶
[resume] [0.000005s] propagating StrictOrderedRing ℝ to subgoal StrictOrderedRing ℝ of OrderedAddCommGroup ℝ ▶
[] [0.000049s] ✅ apply @OrderedRing.toOrderedAddCommGroup to OrderedAddCommGroup ℝ ▶
[resume] [0.000206s] propagating OrderedRing ℝ to subgoal OrderedRing ℝ of OrderedAddCommGroup ℝ ▶
[] [0.000072s] ✅ apply @LinearOrderedAddCommGroup.toOrderedAddCommGroup to OrderedAddCommGroup ℝ ▶
[] [0.000049s] ✅ apply Real.instLinearOrderedAddCommGroupReal to LinearOrderedAddCommGroup ℝ ▶
[resume] [0.000006s] propagating LinearOrderedAddCommGroup ℝ to subgoal LinearOrderedAddCommGroup ℝ of OrderedAddCommGroup ℝ ▶
[] [0.000062s] ✅ apply @NormedLinearOrderedAddGroup.toLinearOrderedAddCommGroup to LinearOrderedAddCommGroup ℝ ▶
[] [0.000048s] ✅ apply @LinearOrderedRing.toLinearOrderedAddCommGroup to LinearOrderedAddCommGroup ℝ ▶
[resume] [0.000006s] propagating LinearOrderedRing ℝ to subgoal LinearOrderedRing ℝ of LinearOrderedAddCommGroup ℝ ▶
[] [0.000087s] ✅ apply @StarOrderedRing.toOrderedAddCommGroup to OrderedAddCommGroup ℝ ▶
[] [0.000062s] ✅ apply @NonUnitalNormedRing.toNonUnitalRing to NonUnitalRing ℝ ▶
[resume] [0.000006s] propagating NonUnitalNormedRing ℝ to subgoal NonUnitalNormedRing ℝ of NonUnitalRing ℝ ▶
[resume] [0.000034s] propagating NonUnitalRing ℝ to subgoal NonUnitalRing ℝ of OrderedAddCommGroup ℝ ▶
[] [0.000056s] ✅ apply Real.partialOrder to PartialOrder ℝ ▶
[] 1986 more entries... ▼
[resume] [0.000029s] propagating PartialOrder ℝ to subgoal PartialOrder ℝ of OrderedAddCommGroup ℝ ▶
[] [0.001104s] ✅ apply Real.instStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing to StarRing
ℝ ▶
[resume] [0.000037s] propagating StarRing ℝ to subgoal StarRing ℝ of OrderedAddCommGroup ℝ ▶
[] [0.000494s] ✅ apply Real.instStarOrderedRingRealToNonUnitalSemiringToNonUnitalCommSemiringToNonUnitalCommRingCommRingPartialOrderInstStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing to StarOrderedRing
ℝ ▶
[resume] [0.000011s] propagating StarOrderedRing ℝ to subgoal StarOrderedRing ℝ of OrderedAddCommGroup ℝ ▶
[] [0.001015s] ✅ apply @RCLike.toStarRing to StarRing ℝ ▶
[resume] [0.000032s] propagating StarRing ℝ to subgoal StarRing ℝ of OrderedAddCommGroup ℝ ▶
[] [0.000332s] ✅ apply Real.instStarOrderedRingRealToNonUnitalSemiringToNonUnitalCommSemiringToNonUnitalCommRingCommRingPartialOrderInstStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing to StarOrderedRing
ℝ ▶
[resume] [0.000010s] propagating StarOrderedRing ℝ to subgoal StarOrderedRing ℝ of OrderedAddCommGroup ℝ ▶
[] [0.000083s] ✅ apply @CompletePartialOrder.toPartialOrder to PartialOrder ℝ ▶
[] [0.000094s] ✅ apply @CompleteLattice.toCompletePartialOrder to CompletePartialOrder ℝ ▶
[] [0.000076s] ✅ apply @CompletelyDistribLattice.toCompleteLattice to CompleteLattice ℝ ▶
[] [0.000143s] ✅ apply @CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice to CompletelyDistribLattice ℝ ▶
[] [0.000073s] ✅ apply @CompleteLinearOrder.toCompletelyDistribLattice to CompletelyDistribLattice ℝ ▶
[] [0.000138s] ✅ apply @Order.Coframe.toCompleteLattice to CompleteLattice ℝ ▶
[] [0.000082s] ✅ apply @CompleteDistribLattice.toCoframe to Order.Coframe ℝ ▶
[] [0.000085s] ✅ apply @CompleteBooleanAlgebra.toCompleteDistribLattice to CompleteDistribLattice ℝ ▶
[] [0.000071s] ✅ apply @CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra to CompleteBooleanAlgebra ℝ ▶
[] [0.000048s] ✅ apply @CompletelyDistribLattice.toCompleteDistribLattice to CompleteDistribLattice ℝ ▶
[] [0.000057s] ✅ apply @Order.Frame.toCompleteLattice to CompleteLattice ℝ ▶
[] [0.000058s] ✅ apply @CompleteDistribLattice.toFrame to Order.Frame ℝ ▶
[] [0.000056s] ✅ apply @CompleteLinearOrder.toCompleteLattice to CompleteLattice ℝ ▶
[] [0.000062s] ✅ apply @OmegaCompletePartialOrder.toPartialOrder to PartialOrder ℝ ▶
[] [0.000065s] ✅ apply @CompletePartialOrder.toOmegaCompletePartialOrder to OmegaCompletePartialOrder ℝ ▶
[] [0.000048s] ✅ apply CompleteLattice.instOmegaCompletePartialOrder to OmegaCompletePartialOrder ℝ ▶
[] [0.000060s] ✅ apply @CompleteSemilatticeInf.toPartialOrder to PartialOrder ℝ ▶
[] [0.000056s] ✅ apply @CompleteLattice.toCompleteSemilatticeInf to CompleteSemilatticeInf ℝ ▶
[] [0.000058s] ✅ apply @CompleteSemilatticeSup.toPartialOrder to PartialOrder ℝ ▶
[] [0.000058s] ✅ apply @CompleteLattice.toCompleteSemilatticeSup to CompleteSemilatticeSup ℝ ▶
[] [0.000047s] ✅ apply @StrictOrderedRing.toPartialOrder to PartialOrder ℝ ▶
[resume] [0.000008s] propagating StrictOrderedRing ℝ to subgoal StrictOrderedRing ℝ of PartialOrder ℝ ▶
[] [0.000062s] ✅ apply @StrictOrderedSemiring.toPartialOrder to PartialOrder ℝ ▶
[] [0.000043s] ✅ apply Real.strictOrderedSemiring to StrictOrderedSemiring ℝ ▶
[resume] [0.000005s] propagating StrictOrderedSemiring ℝ to subgoal StrictOrderedSemiring ℝ of PartialOrder ℝ ▶
[] [0.000066s] ✅ apply @LinearOrderedSemiring.toStrictOrderedSemiring to StrictOrderedSemiring ℝ ▶
[] [0.000044s] ✅ apply Real.instLinearOrderedSemiringReal to LinearOrderedSemiring ℝ ▶
[resume] [0.000006s] propagating LinearOrderedSemiring ℝ to subgoal LinearOrderedSemiring ℝ of StrictOrderedSemiring ℝ ▶
[] [0.000063s] ✅ apply @LinearOrderedCommSemiring.toLinearOrderedSemiring to LinearOrderedSemiring ℝ ▶
[] [0.000067s] ✅ apply @LinearOrderedSemifield.toLinearOrderedCommSemiring to LinearOrderedCommSemiring ℝ ▶
[resume] [0.000006s] propagating LinearOrderedSemifield ℝ to subgoal LinearOrderedSemifield ℝ of LinearOrderedCommSemiring ℝ ▶
[resume] [0.000005s] propagating LinearOrderedCommSemiring ℝ to subgoal LinearOrderedCommSemiring ℝ of LinearOrderedSemiring ℝ ▶
[] [0.000047s] ✅ apply @LinearOrderedCommRing.toLinearOrderedCommSemiring to LinearOrderedCommSemiring ℝ ▶
[resume] [0.000005s] propagating LinearOrderedCommRing ℝ to subgoal LinearOrderedCommRing ℝ of LinearOrderedCommSemiring ℝ ▶
[] [0.000047s] ✅ apply @LinearOrderedRing.toLinearOrderedSemiring to LinearOrderedSemiring ℝ ▶
[resume] [0.000005s] propagating LinearOrderedRing ℝ to subgoal LinearOrderedRing ℝ of LinearOrderedSemiring ℝ ▶
[] [0.000062s] ✅ apply @StrictOrderedCommSemiring.toStrictOrderedSemiring to StrictOrderedSemiring ℝ ▶
[] [0.000043s] ✅ apply Real.strictOrderedCommSemiring to StrictOrderedCommSemiring ℝ ▶
[resume] [0.000005s] propagating StrictOrderedCommSemiring ℝ to subgoal StrictOrderedCommSemiring ℝ of StrictOrderedSemiring ℝ ▶
[] [0.000046s] ✅ apply @LinearOrderedCommSemiring.toStrictOrderedCommSemiring to StrictOrderedCommSemiring ℝ ▶
[resume] [0.000005s] propagating LinearOrderedCommSemiring
ℝ to subgoal LinearOrderedCommSemiring ℝ of StrictOrderedCommSemiring ℝ ▶
[] 1936 more entries... ▼
[] [0.000045s] ✅ apply @StrictOrderedCommRing.toStrictOrderedCommSemiring to StrictOrderedCommSemiring ℝ ▶
[resume] [0.000005s] propagating StrictOrderedCommRing ℝ to subgoal StrictOrderedCommRing ℝ of StrictOrderedCommSemiring ℝ ▶
[] [0.000052s] ✅ apply @StrictOrderedRing.toStrictOrderedSemiring to StrictOrderedSemiring ℝ ▶
[resume] [0.000006s] propagating StrictOrderedRing ℝ to subgoal StrictOrderedRing ℝ of StrictOrderedSemiring ℝ ▶
[] [0.000048s] ✅ apply @OrderedRing.toPartialOrder to PartialOrder ℝ ▶
[resume] [0.000006s] propagating OrderedRing ℝ to subgoal OrderedRing ℝ of PartialOrder ℝ ▶
[] [0.000064s] ✅ apply @OrderedSemiring.toPartialOrder to PartialOrder ℝ ▶
[] [0.000045s] ✅ apply Real.orderedSemiring to OrderedSemiring ℝ ▶
[resume] [0.000005s] propagating OrderedSemiring ℝ to subgoal OrderedSemiring ℝ of PartialOrder ℝ ▶
[] [0.000072s] ✅ apply @OrderedCommSemiring.toOrderedSemiring to OrderedSemiring ℝ ▶
[] [0.000070s] ✅ apply @CanonicallyOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring ℝ ▶
[] [0.000069s] ✅ apply @CanonicallyLinearOrderedSemifield.toCanonicallyOrderedCommSemiring to CanonicallyOrderedCommSemiring
ℝ ▶
[] [0.000050s] ✅ apply @StrictOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring ℝ ▶
[resume] [0.000006s] propagating StrictOrderedCommSemiring ℝ to subgoal StrictOrderedCommSemiring ℝ of OrderedCommSemiring ℝ ▶
[resume] [0.000004s] propagating OrderedCommSemiring ℝ to subgoal OrderedCommSemiring ℝ of OrderedSemiring ℝ ▶
[] [0.000046s] ✅ apply @OrderedCommRing.toOrderedCommSemiring to OrderedCommSemiring ℝ ▶
[resume] [0.000005s] propagating OrderedCommRing ℝ to subgoal OrderedCommRing ℝ of OrderedCommSemiring ℝ ▶
[] [0.000046s] ✅ apply @StrictOrderedSemiring.toOrderedSemiring to OrderedSemiring ℝ ▶
[resume] [0.000006s] propagating StrictOrderedSemiring ℝ to subgoal StrictOrderedSemiring ℝ of OrderedSemiring ℝ ▶
[] [0.000049s] ✅ apply @OrderedRing.toOrderedSemiring to OrderedSemiring ℝ ▶
[resume] [0.000005s] propagating OrderedRing ℝ to subgoal OrderedRing ℝ of OrderedSemiring ℝ ▶
[] [0.000065s] ✅ apply @OrderedCommGroup.toPartialOrder to PartialOrder ℝ ▶
[] [0.000071s] ✅ apply @NormedOrderedGroup.toOrderedCommGroup to OrderedCommGroup ℝ ▶
[] [0.000223s] ✅ apply @NormedLinearOrderedGroup.toNormedOrderedGroup to NormedOrderedGroup ℝ ▶
[] [0.000101s] ✅ apply @LinearOrderedCommGroup.toOrderedCommGroup to OrderedCommGroup ℝ ▶
[] [0.000328s] ✅ apply @NormedLinearOrderedGroup.toLinearOrderedCommGroup to LinearOrderedCommGroup ℝ ▶
[] [0.000089s] ✅ apply @OrderedAddCommGroup.toPartialOrder to PartialOrder ℝ ▶
[resume] [0.000009s] propagating OrderedAddCommGroup ℝ to subgoal OrderedAddCommGroup ℝ of PartialOrder ℝ ▶
[] [0.000081s] ✅ apply @OrderedCommMonoid.toPartialOrder to PartialOrder ℝ ▶
[] [0.000084s] ✅ apply @CanonicallyOrderedCommMonoid.toOrderedCommMonoid to OrderedCommMonoid ℝ ▶
[] [0.000074s] ✅ apply @CanonicallyLinearOrderedCommMonoid.toCanonicallyOrderedCommMonoid to CanonicallyOrderedCommMonoid ℝ ▶
[] [0.000068s] ✅ apply @LinearOrderedCommMonoid.toOrderedCommMonoid to OrderedCommMonoid ℝ ▶
[] [0.000073s] ✅ apply @LinearOrderedCommMonoidWithZero.toLinearOrderedCommMonoid to LinearOrderedCommMonoid ℝ ▶
[] [0.000074s] ✅ apply @LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero to LinearOrderedCommMonoidWithZero
ℝ ▶
[] [0.000087s] ✅ apply @CanonicallyLinearOrderedSemifield.toLinearOrderedCommGroupWithZero to LinearOrderedCommGroupWithZero
ℝ ▶
[] [0.000056s] ✅ apply @CanonicallyLinearOrderedCommMonoid.toLinearOrderedCommMonoid to LinearOrderedCommMonoid ℝ ▶
[] [0.000060s] ✅ apply @LinearOrderedCancelCommMonoid.toLinearOrderedCommMonoid to LinearOrderedCommMonoid ℝ ▶
[] [0.000058s] ✅ apply @LinearOrderedCommGroup.toLinearOrderedCancelCommMonoid to LinearOrderedCancelCommMonoid ℝ ▶
[] [0.000061s] ✅ apply @OrderedCancelCommMonoid.toOrderedCommMonoid to OrderedCommMonoid ℝ ▶
[] [0.000056s] ✅ apply @LinearOrderedCancelCommMonoid.toOrderedCancelCommMonoid to OrderedCancelCommMonoid ℝ ▶
[] [0.000056s] ✅ apply @OrderedCommGroup.toOrderedCancelCommMonoid to OrderedCancelCommMonoid ℝ ▶
[] [0.000048s] ✅ apply @CanonicallyOrderedCommSemiring.toOrderedCommMonoid to OrderedCommMonoid ℝ ▶
[] [0.000067s] ✅ apply @OrderedAddCommMonoid.toPartialOrder to PartialOrder ℝ ▶
[] [0.000046s] ✅ apply Real.orderedAddCommMonoid to OrderedAddCommMonoid ℝ ▶
[resume] [0.000006s] propagating OrderedAddCommMonoid ℝ to subgoal OrderedAddCommMonoid ℝ of PartialOrder ℝ ▶
[] [0.000049s] ✅ apply @OrderedSemiring.toOrderedAddCommMonoid to OrderedAddCommMonoid ℝ ▶
[resume] [0.000005s] propagating OrderedSemiring ℝ to subgoal OrderedSemiring ℝ of OrderedAddCommMonoid ℝ ▶
[] [0.000075s] ✅ apply @CanonicallyOrderedAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ℝ ▶
[] [0.000062s] ✅ apply @CanonicallyOrderedCommSemiring.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid
ℝ ▶
[] [0.000060s] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid
ℝ ▶
[] 1886 more entries... ▼
[] [0.000064s] ✅ apply @CanonicallyLinearOrderedSemifield.toCanonicallyLinearOrderedAddCommMonoid to CanonicallyLinearOrderedAddCommMonoid
ℝ ▶
[] [0.000050s] ✅ apply @IdemSemiring.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid ℝ ▶
[] [0.000063s] ✅ apply @LinearOrderedAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ℝ ▶
[] [0.000056s] ✅ apply @LinearOrderedSemiring.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ℝ ▶
[resume] [0.000007s] propagating LinearOrderedSemiring ℝ to subgoal LinearOrderedSemiring ℝ of LinearOrderedAddCommMonoid ℝ ▶
[resume] [0.000006s] propagating LinearOrderedAddCommMonoid ℝ to subgoal LinearOrderedAddCommMonoid ℝ of OrderedAddCommMonoid ℝ ▶
[] [0.000048s] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ℝ ▶
[] [0.000058s] ✅ apply @LinearOrderedAddCommMonoidWithTop.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ℝ ▶
[] [0.000063s] ✅ apply @LinearOrderedAddCommGroupWithTop.toLinearOrderedAddCommMonoidWithTop to LinearOrderedAddCommMonoidWithTop
ℝ ▶
[] [0.000057s] ✅ apply @LinearOrderedCancelAddCommMonoid.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ℝ ▶
[] [0.000058s] ✅ apply @LinearOrderedCommSemiring.toLinearOrderedCancelAddCommMonoid to LinearOrderedCancelAddCommMonoid ℝ ▶
[resume] [0.000005s] propagating LinearOrderedCommSemiring
ℝ to subgoal LinearOrderedCommSemiring ℝ of LinearOrderedCancelAddCommMonoid ℝ ▶
[resume] [0.000005s] propagating LinearOrderedCancelAddCommMonoid
ℝ to subgoal LinearOrderedCancelAddCommMonoid ℝ of LinearOrderedAddCommMonoid ℝ ▶
[] [0.000054s] ✅ apply @LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid to LinearOrderedCancelAddCommMonoid ℝ ▶
[resume] [0.000005s] propagating LinearOrderedAddCommGroup
ℝ to subgoal LinearOrderedAddCommGroup ℝ of LinearOrderedCancelAddCommMonoid ℝ ▶
[] [0.000068s] ✅ apply @OrderedCancelAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ℝ ▶
[] [0.000045s] ✅ apply Real.orderedCancelAddCommMonoid to OrderedCancelAddCommMonoid ℝ ▶
[resume] [0.000005s] propagating OrderedCancelAddCommMonoid ℝ to subgoal OrderedCancelAddCommMonoid ℝ of OrderedAddCommMonoid ℝ ▶
[] [0.000048s] ✅ apply @StrictOrderedSemiring.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid ℝ ▶
[resume] [0.000005s] propagating StrictOrderedSemiring ℝ to subgoal StrictOrderedSemiring ℝ of OrderedCancelAddCommMonoid ℝ ▶
[] [0.000046s] ✅ apply @LinearOrderedCancelAddCommMonoid.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid ℝ ▶
[resume] [0.000004s] propagating LinearOrderedCancelAddCommMonoid
ℝ to subgoal LinearOrderedCancelAddCommMonoid ℝ of OrderedCancelAddCommMonoid ℝ ▶
[] [0.000049s] ✅ apply @OrderedAddCommGroup.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid ℝ ▶
[resume] [0.000005s] propagating OrderedAddCommGroup ℝ to subgoal OrderedAddCommGroup ℝ of OrderedCancelAddCommMonoid ℝ ▶
[] [0.000077s] ✅ apply @StarOrderedRing.toOrderedAddCommMonoid to OrderedAddCommMonoid ℝ ▶
[] [0.000071s] ✅ apply @NonUnitalCommSemiring.toNonUnitalSemiring to NonUnitalSemiring ℝ ▶
[] [0.000068s] ✅ apply @NonUnitalCommRing.toNonUnitalCommSemiring to NonUnitalCommSemiring ℝ ▶
[] [0.000058s] ✅ apply @NonUnitalSeminormedCommRing.toNonUnitalCommRing to NonUnitalCommRing ℝ ▶
[resume] [0.000006s] propagating NonUnitalSeminormedCommRing ℝ to subgoal NonUnitalSeminormedCommRing ℝ of NonUnitalCommRing ℝ ▶
[resume] [0.000005s] propagating NonUnitalCommRing ℝ to subgoal NonUnitalCommRing ℝ of NonUnitalCommSemiring ℝ ▶
[resume] [0.000004s] propagating NonUnitalCommSemiring ℝ to subgoal NonUnitalCommSemiring ℝ of NonUnitalSemiring ℝ ▶
[resume] [0.000003s] propagating NonUnitalSemiring ℝ to subgoal NonUnitalSemiring ℝ of OrderedAddCommMonoid ℝ ▶
[resume] [0.000024s] propagating PartialOrder ℝ to subgoal PartialOrder ℝ of OrderedAddCommMonoid ℝ ▶
[] [0.000577s] ✅ apply Real.instStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing to StarRing
ℝ ▶
[resume] [0.000027s] propagating StarRing ℝ to subgoal StarRing ℝ of OrderedAddCommMonoid ℝ ▶
[] [0.000310s] ✅ apply Real.instStarOrderedRingRealToNonUnitalSemiringToNonUnitalCommSemiringToNonUnitalCommRingCommRingPartialOrderInstStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing to StarOrderedRing
ℝ ▶
[resume] [0.000009s] propagating StarOrderedRing ℝ to subgoal StarOrderedRing ℝ of OrderedAddCommMonoid ℝ ▶
[] [0.000346s] ✅ apply @RCLike.toStarRing to StarRing ℝ ▶
[resume] [0.000027s] propagating StarRing ℝ to subgoal StarRing ℝ of OrderedAddCommMonoid ℝ ▶
[] [0.000307s] ✅ apply Real.instStarOrderedRingRealToNonUnitalSemiringToNonUnitalCommSemiringToNonUnitalCommRingCommRingPartialOrderInstStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing to StarOrderedRing
ℝ ▶
[resume] [0.000009s] propagating StarOrderedRing ℝ to subgoal StarOrderedRing ℝ of OrderedAddCommMonoid ℝ ▶
[] [0.000060s] ✅ apply @CommRing.toNonUnitalCommRing to NonUnitalCommRing ℝ ▶
[resume] [0.000005s] propagating CommRing ℝ to subgoal CommRing ℝ of NonUnitalCommRing ℝ ▶
[] [0.000073s] ✅ apply @CommSemiring.toNonUnitalCommSemiring to NonUnitalCommSemiring ℝ ▶
[] [0.000056s] ✅ apply Real.instCommSemiringReal to CommSemiring ℝ ▶
[resume] [0.000006s] propagating CommSemiring ℝ to subgoal CommSemiring ℝ of NonUnitalCommSemiring ℝ ▶
[] [0.000074s] ❌ apply @DirectSum.GradeZero.commSemiring to CommSemiring ℝ ▶
[] [0.000070s] ✅ apply @IdemCommSemiring.toCommSemiring to CommSemiring ℝ ▶
[] [0.000051s] ✅ apply @Semifield.toCommSemiring to CommSemiring ℝ ▶
[resume] [0.000007s] propagating Semifield ℝ to subgoal Semifield ℝ of CommSemiring ℝ ▶
[] 1836 more entries... ▼
[] [0.000056s] ✅ apply @CanonicallyOrderedCommSemiring.toCommSemiring to CommSemiring ℝ ▶
[] [0.000059s] ✅ apply @StrictOrderedCommSemiring.toCommSemiring to CommSemiring ℝ ▶
[resume] [0.000006s] propagating StrictOrderedCommSemiring ℝ to subgoal StrictOrderedCommSemiring ℝ of CommSemiring ℝ ▶
[] [0.000049s] ✅ apply @OrderedCommSemiring.toCommSemiring to CommSemiring ℝ ▶
[resume] [0.000005s] propagating OrderedCommSemiring ℝ to subgoal OrderedCommSemiring ℝ of CommSemiring ℝ ▶
[] [0.000046s] ✅ apply @CommRing.toCommSemiring to CommSemiring ℝ ▶
[resume] [0.000005s] propagating CommRing ℝ to subgoal CommRing ℝ of CommSemiring ℝ ▶
[] [0.000050s] ✅ apply @Semiring.toNonUnitalSemiring to NonUnitalSemiring ℝ ▶
[resume] [0.000005s] propagating Semiring ℝ to subgoal Semiring ℝ of NonUnitalSemiring ℝ ▶
[] [0.000049s] ✅ apply @NonUnitalRing.toNonUnitalSemiring to NonUnitalSemiring ℝ ▶
[resume] [0.000005s] propagating NonUnitalRing ℝ to subgoal NonUnitalRing ℝ of NonUnitalSemiring ℝ ▶
[] [0.000078s] ✅ apply @SemilatticeInf.toPartialOrder to PartialOrder ℝ ▶
[] [0.000048s] ✅ apply Real.instSemilatticeInfReal to SemilatticeInf ℝ ▶
[resume] [0.000006s] propagating SemilatticeInf ℝ to subgoal SemilatticeInf ℝ of PartialOrder ℝ ▶
[] [0.000074s] ✅ apply @Lattice.toSemilatticeInf to SemilatticeInf ℝ ▶
[] [0.000043s] ✅ apply Real.lattice to Lattice ℝ ▶
[resume] [0.000005s] propagating Lattice ℝ to subgoal Lattice ℝ of SemilatticeInf ℝ ▶
[] [0.000052s] ✅ apply @NormedLatticeAddCommGroup.toLattice to Lattice ℝ ▶
[resume] [0.000005s] propagating NormedLatticeAddCommGroup ℝ to subgoal NormedLatticeAddCommGroup ℝ of Lattice ℝ ▶
[] [0.000073s] ✅ apply @ConditionallyCompleteLattice.toLattice to Lattice ℝ ▶
[] [0.000079s] ✅ apply @ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice to ConditionallyCompleteLattice ℝ ▶
[] [0.000043s] ✅ apply Real.instConditionallyCompleteLinearOrderReal to ConditionallyCompleteLinearOrder ℝ ▶
[resume] [0.000006s] propagating ConditionallyCompleteLinearOrder
ℝ to subgoal ConditionallyCompleteLinearOrder ℝ of ConditionallyCompleteLattice ℝ ▶
[resume] [0.000005s] propagating ConditionallyCompleteLattice ℝ to subgoal ConditionallyCompleteLattice ℝ of Lattice ℝ ▶
[] [0.000050s] ✅ apply @ConditionallyCompleteLinearOrderedField.toConditionallyCompleteLinearOrder to ConditionallyCompleteLinearOrder
ℝ ▶
[resume] [0.000005s] propagating ConditionallyCompleteLinearOrderedField
ℝ to subgoal ConditionallyCompleteLinearOrderedField
ℝ of ConditionallyCompleteLinearOrder ℝ ▶
[] [0.000060s] ✅ apply @ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder to ConditionallyCompleteLinearOrder
ℝ ▶
[] [0.000071s] ✅ apply @CompleteLinearOrder.toConditionallyCompleteLinearOrderBot to ConditionallyCompleteLinearOrderBot ℝ ▶
[] [0.000051s] ✅ apply @CompleteLattice.toConditionallyCompleteLattice to ConditionallyCompleteLattice ℝ ▶
[] [0.000051s] ✅ apply @CompleteLattice.toLattice to Lattice ℝ ▶
[] [0.000060s] ✅ apply @GeneralizedCoheytingAlgebra.toLattice to Lattice ℝ ▶
[] [0.000063s] ✅ apply @CoheytingAlgebra.toGeneralizedCoheytingAlgebra to GeneralizedCoheytingAlgebra ℝ ▶
[] [0.000067s] ✅ apply @BiheytingAlgebra.toCoheytingAlgebra to CoheytingAlgebra ℝ ▶
[] [0.000073s] ✅ apply @BooleanAlgebra.toBiheytingAlgebra to BiheytingAlgebra ℝ ▶
[] [0.000065s] ✅ apply @CompleteBooleanAlgebra.toBooleanAlgebra to BooleanAlgebra ℝ ▶
[] [0.000058s] ✅ apply @GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra to GeneralizedCoheytingAlgebra ℝ ▶
[] [0.000059s] ✅ apply @BooleanAlgebra.toGeneralizedBooleanAlgebra to GeneralizedBooleanAlgebra ℝ ▶
[] [0.000058s] ✅ apply @GeneralizedHeytingAlgebra.toLattice to Lattice ℝ ▶
[] [0.000067s] ✅ apply @HeytingAlgebra.toGeneralizedHeytingAlgebra to GeneralizedHeytingAlgebra ℝ ▶
[] [0.000058s] ✅ apply @BiheytingAlgebra.toHeytingAlgebra to HeytingAlgebra ℝ ▶
[] [0.000077s] ✅ apply @DistribLattice.toLattice to Lattice ℝ ▶
[] [0.000045s] ✅ apply Real.instDistribLatticeReal to DistribLattice ℝ ▶
[resume] [0.000006s] propagating DistribLattice ℝ to subgoal DistribLattice ℝ of Lattice ℝ ▶
[] [0.000052s] ✅ apply @BooleanAlgebra.toDistribLattice to DistribLattice ℝ ▶
[] [0.000048s] ✅ apply @GeneralizedBooleanAlgebra.toDistribLattice to DistribLattice ℝ ▶
[] [0.000047s] ✅ apply @Coframe.toDistribLattice to DistribLattice ℝ ▶
[] [0.000045s] ✅ apply @Frame.toDistribLattice to DistribLattice ℝ ▶
[] [0.000046s] ✅ apply @CoheytingAlgebra.toDistribLattice to DistribLattice ℝ ▶
[] [0.000055s] ✅ apply @GeneralizedCoheytingAlgebra.toDistribLattice to DistribLattice ℝ ▶
[] [0.000047s] ✅ apply @GeneralizedHeytingAlgebra.toDistribLattice to DistribLattice ℝ ▶
[] 1786 more entries... ▼
[] [0.000070s] ✅ apply @instDistribLattice to DistribLattice ℝ ▶
[] [0.000045s] ✅ apply Real.linearOrder to LinearOrder ℝ ▶
[resume] [0.000006s] propagating LinearOrder ℝ to subgoal LinearOrder ℝ of DistribLattice ℝ ▶
[] [0.000064s] ✅ apply @NonemptyFiniteLinearOrder.toLinearOrder to LinearOrder ℝ ▶
[] [0.000049s] ✅ apply instLinearOrder to LinearOrder ℝ ▶
[resume] [0.000005s] propagating ConditionallyCompleteLinearOrder
ℝ to subgoal ConditionallyCompleteLinearOrder ℝ of LinearOrder ℝ ▶
[] [0.000064s] ✅ apply @CompleteLinearOrder.toLinearOrder to LinearOrder ℝ ▶
[] [0.000046s] ✅ apply @LinearOrderedRing.toLinearOrder to LinearOrder ℝ ▶
[resume] [0.000005s] propagating LinearOrderedRing ℝ to subgoal LinearOrderedRing ℝ of LinearOrder ℝ ▶
[] [0.000049s] ✅ apply @LinearOrderedCommGroup.toLinearOrder to LinearOrder ℝ ▶
[] [0.000049s] ✅ apply @LinearOrderedAddCommGroup.toLinearOrder to LinearOrder ℝ ▶
[resume] [0.000005s] propagating LinearOrderedAddCommGroup ℝ to subgoal LinearOrderedAddCommGroup ℝ of LinearOrder ℝ ▶
[] [0.000092s] ✅ apply @LinearOrderedCommMonoid.toLinearOrder to LinearOrder ℝ ▶
[] [0.000049s] ✅ apply @LinearOrderedAddCommMonoid.toLinearOrder to LinearOrder ℝ ▶
[resume] [0.000005s] propagating LinearOrderedAddCommMonoid ℝ to subgoal LinearOrderedAddCommMonoid ℝ of LinearOrder ℝ ▶
[] [0.000056s] ✅ apply @LinearOrder.toLattice to Lattice ℝ ▶
[resume] [0.000006s] propagating LinearOrder ℝ to subgoal LinearOrder ℝ of Lattice ℝ ▶
[] [0.000069s] ✅ apply @SemilatticeSup.toPartialOrder to PartialOrder ℝ ▶
[] [0.000046s] ✅ apply Real.instSemilatticeSupReal to SemilatticeSup ℝ ▶
[resume] [0.000006s] propagating SemilatticeSup ℝ to subgoal SemilatticeSup ℝ of PartialOrder ℝ ▶
[] [0.000060s] ✅ apply @IdemCommSemiring.toSemilatticeSup to SemilatticeSup ℝ ▶
[] [0.000051s] ✅ apply @IdemSemiring.toSemilatticeSup to SemilatticeSup ℝ ▶
[] [0.000050s] ✅ apply @Lattice.toSemilatticeSup to SemilatticeSup ℝ ▶
[resume] [0.000012s] propagating Lattice ℝ to subgoal Lattice ℝ of SemilatticeSup ℝ ▶
[] [0.000048s] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.semilatticeSup to SemilatticeSup ℝ ▶
[] [0.000053s] ✅ apply @CanonicallyLinearOrderedCommMonoid.semilatticeSup to SemilatticeSup ℝ ▶
[] [0.000046s] ✅ apply @LinearOrder.toPartialOrder to PartialOrder ℝ ▶
[resume] [0.000006s] propagating LinearOrder ℝ to subgoal LinearOrder ℝ of PartialOrder ℝ ▶
[] [0.000072s] ✅ apply @SetLike.instPartialOrder to PartialOrder ℝ ▶
[] [0.000049s] ✅ apply @NonUnitalSeminormedRing.toNonUnitalRing to NonUnitalRing ℝ ▶
[resume] [0.000005s] propagating NonUnitalSeminormedRing ℝ to subgoal NonUnitalSeminormedRing ℝ of NonUnitalRing ℝ ▶
[] [0.000046s] ✅ apply @NonUnitalCommRing.toNonUnitalRing to NonUnitalRing ℝ ▶
[resume] [0.000005s] propagating NonUnitalCommRing ℝ to subgoal NonUnitalCommRing ℝ of NonUnitalRing ℝ ▶
[] [0.000074s] ✅ apply @Ring.toNonUnitalRing to NonUnitalRing ℝ ▶
[resume] [0.000005s] propagating Ring ℝ to subgoal Ring ℝ of NonUnitalRing ℝ ▶
[] [0.000055s] ✅ apply @NormedLatticeAddCommGroup.toOrderedAddCommGroup to OrderedAddCommGroup ℝ ▶
[resume] [0.000006s] propagating NormedLatticeAddCommGroup ℝ to subgoal NormedLatticeAddCommGroup ℝ of OrderedAddCommGroup ℝ ▶
[] [0.000054s] ✅ apply @Ring.toAddCommGroup to AddCommGroup ℝ ▶
[resume] [0.000005s] propagating Ring ℝ to subgoal Ring ℝ of AddCommGroup ℝ ▶
[] [0.000064s] ✅ apply @NonUnitalNonAssocRing.toAddCommGroup to AddCommGroup ℝ ▶
[] [0.000088s] ❌ apply @DirectSum.GradeZero.nonUnitalNonAssocRing to NonUnitalNonAssocRing ℝ ▶
[] [0.000086s] ✅ apply @NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing to NonUnitalNonAssocRing ℝ ▶
[] [0.000060s] ✅ apply @NonUnitalCommRing.toNonUnitalNonAssocCommRing to NonUnitalNonAssocCommRing ℝ ▶
[resume] [0.000007s] propagating NonUnitalCommRing ℝ to subgoal NonUnitalCommRing ℝ of NonUnitalNonAssocCommRing ℝ ▶
[resume] [0.000012s] propagating NonUnitalNonAssocCommRing ℝ to subgoal NonUnitalNonAssocCommRing ℝ of NonUnitalNonAssocRing ℝ ▶
[resume] [0.000007s] propagating NonUnitalNonAssocRing ℝ to subgoal NonUnitalNonAssocRing ℝ of AddCommGroup ℝ ▶
[] [0.000071s] ✅ apply @NonAssocRing.toNonUnitalNonAssocRing to NonUnitalNonAssocRing ℝ ▶
[resume] [0.000006s] propagating NonAssocRing ℝ to subgoal NonAssocRing ℝ of NonUnitalNonAssocRing ℝ ▶
[] [0.000502s] ✅ apply @NonUnitalRing.toNonUnitalNonAssocRing to NonUnitalNonAssocRing ℝ ▶
[resume] [0.000005s] propagating NonUnitalRing ℝ to subgoal NonUnitalRing ℝ of NonUnitalNonAssocRing ℝ ▶
[] 1736 more entries... ▼
[] [0.000050s] ✅ apply @AddCommGroupWithOne.toAddCommGroup to AddCommGroup ℝ ▶
[resume] [0.000006s] propagating AddCommGroupWithOne ℝ to subgoal AddCommGroupWithOne ℝ of AddCommGroup ℝ ▶
[] [0.000097s] ✅ apply @IsKleinFour.instFinite to Finite ℝ ▶
[] [0.001358s] ✅ apply @NormedGroup.toGroup to Group ℝ ▶
[] [0.000075s] ✅ apply @NormedCommGroup.toNormedGroup to NormedGroup ℝ ▶
[] [0.000061s] ✅ apply @NormedOrderedGroup.toNormedCommGroup to NormedCommGroup ℝ ▶
[] [0.000063s] ✅ apply @SeminormedGroup.toGroup to Group ℝ ▶
[] [0.000080s] ✅ apply @SeminormedCommGroup.toSeminormedGroup to SeminormedGroup ℝ ▶
[] [0.000061s] ✅ apply @NormedCommGroup.toSeminormedCommGroup to SeminormedCommGroup ℝ ▶
[] [0.000050s] ✅ apply @NormedGroup.toSeminormedGroup to SeminormedGroup ℝ ▶
[] [0.000064s] ✅ apply @CommGroup.toGroup to Group ℝ ▶
[] [0.000057s] ✅ apply @NormedCommGroup.toCommGroup to CommGroup ℝ ▶
[] [0.000047s] ✅ apply @SeminormedCommGroup.toCommGroup to CommGroup ℝ ▶
[] [0.000062s] ✅ apply @OrderedCommGroup.toCommGroup to CommGroup ℝ ▶
[] [0.000054s] ❌ apply Finite.prop to Finite ℝ ▶
[] [0.000074s] ✅ apply Finite.of_fintype to Finite ℝ ▶
[] [0.000074s] ✅ apply @NonemptyFiniteLinearOrder.toFintype to Fintype ℝ ▶
[] [0.000099s] ✅ apply @CategoryTheory.FinCategory.fintypeObj to Fintype ℝ ▶
[] [0.000091s] ✅ apply @CategoryTheory.Groupoid.toCategory to CategoryTheory.SmallCategory ℝ ▶
[] [0.000106s] ✅ apply CategoryTheory.StrictBicategory.category to CategoryTheory.SmallCategory ℝ ▶
[] [0.000093s] ✅ apply Preorder.smallCategory to CategoryTheory.SmallCategory ℝ ▶
[] [0.000056s] ✅ apply Real.instPreorderReal to Preorder ℝ ▶
[resume] [0.000008s] propagating Preorder ℝ to subgoal Preorder ℝ of CategoryTheory.SmallCategory ℝ ▶
[resume] [0.000022s] propagating CategoryTheory.SmallCategory ℝ to subgoal CategoryTheory.SmallCategory ℝ of Fintype ℝ ▶
[] [0.000063s] ✅ apply @PartialOrder.toPreorder to Preorder ℝ ▶
[resume] [0.000008s] propagating PartialOrder ℝ to subgoal PartialOrder ℝ of Preorder ℝ ▶
[] [0.000085s] ✅ apply @Unique.fintype to Fintype ℝ ▶
[] [0.000111s] ✅ apply @IsSimpleOrder.instFintype to Fintype ℝ ▶
[] [0.000143s] ✅ apply Real.decidableEq to DecidableEq ℝ ▶
[resume] [0.000023s] propagating (a b : ℝ) → Decidable (a = b) to subgoal DecidableEq ℝ of Fintype ℝ ▶
[] [0.000051s] ✅ apply Real.instLEReal to LE ℝ ▶
[resume] [0.000029s] propagating LE ℝ to subgoal LE ℝ of Fintype ℝ ▶
[] [0.000852s] ❌ apply NonemptyFiniteLinearOrder.toBoundedOrder to BoundedOrder ℝ ▶
[] [0.001540s] ❌ apply @CompleteLattice.toBoundedOrder to BoundedOrder ℝ ▶
[] [0.000571s] ❌ apply @BooleanAlgebra.toBoundedOrder to BoundedOrder ℝ ▶
[] [0.000695s] ❌ apply @CoheytingAlgebra.toBoundedOrder to BoundedOrder ℝ ▶
[] [0.000663s] ❌ apply @HeytingAlgebra.toBoundedOrder to BoundedOrder ℝ ▶
[] [0.000063s] ✅ apply @Preorder.toLE to LE ℝ ▶
[resume] [0.000009s] propagating Preorder ℝ to subgoal Preorder ℝ of LE ℝ ▶
[] [0.000197s] ✅ apply @instDecidableEq to DecidableEq ℝ ▶
[resume] [0.000013s] propagating ℝ → ℝ → LinearOrder ℝ to subgoal ℝ → ℝ → LinearOrder ℝ of DecidableEq ℝ ▶
[] [0.000173s] ✅ apply @FinEnum.decEq to DecidableEq ℝ ▶
[] [0.000188s] ✅ apply @RCLike.toDecidableEq to DecidableEq ℝ ▶
[resume] [0.000015s] propagating ℝ → ℝ → RCLike ℝ to subgoal ℝ → ℝ → RCLike ℝ of DecidableEq ℝ ▶
[] [0.000156s] ✅ apply @decidableEq_of_subsingleton to DecidableEq ℝ ▶
[] [0.000072s] ✅ apply @FinEnum.instFintype to Fintype ℝ ▶
[] [0.000104s] ✅ apply @SetLike.instFintype to Fintype ℝ ▶
[] [0.000081s] ✅ apply @SetLike.instFinite to Finite ℝ ▶
[] [0.000055s] ✅ apply @Finite.of_subsingleton to Finite ℝ ▶
[] [0.000058s] ✅ apply @NormedDivisionRing.toDivisionRing to DivisionRing ℝ ▶
[] 1686 more entries... ▼
[resume] [0.000009s] propagating NormedDivisionRing ℝ to subgoal NormedDivisionRing ℝ of DivisionRing ℝ ▶
[] [0.000055s] ✅ apply @Field.toDivisionRing to DivisionRing ℝ ▶
[resume] [0.000006s] propagating Field ℝ to subgoal Field ℝ of DivisionRing ℝ ▶
[] [0.000056s] ✅ apply @DivisionRing.toDivisionSemiring to DivisionSemiring ℝ ▶
[resume] [0.000007s] propagating DivisionRing ℝ to subgoal DivisionRing ℝ of DivisionSemiring ℝ ▶
[] [0.000062s] ✅ apply @StrictOrderedSemiring.toSemiring to Semiring ℝ ▶
[resume] [0.000007s] propagating StrictOrderedSemiring ℝ to subgoal StrictOrderedSemiring ℝ of Semiring ℝ ▶
[] [0.000053s] ✅ apply @OrderedSemiring.toSemiring to Semiring ℝ ▶
[resume] [0.000007s] propagating OrderedSemiring ℝ to subgoal OrderedSemiring ℝ of Semiring ℝ ▶
[] [0.000063s] ✅ apply @CommSemiring.toSemiring to Semiring ℝ ▶
[resume] [0.000017s] propagating CommSemiring ℝ to subgoal CommSemiring ℝ of Semiring ℝ ▶
[] [0.000095s] ✅ apply @Ring.toSemiring to Semiring ℝ ▶
[resume] [0.000007s] propagating Ring ℝ to subgoal Ring ℝ of Semiring ℝ ▶
[] [0.000056s] ✅ apply @instSemiring to Semiring ℝ ▶
[resume] [0.000006s] propagating Ring ℝ to subgoal Ring ℝ of Semiring ℝ ▶
[] [0.000058s] ✅ apply @NonAssocRing.toNonAssocSemiring to NonAssocSemiring ℝ ▶
[resume] [0.000007s] propagating NonAssocRing ℝ to subgoal NonAssocRing ℝ of NonAssocSemiring ℝ ▶
[] [0.000075s] ✅ apply @Unique.instSubsingleton to Subsingleton ℝ ▶
[] [0.000061s] ✅ apply @IsEmpty.instSubsingleton to Subsingleton ℝ ▶
[] [0.000051s] ❌ apply instSubsingleton to Subsingleton (Fin 2 → ℝ) ▶
[] [0.000065s] ✅ apply @CharP.CharOne.subsingleton to Subsingleton (Fin 2 → ℝ) ▶
[] [0.000110s] ✅ apply @Pi.nonAssocSemiring to NonAssocSemiring (Fin 2 → ℝ) ▶
[resume] [0.000009s] propagating Fin 2 → NonAssocSemiring ℝ to subgoal Fin 2 → NonAssocSemiring ℝ of NonAssocSemiring (Fin 2 → ℝ) ▶
[resume] [0.000046s] propagating NonAssocSemiring (Fin 2 → ℝ) to subgoal NonAssocSemiring (Fin 2 → ℝ) of Subsingleton (Fin 2 → ℝ) ▶
[] [0.005967s] ✅ apply CharP.pi' to CharP (Fin 2 → ℝ) 1 ▶
[] [0.000167s] ✅ apply @NonemptyFiniteLinearOrder.Nonempty to Nonempty (Fin 2) ▶
[] [0.000190s] ✅ apply Fin.nonemptyFiniteLinearOrder to NonemptyFiniteLinearOrder (Fin 2) ▶
[resume] [0.000007s] propagating NonemptyFiniteLinearOrder
(Fin (1 + 1)) to subgoal NonemptyFiniteLinearOrder (Fin 2) of Nonempty (Fin 2) ▶
[resume] [0.000031s] propagating Nonempty (Fin 2) to subgoal Nonempty (Fin 2) of CharP (Fin 2 → ℝ) 1 ▶
[] [0.000087s] ❌ apply @instForAllNonemptyNonempty to Nonempty (Fin 2) ▶
[] [0.000087s] ✅ apply @instNonempty to Nonempty (Fin 2) ▶
[] [0.000100s] ✅ apply Fin.inhabited to Inhabited (Fin 2) ▶
[] [0.000324s] ❌ apply USize.neZero to NeZero 2 ▶
[] [0.000462s] ✅ apply @NeZero.succ to NeZero 2 ▶
[resume] [0.000008s] propagating NeZero (1 + 1) to subgoal NeZero 2 of Inhabited (Fin 2) ▶
[resume] [0.000006s] propagating Inhabited (Fin 2) to subgoal Inhabited (Fin 2) of Nonempty (Fin 2) ▶
[] [0.003826s] ✅ apply @CharZero.NeZero.two to NeZero 2 ▶
[] [0.003763s] ❌ apply @NumberField.to_charZero to CharZero ℕ ▶
[] [0.003592s] ❌ apply @RCLike.charZero_rclike to CharZero ℕ ▶
[] [0.000935s] ✅ apply @StrictOrderedSemiring.to_charZero to CharZero ℕ ▶
[resume] [0.000025s] propagating CharZero ℕ to subgoal CharZero ℕ of NeZero 2 ▶
[resume] [0.000010s] propagating NeZero 2 to subgoal NeZero 2 of Inhabited (Fin 2) ▶
[] [0.000968s] ✅ apply ZeroLEOneClass.neZero.two to NeZero 2 ▶
[] [0.000109s] ✅ apply @CompletePartialOrder.toPartialOrder to PartialOrder ℕ ▶
[] [0.000174s] ✅ apply @CompleteLattice.toCompletePartialOrder to CompletePartialOrder ℕ ▶
[] [0.000076s] ✅ apply @CompletelyDistribLattice.toCompleteLattice to CompleteLattice ℕ ▶
[] [0.000065s] ✅ apply @CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice to CompletelyDistribLattice ℕ ▶
[] [0.000054s] ✅ apply @CompleteLinearOrder.toCompletelyDistribLattice to CompletelyDistribLattice ℕ ▶
[] [0.000058s] ✅ apply @Order.Coframe.toCompleteLattice to CompleteLattice ℕ ▶
[] [0.000061s] ✅ apply @CompleteDistribLattice.toCoframe to Order.Coframe ℕ ▶
[] 1636 more entries... ▼
[] [0.000057s] ✅ apply @CompleteBooleanAlgebra.toCompleteDistribLattice to CompleteDistribLattice ℕ ▶
[] [0.000057s] ✅ apply @CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra to CompleteBooleanAlgebra ℕ ▶
[] [0.000045s] ✅ apply @CompletelyDistribLattice.toCompleteDistribLattice to CompleteDistribLattice ℕ ▶
[] [0.000053s] ✅ apply @Order.Frame.toCompleteLattice to CompleteLattice ℕ ▶
[] [0.000047s] ✅ apply @CompleteDistribLattice.toFrame to Order.Frame ℕ ▶
[] [0.000052s] ✅ apply @CompleteLinearOrder.toCompleteLattice to CompleteLattice ℕ ▶
[] [0.000056s] ✅ apply @OmegaCompletePartialOrder.toPartialOrder to PartialOrder ℕ ▶
[] [0.000048s] ✅ apply @CompletePartialOrder.toOmegaCompletePartialOrder to OmegaCompletePartialOrder ℕ ▶
[] [0.000042s] ✅ apply CompleteLattice.instOmegaCompletePartialOrder to OmegaCompletePartialOrder ℕ ▶
[] [0.000054s] ✅ apply @CompleteSemilatticeInf.toPartialOrder to PartialOrder ℕ ▶
[] [0.000044s] ✅ apply @CompleteLattice.toCompleteSemilatticeInf to CompleteSemilatticeInf ℕ ▶
[] [0.000053s] ✅ apply @CompleteSemilatticeSup.toPartialOrder to PartialOrder ℕ ▶
[] [0.000048s] ✅ apply @CompleteLattice.toCompleteSemilatticeSup to CompleteSemilatticeSup ℕ ▶
[] [0.000052s] ✅ apply @StrictOrderedRing.toPartialOrder to PartialOrder ℕ ▶
[] [0.000051s] ✅ apply @LinearOrderedRing.toStrictOrderedRing to StrictOrderedRing ℕ ▶
[] [0.000054s] ✅ apply @LinearOrderedCommRing.toLinearOrderedRing to LinearOrderedRing ℕ ▶
[] [0.000056s] ✅ apply @LinearOrderedField.toLinearOrderedCommRing to LinearOrderedCommRing ℕ ▶
[] [0.000053s] ✅ apply @ConditionallyCompleteLinearOrderedField.toLinearOrderedField to LinearOrderedField ℕ ▶
[] [0.000050s] ✅ apply @NormedLinearOrderedField.toLinearOrderedField to LinearOrderedField ℕ ▶
[] [0.000051s] ✅ apply @StrictOrderedCommRing.toStrictOrderedRing to StrictOrderedRing ℕ ▶
[] [0.000048s] ✅ apply @LinearOrderedCommRing.toStrictOrderedCommRing to StrictOrderedCommRing ℕ ▶
[] [0.000055s] ✅ apply @StrictOrderedSemiring.toPartialOrder to PartialOrder ℕ ▶
[] [0.000038s] ✅ apply Nat.strictOrderedSemiring to StrictOrderedSemiring ℕ ▶
[resume] [0.000006s] propagating StrictOrderedSemiring ℕ to subgoal StrictOrderedSemiring ℕ of PartialOrder ℕ ▶
[resume] [0.000036s] propagating PartialOrder ℕ to subgoal PartialOrder ℕ of NeZero 2 ▶
[] [0.000690s] ✅ apply @OrderedSemiring.zeroLEOneClass to ZeroLEOneClass ℕ ▶
[resume] [0.000041s] propagating ZeroLEOneClass ℕ to subgoal ZeroLEOneClass ℕ of NeZero 2 ▶
[] [0.000502s] ❌ apply USize.neZero to NeZero 1 ▶
[] [0.000498s] ✅ apply @NeZero.succ to NeZero 1 ▶
[resume] [0.000061s] propagating NeZero (Nat.zero + 1) to subgoal NeZero 1 of NeZero 2 ▶
[] [0.008630s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass ℕ ℕ (fun x x_1 => x + x_1)
fun x x_1 => x ≤ x_1 ▶
[] [0.001129s] ✅ apply @OrderedAddCommMonoid.toCovariantClassLeft to CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤ x_1 ▶
[resume] [0.000013s] propagating CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤
x_1 to subgoal CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤ x_1 of NeZero 2 ▶
[] [0.000238s] ✅ apply @NeZero.charZero_one to NeZero 1 ▶
[resume] [0.000010s] propagating CharZero ℕ to subgoal CharZero ℕ of NeZero 1 ▶
[resume] [0.000013s] propagating NeZero 1 to subgoal NeZero 1 of NeZero 2 ▶
[resume] [0.000013s] propagating CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤
x_1 to subgoal CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤ x_1 of NeZero 2 ▶
[] [0.000785s] ✅ apply @NeZero.one to NeZero 1 ▶
[] [0.000056s] ✅ apply Nat.nontrivial to Nontrivial ℕ ▶
[resume] [0.000018s] propagating Nontrivial ℕ to subgoal Nontrivial ℕ of NeZero 1 ▶
[resume] [0.000015s] propagating NeZero 1 to subgoal NeZero 1 of NeZero 2 ▶
[resume] [0.000018s] propagating CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤
x_1 to subgoal CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤ x_1 of NeZero 2 ▶
[] [0.000102s] ✅ apply @LocalRing.toNontrivial to Nontrivial ℕ ▶
[] [0.000046s] ✅ apply Nat.semiring to Semiring ℕ ▶
[resume] [0.000028s] propagating Semiring ℕ to subgoal Semiring ℕ of Nontrivial ℕ ▶
[] [0.003467s] ❌ apply @HenselianLocalRing.toLocalRing to LocalRing ℕ ▶
[] [0.001953s] ❌ apply @DiscreteValuationRing.toLocalRing to LocalRing ℕ ▶
[] [0.001975s] ❌ apply ValuationRing.localRing to LocalRing ℕ ▶
[] [0.002248s] ❌ apply Field.instLocalRingToSemiringToDivisionSemiringToSemifield to LocalRing ℕ ▶
[] [0.000074s] ❌ apply @DirectSum.GradeZero.semiring to Semiring ℕ ▶
[] 1586 more entries... ▼
[] [0.000084s] ✅ apply @IdemSemiring.toSemiring to Semiring ℕ ▶
[] [0.000067s] ✅ apply @KleeneAlgebra.toIdemSemiring to IdemSemiring ℕ ▶
[] [0.000061s] ✅ apply @IdemCommSemiring.toIdemSemiring to IdemSemiring ℕ ▶
[] [0.000059s] ✅ apply @DivisionSemiring.toSemiring to Semiring ℕ ▶
[] [0.000058s] ✅ apply @Semifield.toDivisionSemiring to DivisionSemiring ℕ ▶
[] [0.000058s] ✅ apply @LinearOrderedSemifield.toSemifield to Semifield ℕ ▶
[] [0.000058s] ✅ apply @CanonicallyLinearOrderedSemifield.toLinearOrderedSemifield to LinearOrderedSemifield ℕ ▶
[] [0.000044s] ✅ apply @LinearOrderedField.toLinearOrderedSemifield to LinearOrderedSemifield ℕ ▶
[] [0.000063s] ✅ apply @Field.toSemifield to Semifield ℕ ▶
[] [0.000060s] ✅ apply @NormedField.toField to Field ℕ ▶
[] [0.000054s] ✅ apply @DenselyNormedField.toNormedField to NormedField ℕ ▶
[] [0.000072s] ✅ apply @RCLike.toDenselyNormedField to DenselyNormedField ℕ ▶
[] [0.000058s] ✅ apply @NontriviallyNormedField.toNormedField to NormedField ℕ ▶
[] [0.000055s] ✅ apply @DenselyNormedField.toNontriviallyNormedField to NontriviallyNormedField ℕ ▶
[] [0.000050s] ✅ apply NormedLinearOrderedField.toNormedField to NormedField ℕ ▶
[] [0.000050s] ✅ apply @LinearOrderedField.toField to Field ℕ ▶
[] [0.000056s] ✅ apply littleWedderburn to Field ℕ ▶
[] [0.000059s] ✅ apply @NormedDivisionRing.toDivisionRing to DivisionRing ℕ ▶
[] [0.000047s] ✅ apply @NormedField.toNormedDivisionRing to NormedDivisionRing ℕ ▶
[] [0.000045s] ✅ apply @Field.toDivisionRing to DivisionRing ℕ ▶
[] [0.000042s] ✅ apply @DivisionRing.toDivisionSemiring to DivisionSemiring ℕ ▶
[] [0.000043s] ✅ apply @StrictOrderedSemiring.toSemiring to Semiring ℕ ▶
[resume] [0.000008s] propagating StrictOrderedSemiring ℕ to subgoal StrictOrderedSemiring ℕ of Semiring ℕ ▶
[] [0.000066s] ✅ apply @OrderedSemiring.toSemiring to Semiring ℕ ▶
[] [0.000037s] ✅ apply Nat.orderedSemiring to OrderedSemiring ℕ ▶
[resume] [0.000006s] propagating OrderedSemiring ℕ to subgoal OrderedSemiring ℕ of Semiring ℕ ▶
[] [0.000060s] ✅ apply @OrderedCommSemiring.toOrderedSemiring to OrderedSemiring ℕ ▶
[] [0.000035s] ✅ apply Nat.orderedCommSemiring to OrderedCommSemiring ℕ ▶
[resume] [0.000005s] propagating OrderedCommSemiring ℕ to subgoal OrderedCommSemiring ℕ of OrderedSemiring ℕ ▶
[] [0.000056s] ✅ apply @CanonicallyOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring ℕ ▶
[] [0.000034s] ✅ apply Nat.canonicallyOrderedCommSemiring to CanonicallyOrderedCommSemiring ℕ ▶
[resume] [0.000005s] propagating CanonicallyOrderedCommSemiring
ℕ to subgoal CanonicallyOrderedCommSemiring ℕ of OrderedCommSemiring ℕ ▶
[] [0.000061s] ✅ apply @CanonicallyLinearOrderedSemifield.toCanonicallyOrderedCommSemiring to CanonicallyOrderedCommSemiring
ℕ ▶
[] [0.000059s] ✅ apply @StrictOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring ℕ ▶
[] [0.000034s] ✅ apply Nat.strictOrderedCommSemiring to StrictOrderedCommSemiring ℕ ▶
[resume] [0.000006s] propagating StrictOrderedCommSemiring ℕ to subgoal StrictOrderedCommSemiring ℕ of OrderedCommSemiring ℕ ▶
[] [0.000062s] ✅ apply @LinearOrderedCommSemiring.toStrictOrderedCommSemiring to StrictOrderedCommSemiring ℕ ▶
[] [0.000034s] ✅ apply Nat.linearOrderedCommSemiring to LinearOrderedCommSemiring ℕ ▶
[resume] [0.000005s] propagating LinearOrderedCommSemiring
ℕ to subgoal LinearOrderedCommSemiring ℕ of StrictOrderedCommSemiring ℕ ▶
[] [0.000044s] ✅ apply @LinearOrderedSemifield.toLinearOrderedCommSemiring to LinearOrderedCommSemiring ℕ ▶
[] [0.000042s] ✅ apply @LinearOrderedCommRing.toLinearOrderedCommSemiring to LinearOrderedCommSemiring ℕ ▶
[] [0.000049s] ✅ apply @StrictOrderedCommRing.toStrictOrderedCommSemiring to StrictOrderedCommSemiring ℕ ▶
[] [0.000056s] ✅ apply @OrderedCommRing.toOrderedCommSemiring to OrderedCommSemiring ℕ ▶
[] [0.000047s] ✅ apply @StrictOrderedCommRing.toOrderedCommRing to OrderedCommRing ℕ ▶
[] [0.000041s] ✅ apply @StrictOrderedSemiring.toOrderedSemiring to OrderedSemiring ℕ ▶
[resume] [0.000006s] propagating StrictOrderedSemiring ℕ to subgoal StrictOrderedSemiring ℕ of OrderedSemiring ℕ ▶
[] [0.000054s] ✅ apply @OrderedRing.toOrderedSemiring to OrderedSemiring ℕ ▶
[] [0.000048s] ✅ apply @OrderedCommRing.toOrderedRing to OrderedRing ℕ ▶
[] [0.000043s] ✅ apply @StrictOrderedRing.toOrderedRing to OrderedRing ℕ ▶
[] [0.000068s] ✅ apply @CommSemiring.toSemiring to Semiring ℕ ▶
[] 1536 more entries... ▼
[] [0.000035s] ✅ apply Nat.commSemiring to CommSemiring ℕ ▶
[resume] [0.000005s] propagating CommSemiring ℕ to subgoal CommSemiring ℕ of Semiring ℕ ▶
[] [0.000071s] ❌ apply @DirectSum.GradeZero.commSemiring to CommSemiring ℕ ▶
[] [0.000061s] ✅ apply @IdemCommSemiring.toCommSemiring to CommSemiring ℕ ▶
[] [0.000045s] ✅ apply @Semifield.toCommSemiring to CommSemiring ℕ ▶
[] [0.000042s] ✅ apply @CanonicallyOrderedCommSemiring.toCommSemiring to CommSemiring ℕ ▶
[resume] [0.000006s] propagating CanonicallyOrderedCommSemiring ℕ to subgoal CanonicallyOrderedCommSemiring ℕ of CommSemiring ℕ ▶
[] [0.000043s] ✅ apply @StrictOrderedCommSemiring.toCommSemiring to CommSemiring ℕ ▶
[resume] [0.000005s] propagating StrictOrderedCommSemiring ℕ to subgoal StrictOrderedCommSemiring ℕ of CommSemiring ℕ ▶
[] [0.000044s] ✅ apply @OrderedCommSemiring.toCommSemiring to CommSemiring ℕ ▶
[resume] [0.000005s] propagating OrderedCommSemiring ℕ to subgoal OrderedCommSemiring ℕ of CommSemiring ℕ ▶
[] [0.000064s] ✅ apply @CommRing.toCommSemiring to CommSemiring ℕ ▶
[] [0.000067s] ❌ apply @DirectSum.GradeZero.commRing to CommRing ℕ ▶
[] [0.000058s] ✅ apply @EuclideanDomain.toCommRing to CommRing ℕ ▶
[] [0.000045s] ✅ apply @Field.toEuclideanDomain to EuclideanDomain ℕ ▶
[] [0.000043s] ✅ apply @Field.toCommRing to CommRing ℕ ▶
[] [0.000050s] ✅ apply @StrictOrderedCommRing.toCommRing to CommRing ℕ ▶
[] [0.000042s] ✅ apply @OrderedCommRing.toCommRing to CommRing ℕ ▶
[] [0.000053s] ✅ apply @SeminormedCommRing.toCommRing to CommRing ℕ ▶
[] [0.000056s] ✅ apply @NormedCommRing.toSeminormedCommRing to SeminormedCommRing ℕ ▶
[] [0.000046s] ✅ apply @NormedField.toNormedCommRing to NormedCommRing ℕ ▶
[] [0.000053s] ✅ apply @BooleanRing.toCommRing to CommRing ℕ ▶
[] [0.000057s] ✅ apply @Ring.toSemiring to Semiring ℕ ▶
[] [0.000064s] ✅ apply @NormedRing.toRing to Ring ℕ ▶
[] [0.000048s] ✅ apply @NormedCommRing.toNormedRing to NormedRing ℕ ▶
[] [0.000044s] ✅ apply @NormedDivisionRing.toNormedRing to NormedRing ℕ ▶
[] [0.000420s] ✅ apply @SeminormedRing.toRing to Ring ℕ ▶
[] [0.000202s] ✅ apply @SeminormedCommRing.toSeminormedRing to SeminormedRing ℕ ▶
[] [0.000067s] ✅ apply @NormedRing.toSeminormedRing to SeminormedRing ℕ ▶
[] [0.000102s] ❌ apply @DirectSum.GradeZero.ring to Ring ℕ ▶
[] [0.000109s] ✅ apply @BooleanRing.toRing to Ring ℕ ▶
[] [0.000063s] ✅ apply @DivisionRing.toRing to Ring ℕ ▶
[] [0.000047s] ✅ apply @StrictOrderedRing.toRing to Ring ℕ ▶
[] [0.000056s] ✅ apply @OrderedRing.toRing to Ring ℕ ▶
[] [0.000046s] ✅ apply @CommRing.toRing to Ring ℕ ▶
[] [0.000048s] ✅ apply @instSemiring to Semiring ℕ ▶
[] [0.000072s] ✅ apply @IsSimpleAddGroup.toNontrivial to Nontrivial ℕ ▶
[] [0.000063s] ✅ apply @NormedAddGroup.toAddGroup to AddGroup ℕ ▶
[] [0.000067s] ✅ apply @NormedAddCommGroup.toNormedAddGroup to NormedAddGroup ℕ ▶
[] [0.000066s] ✅ apply @NormedLatticeAddCommGroup.toNormedAddCommGroup to NormedAddCommGroup ℕ ▶
[] [0.000061s] ✅ apply @NormedOrderedAddGroup.toNormedAddCommGroup to NormedAddCommGroup ℕ ▶
[] [0.000059s] ✅ apply @NormedLinearOrderedAddGroup.toNormedOrderedAddGroup to NormedOrderedAddGroup ℕ ▶
[] [0.000059s] ✅ apply @NonUnitalNormedRing.toNormedAddCommGroup to NormedAddCommGroup ℕ ▶
[] [0.000062s] ✅ apply @NonUnitalNormedCommRing.toNonUnitalNormedRing to NonUnitalNormedRing ℕ ▶
[] [0.000048s] ✅ apply @NormedCommRing.toNonUnitalNormedCommRing to NonUnitalNormedCommRing ℕ ▶
[] [0.000045s] ✅ apply @NormedRing.toNonUnitalNormedRing to NonUnitalNormedRing ℕ ▶
[] [0.000056s] ✅ apply @SeminormedAddGroup.toAddGroup to AddGroup ℕ ▶
[] [0.000060s] ✅ apply @SeminormedAddCommGroup.toSeminormedAddGroup to SeminormedAddGroup ℕ ▶
[] [0.000061s] ✅ apply @NonUnitalSeminormedRing.toSeminormedAddCommGroup to SeminormedAddCommGroup ℕ ▶
[] [0.000058s] ✅ apply @NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing to NonUnitalSeminormedRing ℕ ▶
[] 1486 more entries... ▼
[] [0.000049s] ✅ apply @SeminormedCommRing.toNonUnitalSeminormedCommRing to NonUnitalSeminormedCommRing ℕ ▶
[] [0.000044s] ✅ apply @NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing to NonUnitalSeminormedCommRing ℕ ▶
[] [0.000046s] ✅ apply @NonUnitalNormedRing.toNonUnitalSeminormedRing to NonUnitalSeminormedRing ℕ ▶
[] [0.000044s] ✅ apply @SeminormedRing.toNonUnitalSeminormedRing to NonUnitalSeminormedRing ℕ ▶
[] [0.000043s] ✅ apply @NormedAddCommGroup.toSeminormedAddCommGroup to SeminormedAddCommGroup ℕ ▶
[] [0.000042s] ✅ apply @NormedAddGroup.toSeminormedAddGroup to SeminormedAddGroup ℕ ▶
[] [0.000054s] ✅ apply @AddGroupWithOne.toAddGroup to AddGroup ℕ ▶
[] [0.000051s] ✅ apply @Ring.toAddGroupWithOne to AddGroupWithOne ℕ ▶
[] [0.000054s] ✅ apply @AddCommGroupWithOne.toAddGroupWithOne to AddGroupWithOne ℕ ▶
[] [0.000073s] ✅ apply @NonAssocRing.toAddCommGroupWithOne to AddCommGroupWithOne ℕ ▶
[] [0.000047s] ✅ apply @Ring.toNonAssocRing to NonAssocRing ℕ ▶
[] [0.000046s] ✅ apply @CommRing.toAddCommGroupWithOne to AddCommGroupWithOne ℕ ▶
[] [0.000066s] ✅ apply @AddCommGroup.toAddGroup to AddGroup ℕ ▶
[] [0.000046s] ✅ apply @NormedAddCommGroup.toAddCommGroup to AddCommGroup ℕ ▶
[] [0.000040s] ✅ apply @SeminormedAddCommGroup.toAddCommGroup to AddCommGroup ℕ ▶
[] [0.000054s] ✅ apply @LieRing.toAddCommGroup to AddCommGroup ℕ ▶
[] [0.000049s] ✅ apply @LieRing.ofAssociativeRing to LieRing ℕ ▶
[] [0.000058s] ✅ apply @OrderedAddCommGroup.toAddCommGroup to AddCommGroup ℕ ▶
[] [0.000047s] ✅ apply @NormedOrderedAddGroup.toOrderedAddCommGroup to OrderedAddCommGroup ℕ ▶
[] [0.000042s] ✅ apply @StrictOrderedRing.toOrderedAddCommGroup to OrderedAddCommGroup ℕ ▶
[] [0.000043s] ✅ apply @OrderedRing.toOrderedAddCommGroup to OrderedAddCommGroup ℕ ▶
[] [0.000053s] ✅ apply @LinearOrderedAddCommGroup.toOrderedAddCommGroup to OrderedAddCommGroup ℕ ▶
[] [0.000052s] ✅ apply @NormedLinearOrderedAddGroup.toLinearOrderedAddCommGroup to LinearOrderedAddCommGroup ℕ ▶
[] [0.000043s] ✅ apply @LinearOrderedRing.toLinearOrderedAddCommGroup to LinearOrderedAddCommGroup ℕ ▶
[] [0.000072s] ✅ apply @StarOrderedRing.toOrderedAddCommGroup to OrderedAddCommGroup ℕ ▶
[] [0.000049s] ✅ apply @NonUnitalNormedRing.toNonUnitalRing to NonUnitalRing ℕ ▶
[] [0.000046s] ✅ apply @NonUnitalSeminormedRing.toNonUnitalRing to NonUnitalRing ℕ ▶
[] [0.000066s] ✅ apply @NonUnitalCommRing.toNonUnitalRing to NonUnitalRing ℕ ▶
[] [0.000050s] ✅ apply @NonUnitalSeminormedCommRing.toNonUnitalCommRing to NonUnitalCommRing ℕ ▶
[] [0.000041s] ✅ apply @CommRing.toNonUnitalCommRing to NonUnitalCommRing ℕ ▶
[] [0.000044s] ✅ apply @Ring.toNonUnitalRing to NonUnitalRing ℕ ▶
[] [0.000054s] ✅ apply @NormedLatticeAddCommGroup.toOrderedAddCommGroup to OrderedAddCommGroup ℕ ▶
[] [0.000045s] ✅ apply @Ring.toAddCommGroup to AddCommGroup ℕ ▶
[] [0.000053s] ✅ apply @NonUnitalNonAssocRing.toAddCommGroup to AddCommGroup ℕ ▶
[] [0.000083s] ❌ apply @DirectSum.GradeZero.nonUnitalNonAssocRing to NonUnitalNonAssocRing ℕ ▶
[] [0.000064s] ✅ apply @NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing to NonUnitalNonAssocRing ℕ ▶
[] [0.000051s] ✅ apply @NonUnitalCommRing.toNonUnitalNonAssocCommRing to NonUnitalNonAssocCommRing ℕ ▶
[] [0.000045s] ✅ apply @NonAssocRing.toNonUnitalNonAssocRing to NonUnitalNonAssocRing ℕ ▶
[] [0.000043s] ✅ apply @NonUnitalRing.toNonUnitalNonAssocRing to NonUnitalNonAssocRing ℕ ▶
[] [0.000045s] ✅ apply @AddCommGroupWithOne.toAddCommGroup to AddCommGroup ℕ ▶
[] [0.000075s] ✅ apply @IsSimpleGroup.toNontrivial to Nontrivial ℕ ▶
[] [0.000067s] ✅ apply @NormedGroup.toGroup to Group ℕ ▶
[] [0.000057s] ✅ apply @NormedCommGroup.toNormedGroup to NormedGroup ℕ ▶
[] [0.000058s] ✅ apply @NormedOrderedGroup.toNormedCommGroup to NormedCommGroup ℕ ▶
[] [0.000059s] ✅ apply @NormedLinearOrderedGroup.toNormedOrderedGroup to NormedOrderedGroup ℕ ▶
[] [0.000058s] ✅ apply @SeminormedGroup.toGroup to Group ℕ ▶
[] [0.000056s] ✅ apply @SeminormedCommGroup.toSeminormedGroup to SeminormedGroup ℕ ▶
[] [0.000045s] ✅ apply @NormedCommGroup.toSeminormedCommGroup to SeminormedCommGroup ℕ ▶
[] [0.000052s] ✅ apply @NormedGroup.toSeminormedGroup to SeminormedGroup ℕ ▶
[] [0.000059s] ✅ apply @CommGroup.toGroup to Group ℕ ▶
[] 1436 more entries... ▼
[] [0.000047s] ✅ apply @NormedCommGroup.toCommGroup to CommGroup ℕ ▶
[] [0.000041s] ✅ apply @SeminormedCommGroup.toCommGroup to CommGroup ℕ ▶
[] [0.000053s] ✅ apply @OrderedCommGroup.toCommGroup to CommGroup ℕ ▶
[] [0.000050s] ✅ apply @NormedOrderedGroup.toOrderedCommGroup to OrderedCommGroup ℕ ▶
[] [0.000056s] ✅ apply @LinearOrderedCommGroup.toOrderedCommGroup to OrderedCommGroup ℕ ▶
[] [0.000064s] ✅ apply @NormedLinearOrderedGroup.toLinearOrderedCommGroup to LinearOrderedCommGroup ℕ ▶
[] [0.000069s] ✅ apply @IsSimpleOrder.toNontrivial to Nontrivial ℕ ▶
[] [0.000039s] ✅ apply instLENat to LE ℕ ▶
[resume] [0.000027s] propagating LE ℕ to subgoal LE ℕ of Nontrivial ℕ ▶
[] [0.000568s] ❌ apply NonemptyFiniteLinearOrder.toBoundedOrder to BoundedOrder ℕ ▶
[] [0.001058s] ❌ apply @CompleteLattice.toBoundedOrder to BoundedOrder ℕ ▶
[] [0.000551s] ❌ apply @BooleanAlgebra.toBoundedOrder to BoundedOrder ℕ ▶
[] [0.000682s] ❌ apply @CoheytingAlgebra.toBoundedOrder to BoundedOrder ℕ ▶
[] [0.000665s] ❌ apply @HeytingAlgebra.toBoundedOrder to BoundedOrder ℕ ▶
[] [0.000073s] ✅ apply @Preorder.toLE to LE ℕ ▶
[] [0.000052s] ✅ apply @PartialOrder.toPreorder to Preorder ℕ ▶
[resume] [0.000008s] propagating PartialOrder ℕ to subgoal PartialOrder ℕ of Preorder ℕ ▶
[resume] [0.000006s] propagating Preorder ℕ to subgoal Preorder ℕ of LE ℕ ▶
[] [0.000054s] ✅ apply @EuclideanDomain.toNontrivial to Nontrivial ℕ ▶
[] [0.000061s] ✅ apply @CanonicallyLinearOrderedSemifield.toNontrivial to Nontrivial ℕ ▶
[] [0.000049s] ✅ apply @Field.toNontrivial to Nontrivial ℕ ▶
[] [0.000048s] ✅ apply @Semifield.toNontrivial to Nontrivial ℕ ▶
[] [0.000044s] ✅ apply @DivisionRing.toNontrivial to Nontrivial ℕ ▶
[] [0.000046s] ✅ apply @DivisionSemiring.toNontrivial to Nontrivial ℕ ▶
[] [0.000065s] ✅ apply @instNontrivial to Nontrivial ℕ ▶
[] [0.000053s] ✅ apply @AddGroupWithOne.toAddMonoidWithOne to AddMonoidWithOne ℕ ▶
[] [0.000058s] ✅ apply @AddCommMonoidWithOne.toAddMonoidWithOne to AddMonoidWithOne ℕ ▶
[] [0.000048s] ✅ apply Nat.addCommMonoidWithOne to AddCommMonoidWithOne ℕ ▶
[resume] [0.000005s] propagating AddCommMonoidWithOne ℕ to subgoal AddCommMonoidWithOne ℕ of AddMonoidWithOne ℕ ▶
[resume] [0.000004s] propagating AddMonoidWithOne ℕ to subgoal AddMonoidWithOne ℕ of Nontrivial ℕ ▶
[resume] [0.000008s] propagating CharZero ℕ to subgoal CharZero ℕ of Nontrivial ℕ ▶
[] [0.000064s] ✅ apply @NonAssocSemiring.toAddCommMonoidWithOne to AddCommMonoidWithOne ℕ ▶
[] [0.000046s] ✅ apply @Semiring.toNonAssocSemiring to NonAssocSemiring ℕ ▶
[resume] [0.000005s] propagating Semiring ℕ to subgoal Semiring ℕ of NonAssocSemiring ℕ ▶
[resume] [0.000005s] propagating NonAssocSemiring ℕ to subgoal NonAssocSemiring ℕ of AddCommMonoidWithOne ℕ ▶
[] [0.000055s] ✅ apply @NonAssocRing.toNonAssocSemiring to NonAssocSemiring ℕ ▶
[] [0.000050s] ✅ apply @AddCommGroupWithOne.toAddCommMonoidWithOne to AddCommMonoidWithOne ℕ ▶
[] [0.000048s] ✅ apply @StrictOrderedRing.toNontrivial to Nontrivial ℕ ▶
[] [0.000048s] ✅ apply @StrictOrderedSemiring.toNontrivial to Nontrivial ℕ ▶
[resume] [0.000006s] propagating StrictOrderedSemiring ℕ to subgoal StrictOrderedSemiring ℕ of Nontrivial ℕ ▶
[] [0.000063s] ✅ apply @LinearOrderedCommGroupWithZero.toNontrivial to Nontrivial ℕ ▶
[] [0.000060s] ✅ apply @CanonicallyLinearOrderedSemifield.toLinearOrderedCommGroupWithZero to LinearOrderedCommGroupWithZero
ℕ ▶
[] [0.000062s] ✅ apply @LinearOrderedAddCommGroupWithTop.toNontrivial to Nontrivial ℕ ▶
[] [0.000051s] ✅ apply @IsDomain.toNontrivial to Nontrivial ℕ ▶
[resume] [0.000024s] propagating Semiring ℕ to subgoal Semiring ℕ of Nontrivial ℕ ▶
[] [0.001958s] ❌ apply @IsDedekindDomain.toIsDomain to IsDomain ℕ ▶
[] [0.002084s] ❌ apply @Field.isDomain to IsDomain ℕ ▶
[] [0.003143s] ❌ apply @DivisionRing.isDomain to IsDomain ℕ ▶
[] [0.000333s] ✅ apply @LinearOrderedRing.isDomain to IsDomain ℕ ▶
[] [0.004656s] ✅ apply @StarOrderedRing.toExistsAddOfLE to ExistsAddOfLE ℕ ▶
[] 1386 more entries... ▼
[] [0.000263s] ✅ apply Nat.instStarRing to StarRing ℕ ▶
[resume] [0.000030s] propagating StarRing ℕ to subgoal StarRing ℕ of ExistsAddOfLE ℕ ▶
[] [0.000069s] ✅ apply Nat.instStarOrderedRing to StarOrderedRing ℕ ▶
[resume] [0.000010s] propagating StarOrderedRing ℕ to subgoal StarOrderedRing ℕ of ExistsAddOfLE ℕ ▶
[resume] [0.000006s] propagating ExistsAddOfLE ℕ to subgoal ExistsAddOfLE ℕ of IsDomain ℕ ▶
[resume] [0.000007s] propagating IsDomain ℕ to subgoal IsDomain ℕ of Nontrivial ℕ ▶
[] [0.004294s] ❌ apply @RCLike.toStarRing to StarRing ℕ ▶
[] [0.000698s] ✅ apply CanonicallyOrderedAddCommMonoid.existsAddOfLE to ExistsAddOfLE ℕ ▶
[resume] [0.000008s] propagating ExistsAddOfLE ℕ to subgoal ExistsAddOfLE ℕ of IsDomain ℕ ▶
[] [0.007637s] ❌ apply AddGroup.existsAddOfLE to ExistsAddOfLE ℕ ▶
[] [0.003274s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain ℕ ▶
[] [0.000123s] ✅ apply @CommGroupWithZero.toNontrivial to Nontrivial ℕ ▶
[] [0.000083s] ✅ apply @Semifield.toCommGroupWithZero to CommGroupWithZero ℕ ▶
[] [0.000057s] ✅ apply @LinearOrderedCommGroupWithZero.toCommGroupWithZero to CommGroupWithZero ℕ ▶
[] [0.000070s] ✅ apply @GroupWithZero.toNontrivial to Nontrivial ℕ ▶
[] [0.000067s] ✅ apply @DivisionSemiring.toGroupWithZero to GroupWithZero ℕ ▶
[] [0.000050s] ✅ apply @CommGroupWithZero.toGroupWithZero to GroupWithZero ℕ ▶
[] [0.000057s] ✅ apply instNontrivial_1 to Nontrivial ℕ ▶
[] [0.000075s] ✅ apply Infinite.instNontrivial to Nontrivial ℕ ▶
[] [0.000056s] ✅ apply instInfiniteNat to Infinite ℕ ▶
[resume] [0.000023s] propagating Infinite ℕ to subgoal Infinite ℕ of Nontrivial ℕ ▶
[] [0.000066s] ✅ apply @IsAlgClosed.instInfinite to Infinite ℕ ▶
[] [0.000061s] ✅ apply CharZero.infinite to Infinite ℕ ▶
[resume] [0.000005s] propagating AddMonoidWithOne ℕ to subgoal AddMonoidWithOne ℕ of Infinite ℕ ▶
[resume] [0.000029s] propagating CharZero ℕ to subgoal CharZero ℕ of Infinite ℕ ▶
[] [0.000153s] ✅ apply @Denumerable.instInfinite to Infinite ℕ ▶
[] [0.000057s] ✅ apply Denumerable.nat to Denumerable ℕ ▶
[resume] [0.000007s] propagating Denumerable ℕ to subgoal Denumerable ℕ of Infinite ℕ ▶
[] [0.000072s] ✅ apply @instInfinite to Infinite ℕ ▶
[] [0.000053s] ✅ apply NontriviallyNormedField.infinite to Infinite ℕ ▶
[] [0.000218s] ✅ apply Nat.AtLeastTwo.toNeZero to NeZero 1 ▶
[] [0.000580s] ❌ apply @instNatAtLeastTwo to Nat.AtLeastTwo 1 ▶
[] [0.000218s] ✅ apply @Invertible.ne_zero to NeZero 1 ▶
[resume] [0.000037s] propagating Nontrivial ℕ to subgoal Nontrivial ℕ of NeZero 1 ▶
[] [0.000243s] ✅ apply @NeZero.of_gt' to NeZero 1 ▶
[] [0.000086s] ✅ apply @UnitalShelf.toOne to One ℕ ▶
[] [0.000056s] ❌ apply @GradedMonoid.GradeZero.one to One ℕ ▶
[] [0.000058s] ✅ apply @CanonicallyOrderedCommSemiring.toOne to One ℕ ▶
[resume] [0.000008s] propagating CanonicallyOrderedCommSemiring ℕ to subgoal CanonicallyOrderedCommSemiring ℕ of One ℕ ▶
[resume] [0.000046s] propagating One ℕ to subgoal One ℕ of NeZero 1 ▶
[] [0.000440s] ✅ apply Nat.Prime.one_lt' to Fact (1 < 1) ▶
[] [0.000073s] ✅ apply @Semiring.toOne to One ℕ ▶
[resume] [0.000008s] propagating Semiring ℕ to subgoal Semiring ℕ of One ℕ ▶
[] [0.000167s] ✅ apply @NonAssocRing.toOne to One ℕ ▶
[] [0.000073s] ✅ apply @NonAssocSemiring.toOne to One ℕ ▶
[resume] [0.000010s] propagating NonAssocSemiring ℕ to subgoal NonAssocSemiring ℕ of One ℕ ▶
[] [0.000060s] ✅ apply @AddCommGroupWithOne.toOne to One ℕ ▶
[] [0.000050s] ✅ apply @AddMonoidWithOne.toOne to One ℕ ▶
[resume] [0.000006s] propagating AddMonoidWithOne ℕ to subgoal AddMonoidWithOne ℕ of One ℕ ▶
[] [0.000068s] ✅ apply @InvOneClass.toOne to One ℕ ▶
[] 1336 more entries... ▼
[] [0.000081s] ✅ apply @DivInvOneMonoid.toInvOneClass to InvOneClass ℕ ▶
[] [0.000079s] ✅ apply @DivisionMonoid.toDivInvOneMonoid to DivInvOneMonoid ℕ ▶
[] [0.000072s] ✅ apply @DivisionCommMonoid.toDivisionMonoid to DivisionMonoid ℕ ▶
[] [0.000058s] ✅ apply @CommGroupWithZero.toDivisionCommMonoid to DivisionCommMonoid ℕ ▶
[] [0.000049s] ✅ apply @CommGroup.toDivisionCommMonoid to DivisionCommMonoid ℕ ▶
[] [0.000047s] ✅ apply @GroupWithZero.toDivisionMonoid to DivisionMonoid ℕ ▶
[] [0.000047s] ✅ apply @Group.toDivisionMonoid to DivisionMonoid ℕ ▶
[] [0.000058s] ✅ apply @RightCancelMonoid.toOne to One ℕ ▶
[] [0.000072s] ✅ apply @CancelMonoid.toRightCancelMonoid to RightCancelMonoid ℕ ▶
[] [0.000060s] ✅ apply @Group.toCancelMonoid to CancelMonoid ℕ ▶
[] [0.000063s] ✅ apply CancelCommMonoid.toCancelMonoid to CancelMonoid ℕ ▶
[] [0.000067s] ✅ apply @OrderedCancelCommMonoid.toCancelCommMonoid to CancelCommMonoid ℕ ▶
[] [0.000062s] ✅ apply @LinearOrderedCancelCommMonoid.toOrderedCancelCommMonoid to OrderedCancelCommMonoid ℕ ▶
[] [0.000053s] ✅ apply @LinearOrderedCommGroup.toLinearOrderedCancelCommMonoid to LinearOrderedCancelCommMonoid ℕ ▶
[] [0.000047s] ✅ apply @OrderedCommGroup.toOrderedCancelCommMonoid to OrderedCancelCommMonoid ℕ ▶
[] [0.000046s] ✅ apply @CommGroup.toCancelCommMonoid to CancelCommMonoid ℕ ▶
[] [0.000058s] ✅ apply @LeftCancelMonoid.toOne to One ℕ ▶
[] [0.000062s] ✅ apply @CancelCommMonoid.toLeftCancelMonoid to LeftCancelMonoid ℕ ▶
[] [0.000045s] ✅ apply @CancelMonoid.toLeftCancelMonoid to LeftCancelMonoid ℕ ▶
[] [0.000063s] ✅ apply @Monoid.toOne to One ℕ ▶
[] [0.000062s] ✅ apply Nat.monoid to Monoid ℕ ▶
[resume] [0.000007s] propagating Monoid ℕ to subgoal Monoid ℕ of One ℕ ▶
[] [0.000062s] ❌ apply @GradedMonoid.GradeZero.monoid to Monoid ℕ ▶
[] [0.000067s] ✅ apply @MonoidWithZero.toMonoid to Monoid ℕ ▶
[] [0.000057s] ✅ apply @Semiring.toMonoidWithZero to MonoidWithZero ℕ ▶
[resume] [0.000007s] propagating Semiring ℕ to subgoal Semiring ℕ of MonoidWithZero ℕ ▶
[resume] [0.000006s] propagating MonoidWithZero ℕ to subgoal MonoidWithZero ℕ of Monoid ℕ ▶
[] [0.000056s] ✅ apply @GroupWithZero.toMonoidWithZero to MonoidWithZero ℕ ▶
[] [0.000079s] ✅ apply @CommMonoidWithZero.toMonoidWithZero to MonoidWithZero ℕ ▶
[] [0.000072s] ✅ apply @LinearOrderedCommMonoidWithZero.toCommMonoidWithZero to CommMonoidWithZero ℕ ▶
[] [0.000042s] ✅ apply Nat.linearOrderedCommMonoidWithZero to LinearOrderedCommMonoidWithZero ℕ ▶
[resume] [0.000006s] propagating LinearOrderedCommMonoidWithZero
ℕ to subgoal LinearOrderedCommMonoidWithZero
ℕ of CommMonoidWithZero ℕ ▶
[resume] [0.000005s] propagating CommMonoidWithZero ℕ to subgoal CommMonoidWithZero ℕ of MonoidWithZero ℕ ▶
[] [0.000045s] ✅ apply @LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero to LinearOrderedCommMonoidWithZero
ℕ ▶
[] [0.000046s] ✅ apply @CommGroupWithZero.toCommMonoidWithZero to CommMonoidWithZero ℕ ▶
[] [0.000048s] ✅ apply @CommSemiring.toCommMonoidWithZero to CommMonoidWithZero ℕ ▶
[resume] [0.000006s] propagating CommSemiring ℕ to subgoal CommSemiring ℕ of CommMonoidWithZero ℕ ▶
[] [0.000077s] ✅ apply @CancelCommMonoidWithZero.toCommMonoidWithZero to CommMonoidWithZero ℕ ▶
[] [0.000049s] ✅ apply Nat.cancelCommMonoidWithZero to CancelCommMonoidWithZero ℕ ▶
[resume] [0.000006s] propagating CancelCommMonoidWithZero ℕ to subgoal CancelCommMonoidWithZero ℕ of CommMonoidWithZero ℕ ▶
[] [0.000056s] ✅ apply @IsDomain.toCancelCommMonoidWithZero to CancelCommMonoidWithZero ℕ ▶
[resume] [0.000029s] propagating CommSemiring ℕ to subgoal CommSemiring ℕ of CancelCommMonoidWithZero ℕ ▶
[] [0.001984s] ❌ apply @IsDedekindDomain.toIsDomain to IsDomain ℕ ▶
[] [0.002134s] ❌ apply @Field.isDomain to IsDomain ℕ ▶
[] [0.001902s] ❌ apply @DivisionRing.isDomain to IsDomain ℕ ▶
[] [0.000190s] ✅ apply @LinearOrderedRing.isDomain to IsDomain ℕ ▶
[resume] [0.000009s] propagating ExistsAddOfLE ℕ to subgoal ExistsAddOfLE ℕ of IsDomain ℕ ▶
[resume] [0.000008s] propagating IsDomain ℕ to subgoal IsDomain ℕ of CancelCommMonoidWithZero ℕ ▶
[resume] [0.000005s] propagating ExistsAddOfLE ℕ to subgoal ExistsAddOfLE ℕ of IsDomain ℕ ▶
[] [0.002038s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain ℕ ▶
[] 1286 more entries... ▼
[] [0.000088s] ✅ apply @CommGroupWithZero.toCancelCommMonoidWithZero to CancelCommMonoidWithZero ℕ ▶
[] [0.000081s] ✅ apply @CancelMonoidWithZero.toMonoidWithZero to MonoidWithZero ℕ ▶
[] [0.000074s] ✅ apply @IsDomain.toCancelMonoidWithZero to CancelMonoidWithZero ℕ ▶
[resume] [0.000005s] propagating Semiring ℕ to subgoal Semiring ℕ of CancelMonoidWithZero ℕ ▶
[resume] [0.000010s] propagating IsDomain ℕ to subgoal IsDomain ℕ of CancelMonoidWithZero ℕ ▶
[resume] [0.000006s] propagating CancelMonoidWithZero ℕ to subgoal CancelMonoidWithZero ℕ of MonoidWithZero ℕ ▶
[] [0.000070s] ✅ apply @CancelCommMonoidWithZero.toCancelMonoidWithZero to CancelMonoidWithZero ℕ ▶
[resume] [0.000006s] propagating CancelCommMonoidWithZero ℕ to subgoal CancelCommMonoidWithZero ℕ of CancelMonoidWithZero ℕ ▶
[] [0.000057s] ✅ apply @GroupWithZero.toCancelMonoidWithZero to CancelMonoidWithZero ℕ ▶
[] [0.000122s] ✅ apply @DivInvMonoid.toMonoid to Monoid ℕ ▶
[] [0.000070s] ✅ apply @DivisionRing.toDivInvMonoid to DivInvMonoid ℕ ▶
[] [0.000052s] ✅ apply @GroupWithZero.toDivInvMonoid to DivInvMonoid ℕ ▶
[] [0.000047s] ✅ apply @Group.toDivInvMonoid to DivInvMonoid ℕ ▶
[] [0.000059s] ✅ apply @DivisionMonoid.toDivInvMonoid to DivInvMonoid ℕ ▶
[] [0.000050s] ✅ apply @DivInvOneMonoid.toDivInvMonoid to DivInvMonoid ℕ ▶
[] [0.000075s] ✅ apply @CommMonoid.toMonoid to Monoid ℕ ▶
[] [0.000049s] ✅ apply Nat.commMonoid to CommMonoid ℕ ▶
[resume] [0.000007s] propagating CommMonoid ℕ to subgoal CommMonoid ℕ of Monoid ℕ ▶
[] [0.000065s] ❌ apply @GradedMonoid.GradeZero.commMonoid to CommMonoid ℕ ▶
[] [0.000057s] ✅ apply @LinearOrderedCommRing.toCommMonoid to CommMonoid ℕ ▶
[] [0.000081s] ✅ apply @OrderedCommMonoid.toCommMonoid to CommMonoid ℕ ▶
[] [0.000068s] ✅ apply @CanonicallyOrderedCommMonoid.toOrderedCommMonoid to OrderedCommMonoid ℕ ▶
[] [0.000065s] ✅ apply @CanonicallyLinearOrderedCommMonoid.toCanonicallyOrderedCommMonoid to CanonicallyOrderedCommMonoid ℕ ▶
[] [0.000067s] ✅ apply @LinearOrderedCommMonoid.toOrderedCommMonoid to OrderedCommMonoid ℕ ▶
[] [0.000040s] ✅ apply Nat.linearOrderedCommMonoid to LinearOrderedCommMonoid ℕ ▶
[resume] [0.000007s] propagating LinearOrderedCommMonoid ℕ to subgoal LinearOrderedCommMonoid ℕ of OrderedCommMonoid ℕ ▶
[resume] [0.000005s] propagating OrderedCommMonoid ℕ to subgoal OrderedCommMonoid ℕ of CommMonoid ℕ ▶
[] [0.000049s] ✅ apply @LinearOrderedCommMonoidWithZero.toLinearOrderedCommMonoid to LinearOrderedCommMonoid ℕ ▶
[resume] [0.000006s] propagating LinearOrderedCommMonoidWithZero
ℕ to subgoal LinearOrderedCommMonoidWithZero
ℕ of LinearOrderedCommMonoid ℕ ▶
[] [0.000061s] ✅ apply @CanonicallyLinearOrderedCommMonoid.toLinearOrderedCommMonoid to LinearOrderedCommMonoid ℕ ▶
[] [0.000049s] ✅ apply @LinearOrderedCancelCommMonoid.toLinearOrderedCommMonoid to LinearOrderedCommMonoid ℕ ▶
[] [0.000045s] ✅ apply @OrderedCancelCommMonoid.toOrderedCommMonoid to OrderedCommMonoid ℕ ▶
[] [0.000044s] ✅ apply @CanonicallyOrderedCommSemiring.toOrderedCommMonoid to OrderedCommMonoid ℕ ▶
[resume] [0.000007s] propagating CanonicallyOrderedCommSemiring
ℕ to subgoal CanonicallyOrderedCommSemiring
ℕ of OrderedCommMonoid ℕ ▶
[] [0.000049s] ✅ apply @CommRing.toCommMonoid to CommMonoid ℕ ▶
[] [0.000049s] ✅ apply @CommSemiring.toCommMonoid to CommMonoid ℕ ▶
[resume] [0.000006s] propagating CommSemiring ℕ to subgoal CommSemiring ℕ of CommMonoid ℕ ▶
[] [0.000049s] ✅ apply @CommMonoidWithZero.toCommMonoid to CommMonoid ℕ ▶
[resume] [0.000005s] propagating CommMonoidWithZero ℕ to subgoal CommMonoidWithZero ℕ of CommMonoid ℕ ▶
[] [0.000048s] ✅ apply @CommGroup.toCommMonoid to CommMonoid ℕ ▶
[] [0.000046s] ✅ apply @DivisionCommMonoid.toCommMonoid to CommMonoid ℕ ▶
[] [0.000049s] ✅ apply @CancelCommMonoid.toCommMonoid to CommMonoid ℕ ▶
[] [0.000052s] ✅ apply @RightCancelMonoid.toMonoid to Monoid ℕ ▶
[] [0.000050s] ✅ apply @LeftCancelMonoid.toMonoid to Monoid ℕ ▶
[] [0.000075s] ✅ apply @MulOneClass.toOne to One ℕ ▶
[] [0.000079s] ✅ apply @MulZeroOneClass.toMulOneClass to MulOneClass ℕ ▶
[] [0.000061s] ✅ apply @NonAssocSemiring.toMulZeroOneClass to MulZeroOneClass ℕ ▶
[resume] [0.000006s] propagating NonAssocSemiring ℕ to subgoal NonAssocSemiring ℕ of MulZeroOneClass ℕ ▶
[resume] [0.000005s] propagating MulZeroOneClass ℕ to subgoal MulZeroOneClass ℕ of MulOneClass ℕ ▶
[resume] [0.000005s] propagating MulOneClass ℕ to subgoal MulOneClass ℕ of One ℕ ▶
[] 1236 more entries... ▼
[] [0.000048s] ✅ apply @MonoidWithZero.toMulZeroOneClass to MulZeroOneClass ℕ ▶
[resume] [0.000005s] propagating MonoidWithZero ℕ to subgoal MonoidWithZero ℕ of MulZeroOneClass ℕ ▶
[] [0.000062s] ✅ apply @Monoid.toMulOneClass to MulOneClass ℕ ▶
[resume] [0.000007s] propagating Monoid ℕ to subgoal Monoid ℕ of MulOneClass ℕ ▶
[] [0.000071s] ✅ apply @One.ofOfNat1 to One ℕ ▶
[] [0.000055s] ✅ apply instOfNatNat to OfNat ℕ 1 ▶
[resume] [0.000006s] propagating OfNat ℕ 1 to subgoal OfNat ℕ 1 of One ℕ ▶
[] [0.000050s] ✅ apply @One.toOfNat1 to OfNat ℕ 1 ▶
[resume] [0.000005s] propagating One ℕ to subgoal One ℕ of OfNat ℕ 1 ▶
[] [0.000088s] ✅ apply @instOfNatAtLeastTwo to OfNat ℕ 1 ▶
[] [0.000047s] ✅ apply instNatCastNat to NatCast ℕ ▶
[resume] [0.000013s] propagating NatCast ℕ to subgoal NatCast ℕ of OfNat ℕ 1 ▶
[] [0.000076s] ❌ apply @instNatAtLeastTwo to Nat.AtLeastTwo 1 ▶
[] [0.000064s] ❌ apply @DirectSum.instNatCastOfNatToOfNat0ToZero to NatCast ℕ ▶
[] [0.000064s] ✅ apply @CanonicallyOrderedCommSemiring.toNatCast to NatCast ℕ ▶
[resume] [0.000008s] propagating CanonicallyOrderedCommSemiring ℕ to subgoal CanonicallyOrderedCommSemiring ℕ of NatCast ℕ ▶
[] [0.000050s] ✅ apply @Semiring.toNatCast to NatCast ℕ ▶
[resume] [0.000006s] propagating Semiring ℕ to subgoal Semiring ℕ of NatCast ℕ ▶
[] [0.000057s] ✅ apply @NonAssocRing.toNatCast to NatCast ℕ ▶
[] [0.000044s] ✅ apply @NonAssocSemiring.toNatCast to NatCast ℕ ▶
[resume] [0.000006s] propagating NonAssocSemiring ℕ to subgoal NonAssocSemiring ℕ of NatCast ℕ ▶
[] [0.000051s] ✅ apply @AddCommGroupWithOne.toNatCast to NatCast ℕ ▶
[] [0.000046s] ✅ apply @AddMonoidWithOne.toNatCast to NatCast ℕ ▶
[resume] [0.000006s] propagating AddMonoidWithOne ℕ to subgoal AddMonoidWithOne ℕ of NatCast ℕ ▶
[] [0.000309s] ✅ apply @canonicallyOrderedAddCommMonoid.toZeroLeOneClass to ZeroLEOneClass ℕ ▶
[resume] [0.000010s] propagating ZeroLEOneClass ℕ to subgoal ZeroLEOneClass ℕ of NeZero 2 ▶
[resume] [0.000016s] propagating NeZero 1 to subgoal NeZero 1 of NeZero 2 ▶
[resume] [0.000035s] propagating CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤
x_1 to subgoal CovariantClass ℕ ℕ (fun x x_1 => x + x_1)
fun x x_1 => x ≤ x_1 of NeZero 2 ▶
[resume] [0.000016s] propagating NeZero 1 to subgoal NeZero 1 of NeZero 2 ▶
[resume] [0.000018s] propagating CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤
x_1 to subgoal CovariantClass ℕ ℕ (fun x x_1 => x + x_1)
fun x x_1 => x ≤ x_1 of NeZero 2 ▶
[resume] [0.000022s] propagating NeZero (Nat.zero + 1) to subgoal NeZero 1 of NeZero 2 ▶
[resume] [0.000018s] propagating CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤
x_1 to subgoal CovariantClass ℕ ℕ (fun x x_1 => x + x_1)
fun x x_1 => x ≤ x_1 of NeZero 2 ▶
[] [0.000716s] ✅ apply @LinearOrderedCommMonoidWithZero.toZeroLeOneClass to ZeroLEOneClass ℕ ▶
[resume] [0.000010s] propagating ZeroLEOneClass ℕ to subgoal ZeroLEOneClass ℕ of NeZero 2 ▶
[resume] [0.000013s] propagating NeZero 1 to subgoal NeZero 1 of NeZero 2 ▶
[resume] [0.000014s] propagating CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤
x_1 to subgoal CovariantClass ℕ ℕ (fun x x_1 => x + x_1)
fun x x_1 => x ≤ x_1 of NeZero 2 ▶
[resume] [0.000011s] propagating NeZero 1 to subgoal NeZero 1 of NeZero 2 ▶
[resume] [0.000245s] propagating CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤
x_1 to subgoal CovariantClass ℕ ℕ (fun x x_1 => x + x_1)
fun x x_1 => x ≤ x_1 of NeZero 2 ▶
[resume] [0.000024s] propagating NeZero (Nat.zero + 1) to subgoal NeZero 1 of NeZero 2 ▶
[resume] [0.000023s] propagating CovariantClass ℕ ℕ (fun x x_1 => x + x_1) fun x x_1 =>
x ≤
x_1 to subgoal CovariantClass ℕ ℕ (fun x x_1 => x + x_1)
fun x x_1 => x ≤ x_1 of NeZero 2 ▶
[] [0.000164s] ✅ apply @LinearOrderedSemiring.toStrictOrderedSemiring to StrictOrderedSemiring ℕ ▶
[] [0.000092s] ✅ apply Nat.linearOrderedSemiring to LinearOrderedSemiring ℕ ▶
[resume] [0.000014s] propagating LinearOrderedSemiring ℕ to subgoal LinearOrderedSemiring ℕ of StrictOrderedSemiring ℕ ▶
[] [0.000117s] ✅ apply @LinearOrderedCommSemiring.toLinearOrderedSemiring to LinearOrderedSemiring ℕ ▶
[resume] [0.000013s] propagating LinearOrderedCommSemiring ℕ to subgoal LinearOrderedCommSemiring ℕ of LinearOrderedSemiring ℕ ▶
[] [0.000111s] ✅ apply @LinearOrderedRing.toLinearOrderedSemiring to LinearOrderedSemiring ℕ ▶
[] [0.000113s] ✅ apply @StrictOrderedCommSemiring.toStrictOrderedSemiring to StrictOrderedSemiring ℕ ▶
[resume] [0.000014s] propagating StrictOrderedCommSemiring ℕ to subgoal StrictOrderedCommSemiring ℕ of StrictOrderedSemiring ℕ ▶
[] [0.000112s] ✅ apply @StrictOrderedRing.toStrictOrderedSemiring to StrictOrderedSemiring ℕ ▶
[] [0.000113s] ✅ apply @OrderedRing.toPartialOrder to PartialOrder ℕ ▶
[] 1186 more entries... ▼
[] [0.000104s] ✅ apply @OrderedSemiring.toPartialOrder to PartialOrder ℕ ▶
[resume] [0.000013s] propagating OrderedSemiring ℕ to subgoal OrderedSemiring ℕ of PartialOrder ℕ ▶
[] [0.000107s] ✅ apply @OrderedCommGroup.toPartialOrder to PartialOrder ℕ ▶
[] [0.000107s] ✅ apply @OrderedAddCommGroup.toPartialOrder to PartialOrder ℕ ▶
[] [0.000104s] ✅ apply @OrderedCommMonoid.toPartialOrder to PartialOrder ℕ ▶
[resume] [0.000012s] propagating OrderedCommMonoid ℕ to subgoal OrderedCommMonoid ℕ of PartialOrder ℕ ▶
[] [0.000136s] ✅ apply @OrderedAddCommMonoid.toPartialOrder to PartialOrder ℕ ▶
[] [0.000110s] ✅ apply @OrderedSemiring.toOrderedAddCommMonoid to OrderedAddCommMonoid ℕ ▶
[resume] [0.000011s] propagating OrderedSemiring ℕ to subgoal OrderedSemiring ℕ of OrderedAddCommMonoid ℕ ▶
[resume] [0.000012s] propagating OrderedAddCommMonoid ℕ to subgoal OrderedAddCommMonoid ℕ of PartialOrder ℕ ▶
[] [0.000153s] ✅ apply @CanonicallyOrderedAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ℕ ▶
[] [0.000113s] ✅ apply @CanonicallyOrderedCommSemiring.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid
ℕ ▶
[resume] [0.000011s] propagating CanonicallyOrderedCommSemiring
ℕ to subgoal CanonicallyOrderedCommSemiring
ℕ of CanonicallyOrderedAddCommMonoid ℕ ▶
[resume] [0.000011s] propagating CanonicallyOrderedAddCommMonoid
ℕ to subgoal CanonicallyOrderedAddCommMonoid
ℕ of OrderedAddCommMonoid ℕ ▶
[] [0.000154s] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid
ℕ ▶
[] [0.000089s] ✅ apply Nat.canonicallyLinearOrderedAddCommMonoid to CanonicallyLinearOrderedAddCommMonoid ℕ ▶
[resume] [0.000013s] propagating CanonicallyLinearOrderedAddCommMonoid
ℕ to subgoal CanonicallyLinearOrderedAddCommMonoid
ℕ of CanonicallyOrderedAddCommMonoid ℕ ▶
[] [0.000275s] ✅ apply @CanonicallyLinearOrderedSemifield.toCanonicallyLinearOrderedAddCommMonoid to CanonicallyLinearOrderedAddCommMonoid
ℕ ▶
[] [0.000061s] ✅ apply @IdemSemiring.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid ℕ ▶
[] [0.000063s] ✅ apply @LinearOrderedAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ℕ ▶
[] [0.000053s] ✅ apply @LinearOrderedSemiring.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ℕ ▶
[resume] [0.000009s] propagating LinearOrderedSemiring ℕ to subgoal LinearOrderedSemiring ℕ of LinearOrderedAddCommMonoid ℕ ▶
[resume] [0.000005s] propagating LinearOrderedAddCommMonoid ℕ to subgoal LinearOrderedAddCommMonoid ℕ of OrderedAddCommMonoid ℕ ▶
[] [0.000046s] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ℕ ▶
[resume] [0.000005s] propagating CanonicallyLinearOrderedAddCommMonoid
ℕ to subgoal CanonicallyLinearOrderedAddCommMonoid
ℕ of LinearOrderedAddCommMonoid ℕ ▶
[] [0.000066s] ✅ apply @LinearOrderedAddCommMonoidWithTop.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ℕ ▶
[] [0.000062s] ✅ apply @LinearOrderedAddCommGroupWithTop.toLinearOrderedAddCommMonoidWithTop to LinearOrderedAddCommMonoidWithTop
ℕ ▶
[] [0.000059s] ✅ apply @LinearOrderedCancelAddCommMonoid.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid ℕ ▶
[] [0.000036s] ✅ apply Nat.linearOrderedCancelAddCommMonoid to LinearOrderedCancelAddCommMonoid ℕ ▶
[resume] [0.000005s] propagating LinearOrderedCancelAddCommMonoid
ℕ to subgoal LinearOrderedCancelAddCommMonoid
ℕ of LinearOrderedAddCommMonoid ℕ ▶
[] [0.000044s] ✅ apply @LinearOrderedCommSemiring.toLinearOrderedCancelAddCommMonoid to LinearOrderedCancelAddCommMonoid ℕ ▶
[resume] [0.000005s] propagating LinearOrderedCommSemiring
ℕ to subgoal LinearOrderedCommSemiring
ℕ of LinearOrderedCancelAddCommMonoid ℕ ▶
[] [0.000045s] ✅ apply @LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid to LinearOrderedCancelAddCommMonoid ℕ ▶
[] [0.000060s] ✅ apply @OrderedCancelAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid ℕ ▶
[] [0.000061s] ✅ apply @StrictOrderedSemiring.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid ℕ ▶
[resume] [0.000007s] propagating StrictOrderedSemiring ℕ to subgoal StrictOrderedSemiring ℕ of OrderedCancelAddCommMonoid ℕ ▶
[resume] [0.000005s] propagating OrderedCancelAddCommMonoid ℕ to subgoal OrderedCancelAddCommMonoid ℕ of OrderedAddCommMonoid ℕ ▶
[] [0.000044s] ✅ apply @LinearOrderedCancelAddCommMonoid.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid ℕ ▶
[resume] [0.000004s] propagating LinearOrderedCancelAddCommMonoid
ℕ to subgoal LinearOrderedCancelAddCommMonoid
ℕ of OrderedCancelAddCommMonoid ℕ ▶
[] [0.000045s] ✅ apply @OrderedAddCommGroup.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid ℕ ▶
[] [0.000071s] ✅ apply @StarOrderedRing.toOrderedAddCommMonoid to OrderedAddCommMonoid ℕ ▶
[] [0.000062s] ✅ apply @NonUnitalCommSemiring.toNonUnitalSemiring to NonUnitalSemiring ℕ ▶
[] [0.000055s] ✅ apply @NonUnitalCommRing.toNonUnitalCommSemiring to NonUnitalCommSemiring ℕ ▶
[] [0.000043s] ✅ apply @CommSemiring.toNonUnitalCommSemiring to NonUnitalCommSemiring ℕ ▶
[resume] [0.000005s] propagating CommSemiring ℕ to subgoal CommSemiring ℕ of NonUnitalCommSemiring ℕ ▶
[resume] [0.000004s] propagating NonUnitalCommSemiring ℕ to subgoal NonUnitalCommSemiring ℕ of NonUnitalSemiring ℕ ▶
[resume] [0.000003s] propagating NonUnitalSemiring ℕ to subgoal NonUnitalSemiring ℕ of OrderedAddCommMonoid ℕ ▶
[resume] [0.000005s] propagating PartialOrder ℕ to subgoal PartialOrder ℕ of OrderedAddCommMonoid ℕ ▶
[resume] [0.000008s] propagating StarRing ℕ to subgoal StarRing ℕ of OrderedAddCommMonoid ℕ ▶
[resume] [0.000008s] propagating StarOrderedRing ℕ to subgoal StarOrderedRing ℕ of OrderedAddCommMonoid ℕ ▶
[] 1136 more entries... ▼
[] [0.000053s] ✅ apply @Semiring.toNonUnitalSemiring to NonUnitalSemiring ℕ ▶
[resume] [0.000006s] propagating Semiring ℕ to subgoal Semiring ℕ of NonUnitalSemiring ℕ ▶
[] [0.000046s] ✅ apply @NonUnitalRing.toNonUnitalSemiring to NonUnitalSemiring ℕ ▶
[] [0.000069s] ✅ apply @SemilatticeInf.toPartialOrder to PartialOrder ℕ ▶
[] [0.000074s] ✅ apply @Lattice.toSemilatticeInf to SemilatticeInf ℕ ▶
[] [0.000040s] ✅ apply Nat.instLatticeNat to Lattice ℕ ▶
[resume] [0.000006s] propagating Lattice ℕ to subgoal Lattice ℕ of SemilatticeInf ℕ ▶
[resume] [0.000006s] propagating SemilatticeInf ℕ to subgoal SemilatticeInf ℕ of PartialOrder ℕ ▶
[] [0.000058s] ✅ apply @NormedLatticeAddCommGroup.toLattice to Lattice ℕ ▶
[] [0.000069s] ✅ apply @ConditionallyCompleteLattice.toLattice to Lattice ℕ ▶
[] [0.000062s] ✅ apply @ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice to ConditionallyCompleteLattice ℕ ▶
[] [0.000056s] ✅ apply @ConditionallyCompleteLinearOrderedField.toConditionallyCompleteLinearOrder to ConditionallyCompleteLinearOrder
ℕ ▶
[] [0.000060s] ✅ apply @ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder to ConditionallyCompleteLinearOrder
ℕ ▶
[] [0.000039s] ✅ apply Nat.instConditionallyCompleteLinearOrderBotNat to ConditionallyCompleteLinearOrderBot ℕ ▶
[resume] [0.000006s] propagating ConditionallyCompleteLinearOrderBot
ℕ to subgoal ConditionallyCompleteLinearOrderBot
ℕ of ConditionallyCompleteLinearOrder ℕ ▶
[resume] [0.000005s] propagating ConditionallyCompleteLinearOrder
ℕ to subgoal ConditionallyCompleteLinearOrder
ℕ of ConditionallyCompleteLattice ℕ ▶
[resume] [0.000004s] propagating ConditionallyCompleteLattice ℕ to subgoal ConditionallyCompleteLattice ℕ of Lattice ℕ ▶
[] [0.000055s] ✅ apply @CompleteLinearOrder.toConditionallyCompleteLinearOrderBot to ConditionallyCompleteLinearOrderBot ℕ ▶
[] [0.000051s] ✅ apply @CompleteLattice.toConditionallyCompleteLattice to ConditionallyCompleteLattice ℕ ▶
[] [0.000048s] ✅ apply @CompleteLattice.toLattice to Lattice ℕ ▶
[] [0.000060s] ✅ apply @GeneralizedCoheytingAlgebra.toLattice to Lattice ℕ ▶
[] [0.000060s] ✅ apply @CoheytingAlgebra.toGeneralizedCoheytingAlgebra to GeneralizedCoheytingAlgebra ℕ ▶
[] [0.000058s] ✅ apply @BiheytingAlgebra.toCoheytingAlgebra to CoheytingAlgebra ℕ ▶
[] [0.000061s] ✅ apply @BooleanAlgebra.toBiheytingAlgebra to BiheytingAlgebra ℕ ▶
[] [0.000047s] ✅ apply @CompleteBooleanAlgebra.toBooleanAlgebra to BooleanAlgebra ℕ ▶
[] [0.000059s] ✅ apply @GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra to GeneralizedCoheytingAlgebra ℕ ▶
[] [0.000049s] ✅ apply @BooleanAlgebra.toGeneralizedBooleanAlgebra to GeneralizedBooleanAlgebra ℕ ▶
[] [0.000057s] ✅ apply @GeneralizedHeytingAlgebra.toLattice to Lattice ℕ ▶
[] [0.000059s] ✅ apply @HeytingAlgebra.toGeneralizedHeytingAlgebra to GeneralizedHeytingAlgebra ℕ ▶
[] [0.000046s] ✅ apply @BiheytingAlgebra.toHeytingAlgebra to HeytingAlgebra ℕ ▶
[] [0.000058s] ✅ apply @DistribLattice.toLattice to Lattice ℕ ▶
[] [0.000036s] ✅ apply instDistribLatticeNat to DistribLattice ℕ ▶
[resume] [0.000012s] propagating DistribLattice ℕ to subgoal DistribLattice ℕ of Lattice ℕ ▶
[] [0.000044s] ✅ apply @BooleanAlgebra.toDistribLattice to DistribLattice ℕ ▶
[] [0.000044s] ✅ apply @GeneralizedBooleanAlgebra.toDistribLattice to DistribLattice ℕ ▶
[] [0.000046s] ✅ apply @Coframe.toDistribLattice to DistribLattice ℕ ▶
[] [0.000044s] ✅ apply @Frame.toDistribLattice to DistribLattice ℕ ▶
[] [0.000040s] ✅ apply @CoheytingAlgebra.toDistribLattice to DistribLattice ℕ ▶
[] [0.000040s] ✅ apply @GeneralizedCoheytingAlgebra.toDistribLattice to DistribLattice ℕ ▶
[] [0.000043s] ✅ apply @GeneralizedHeytingAlgebra.toDistribLattice to DistribLattice ℕ ▶
[] [0.000070s] ✅ apply @instDistribLattice to DistribLattice ℕ ▶
[] [0.000038s] ✅ apply Nat.linearOrder to LinearOrder ℕ ▶
[resume] [0.000006s] propagating LinearOrder ℕ to subgoal LinearOrder ℕ of DistribLattice ℕ ▶
[] [0.000055s] ✅ apply @NonemptyFiniteLinearOrder.toLinearOrder to LinearOrder ℕ ▶
[] [0.000046s] ✅ apply instLinearOrder to LinearOrder ℕ ▶
[resume] [0.000005s] propagating ConditionallyCompleteLinearOrder
ℕ to subgoal ConditionallyCompleteLinearOrder
ℕ of LinearOrder ℕ ▶
[] [0.000056s] ✅ apply @CompleteLinearOrder.toLinearOrder to LinearOrder ℕ ▶
[] [0.000046s] ✅ apply @LinearOrderedRing.toLinearOrder to LinearOrder ℕ ▶
[] [0.000044s] ✅ apply @LinearOrderedCommGroup.toLinearOrder to LinearOrder ℕ ▶
[] [0.000041s] ✅ apply @LinearOrderedAddCommGroup.toLinearOrder to LinearOrder ℕ ▶
[] 1086 more entries... ▼
[] [0.000048s] ✅ apply @LinearOrderedCommMonoid.toLinearOrder to LinearOrder ℕ ▶
[resume] [0.000006s] propagating LinearOrderedCommMonoid ℕ to subgoal LinearOrderedCommMonoid ℕ of LinearOrder ℕ ▶
[] [0.000046s] ✅ apply @LinearOrderedAddCommMonoid.toLinearOrder to LinearOrder ℕ ▶
[resume] [0.000005s] propagating LinearOrderedAddCommMonoid ℕ to subgoal LinearOrderedAddCommMonoid ℕ of LinearOrder ℕ ▶
[] [0.000046s] ✅ apply @LinearOrder.toLattice to Lattice ℕ ▶
[resume] [0.000005s] propagating LinearOrder ℕ to subgoal LinearOrder ℕ of Lattice ℕ ▶
[] [0.000064s] ✅ apply @SemilatticeSup.toPartialOrder to PartialOrder ℕ ▶
[] [0.000061s] ✅ apply @IdemCommSemiring.toSemilatticeSup to SemilatticeSup ℕ ▶
[] [0.000045s] ✅ apply @IdemSemiring.toSemilatticeSup to SemilatticeSup ℕ ▶
[] [0.000043s] ✅ apply @Lattice.toSemilatticeSup to SemilatticeSup ℕ ▶
[resume] [0.000005s] propagating Lattice ℕ to subgoal Lattice ℕ of SemilatticeSup ℕ ▶
[resume] [0.000005s] propagating SemilatticeSup ℕ to subgoal SemilatticeSup ℕ of PartialOrder ℕ ▶
[] [0.000043s] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.semilatticeSup to SemilatticeSup ℕ ▶
[resume] [0.000005s] propagating CanonicallyLinearOrderedAddCommMonoid
ℕ to subgoal CanonicallyLinearOrderedAddCommMonoid
ℕ of SemilatticeSup ℕ ▶
[] [0.000058s] ✅ apply @CanonicallyLinearOrderedCommMonoid.semilatticeSup to SemilatticeSup ℕ ▶
[] [0.000045s] ✅ apply @LinearOrder.toPartialOrder to PartialOrder ℕ ▶
[resume] [0.000005s] propagating LinearOrder ℕ to subgoal LinearOrder ℕ of PartialOrder ℕ ▶
[] [0.000069s] ✅ apply @SetLike.instPartialOrder to PartialOrder ℕ ▶
[] [0.000212s] ✅ apply Nat.AtLeastTwo.toNeZero to NeZero 2 ▶
[] [0.000132s] ✅ apply @instNatAtLeastTwo to Nat.AtLeastTwo 2 ▶
[resume] [0.000008s] propagating Nat.AtLeastTwo (0 + 2) to subgoal Nat.AtLeastTwo 2 of NeZero 2 ▶
[resume] [0.000008s] propagating NeZero 2 to subgoal NeZero 2 of Inhabited (Fin 2) ▶
[] [0.000179s] ✅ apply @Invertible.ne_zero to NeZero 2 ▶
[resume] [0.000036s] propagating Nontrivial ℕ to subgoal Nontrivial ℕ of NeZero 2 ▶
[] [0.000397s] ❌ apply @invertibleTwo to Invertible 2 ▶
[] [0.000209s] ✅ apply @NeZero.of_gt' to NeZero 2 ▶
[resume] [0.000044s] propagating One ℕ to subgoal One ℕ of NeZero 2 ▶
[] [0.000267s] ✅ apply Nat.Prime.one_lt' to Fact (1 < 2) ▶
[] [0.000040s] ✅ apply Nat.fact_prime_two to Fact (Nat.Prime 2) ▶
[resume] [0.000007s] propagating Fact (Nat.Prime 2) to subgoal Fact (Nat.Prime 2) of Fact (1 < 2) ▶
[resume] [0.000010s] propagating Fact (1 < 2) to subgoal Fact (1 < 2) of NeZero 2 ▶
[resume] [0.000007s] propagating NeZero 2 to subgoal NeZero 2 of Inhabited (Fin 2) ▶
[] [0.000165s] ✅ apply @Fin.instInhabitedFinHAddNatInstHAddInstAddNatOfNat to Inhabited (Fin 2) ▶
[resume] [0.000007s] propagating Inhabited (Fin (1 + 1)) to subgoal Inhabited (Fin 2) of Nonempty (Fin 2) ▶
[] [0.000076s] ❌ apply @instInhabited to Inhabited (Fin 2) ▶
[] [0.000074s] ✅ apply @Unique.instInhabited to Inhabited (Fin 2) ▶
[] [0.000092s] ✅ apply @Nontrivial.to_nonempty to Nonempty (Fin 2) ▶
[] [0.000139s] ✅ apply @Fin.nontrivial to Nontrivial (Fin 2) ▶
[resume] [0.000006s] propagating Nontrivial (Fin (0 + 2)) to subgoal Nontrivial (Fin 2) of Nonempty (Fin 2) ▶
[] [0.000074s] ✅ apply @LocalRing.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000401s] ❌ apply @DirectSum.GradeZero.semiring to Semiring (Fin 2) ▶
[] [0.000073s] ✅ apply @IdemSemiring.toSemiring to Semiring (Fin 2) ▶
[] [0.000063s] ✅ apply @KleeneAlgebra.toIdemSemiring to IdemSemiring (Fin 2) ▶
[] [0.000068s] ✅ apply @IdemCommSemiring.toIdemSemiring to IdemSemiring (Fin 2) ▶
[] [0.000058s] ✅ apply @DivisionSemiring.toSemiring to Semiring (Fin 2) ▶
[] [0.000058s] ✅ apply @Semifield.toDivisionSemiring to DivisionSemiring (Fin 2) ▶
[] [0.000060s] ✅ apply @LinearOrderedSemifield.toSemifield to Semifield (Fin 2) ▶
[] [0.000059s] ✅ apply @CanonicallyLinearOrderedSemifield.toLinearOrderedSemifield to LinearOrderedSemifield (Fin 2) ▶
[] [0.000057s] ✅ apply @LinearOrderedField.toLinearOrderedSemifield to LinearOrderedSemifield (Fin 2) ▶
[] [0.000062s] ✅ apply @ConditionallyCompleteLinearOrderedField.toLinearOrderedField to LinearOrderedField (Fin 2) ▶
[] 1036 more entries... ▼
[] [0.000049s] ✅ apply @NormedLinearOrderedField.toLinearOrderedField to LinearOrderedField (Fin 2) ▶
[] [0.000056s] ✅ apply @Field.toSemifield to Semifield (Fin 2) ▶
[] [0.000061s] ✅ apply @NormedField.toField to Field (Fin 2) ▶
[] [0.000055s] ✅ apply @DenselyNormedField.toNormedField to NormedField (Fin 2) ▶
[] [0.000075s] ✅ apply @RCLike.toDenselyNormedField to DenselyNormedField (Fin 2) ▶
[] [0.000062s] ✅ apply @NontriviallyNormedField.toNormedField to NormedField (Fin 2) ▶
[] [0.000052s] ✅ apply @DenselyNormedField.toNontriviallyNormedField to NontriviallyNormedField (Fin 2) ▶
[] [0.000051s] ✅ apply NormedLinearOrderedField.toNormedField to NormedField (Fin 2) ▶
[] [0.000042s] ✅ apply @LinearOrderedField.toField to Field (Fin 2) ▶
[] [0.000077s] ✅ apply littleWedderburn to Field (Fin 2) ▶
[] [0.000065s] ✅ apply @NormedDivisionRing.toDivisionRing to DivisionRing (Fin 2) ▶
[] [0.000050s] ✅ apply @NormedField.toNormedDivisionRing to NormedDivisionRing (Fin 2) ▶
[] [0.000041s] ✅ apply @Field.toDivisionRing to DivisionRing (Fin 2) ▶
[] [0.000050s] ✅ apply @DivisionRing.toDivisionSemiring to DivisionSemiring (Fin 2) ▶
[] [0.000054s] ✅ apply @StrictOrderedSemiring.toSemiring to Semiring (Fin 2) ▶
[] [0.000053s] ✅ apply @LinearOrderedSemiring.toStrictOrderedSemiring to StrictOrderedSemiring (Fin 2) ▶
[] [0.000056s] ✅ apply @LinearOrderedCommSemiring.toLinearOrderedSemiring to LinearOrderedSemiring (Fin 2) ▶
[] [0.000045s] ✅ apply @LinearOrderedSemifield.toLinearOrderedCommSemiring to LinearOrderedCommSemiring (Fin 2) ▶
[] [0.000050s] ✅ apply @LinearOrderedCommRing.toLinearOrderedCommSemiring to LinearOrderedCommSemiring (Fin 2) ▶
[] [0.000044s] ✅ apply @LinearOrderedField.toLinearOrderedCommRing to LinearOrderedCommRing (Fin 2) ▶
[] [0.000056s] ✅ apply @LinearOrderedRing.toLinearOrderedSemiring to LinearOrderedSemiring (Fin 2) ▶
[] [0.000046s] ✅ apply @LinearOrderedCommRing.toLinearOrderedRing to LinearOrderedRing (Fin 2) ▶
[] [0.000051s] ✅ apply @StrictOrderedCommSemiring.toStrictOrderedSemiring to StrictOrderedSemiring (Fin 2) ▶
[] [0.000042s] ✅ apply @LinearOrderedCommSemiring.toStrictOrderedCommSemiring to StrictOrderedCommSemiring (Fin 2) ▶
[] [0.000055s] ✅ apply @StrictOrderedCommRing.toStrictOrderedCommSemiring to StrictOrderedCommSemiring (Fin 2) ▶
[] [0.000048s] ✅ apply @LinearOrderedCommRing.toStrictOrderedCommRing to StrictOrderedCommRing (Fin 2) ▶
[] [0.000055s] ✅ apply @StrictOrderedRing.toStrictOrderedSemiring to StrictOrderedSemiring (Fin 2) ▶
[] [0.000046s] ✅ apply @LinearOrderedRing.toStrictOrderedRing to StrictOrderedRing (Fin 2) ▶
[] [0.000047s] ✅ apply @StrictOrderedCommRing.toStrictOrderedRing to StrictOrderedRing (Fin 2) ▶
[] [0.000054s] ✅ apply @OrderedSemiring.toSemiring to Semiring (Fin 2) ▶
[] [0.000058s] ✅ apply @OrderedCommSemiring.toOrderedSemiring to OrderedSemiring (Fin 2) ▶
[] [0.000057s] ✅ apply @CanonicallyOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring (Fin 2) ▶
[] [0.000052s] ✅ apply @CanonicallyLinearOrderedSemifield.toCanonicallyOrderedCommSemiring to CanonicallyOrderedCommSemiring
(Fin 2) ▶
[] [0.000041s] ✅ apply @StrictOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring (Fin 2) ▶
[] [0.000052s] ✅ apply @OrderedCommRing.toOrderedCommSemiring to OrderedCommSemiring (Fin 2) ▶
[] [0.000046s] ✅ apply @StrictOrderedCommRing.toOrderedCommRing to OrderedCommRing (Fin 2) ▶
[] [0.000047s] ✅ apply @StrictOrderedSemiring.toOrderedSemiring to OrderedSemiring (Fin 2) ▶
[] [0.000050s] ✅ apply @OrderedRing.toOrderedSemiring to OrderedSemiring (Fin 2) ▶
[] [0.000044s] ✅ apply @OrderedCommRing.toOrderedRing to OrderedRing (Fin 2) ▶
[] [0.000042s] ✅ apply @StrictOrderedRing.toOrderedRing to OrderedRing (Fin 2) ▶
[] [0.000057s] ✅ apply @CommSemiring.toSemiring to Semiring (Fin 2) ▶
[] [0.000495s] ❌ apply @DirectSum.GradeZero.commSemiring to CommSemiring (Fin 2) ▶
[] [0.000079s] ✅ apply @IdemCommSemiring.toCommSemiring to CommSemiring (Fin 2) ▶
[] [0.000052s] ✅ apply @Semifield.toCommSemiring to CommSemiring (Fin 2) ▶
[] [0.000046s] ✅ apply @CanonicallyOrderedCommSemiring.toCommSemiring to CommSemiring (Fin 2) ▶
[] [0.000045s] ✅ apply @StrictOrderedCommSemiring.toCommSemiring to CommSemiring (Fin 2) ▶
[] [0.000043s] ✅ apply @OrderedCommSemiring.toCommSemiring to CommSemiring (Fin 2) ▶
[] [0.000068s] ✅ apply @CommRing.toCommSemiring to CommSemiring (Fin 2) ▶
[] [0.000061s] ✅ apply Fin.instCommRing to CommRing (Fin 2) ▶
[resume] [0.000009s] propagating NeZero 2 to subgoal NeZero 2 of CommRing (Fin 2) ▶
[] 986 more entries... ▼
[resume] [0.000005s] propagating CommRing (Fin 2) to subgoal CommRing (Fin 2) of CommSemiring (Fin 2) ▶
[resume] [0.000005s] propagating CommSemiring (Fin 2) to subgoal CommSemiring (Fin 2) of Semiring (Fin 2) ▶
[resume] [0.000028s] propagating Semiring (Fin 2) to subgoal Semiring (Fin 2) of Nontrivial (Fin 2) ▶
[resume] [0.000007s] propagating NeZero 2 to subgoal NeZero 2 of CommRing (Fin 2) ▶
[resume] [0.000016s] propagating NeZero 2 to subgoal NeZero 2 of CommRing (Fin 2) ▶
[resume] [0.000008s] propagating NeZero (1 + 1) to subgoal NeZero 2 of CommRing (Fin 2) ▶
[] [0.000416s] ✅ apply @HenselianLocalRing.toLocalRing to LocalRing (Fin 2) ▶
[] [0.008549s] ❌ apply Field.henselian to HenselianLocalRing (Fin 2) ▶
[] [0.000197s] ✅ apply @DiscreteValuationRing.toLocalRing to LocalRing (Fin 2) ▶
[] [0.000158s] ✅ apply @IsDedekindDomain.toIsDomain to IsDomain (Fin 2) ▶
[] [0.000105s] ✅ apply instIsDedekindDomain to IsDedekindDomain (Fin 2) ▶
[] [0.000083s] ✅ apply IsPrincipalIdealRing.isDedekindDomain to IsDedekindDomain (Fin 2) ▶
[] [0.017977s] ❌ apply @Field.isDomain to IsDomain (Fin 2) ▶
[] [0.012582s] ❌ apply @DivisionRing.isDomain to IsDomain (Fin 2) ▶
[] [0.005813s] ❌ apply @LinearOrderedRing.isDomain to IsDomain (Fin 2) ▶
[] [0.025721s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain (Fin 2) ▶
[] [0.000179s] ✅ apply ValuationRing.localRing to LocalRing (Fin 2) ▶
[] [0.021049s] ❌ apply Field.instLocalRingToSemiringToDivisionSemiringToSemifield to LocalRing (Fin 2) ▶
[] [0.000903s] ❌ apply @DirectSum.GradeZero.commRing to CommRing (Fin 2) ▶
[] [0.000093s] ✅ apply @EuclideanDomain.toCommRing to CommRing (Fin 2) ▶
[] [0.000060s] ✅ apply @Field.toEuclideanDomain to EuclideanDomain (Fin 2) ▶
[] [0.000053s] ✅ apply @Field.toCommRing to CommRing (Fin 2) ▶
[] [0.000050s] ✅ apply @StrictOrderedCommRing.toCommRing to CommRing (Fin 2) ▶
[] [0.000046s] ✅ apply @OrderedCommRing.toCommRing to CommRing (Fin 2) ▶
[] [0.000062s] ✅ apply @SeminormedCommRing.toCommRing to CommRing (Fin 2) ▶
[] [0.000070s] ✅ apply @NormedCommRing.toSeminormedCommRing to SeminormedCommRing (Fin 2) ▶
[] [0.000053s] ✅ apply @NormedField.toNormedCommRing to NormedCommRing (Fin 2) ▶
[] [0.000057s] ✅ apply @BooleanRing.toCommRing to CommRing (Fin 2) ▶
[] [0.000073s] ✅ apply @Ring.toSemiring to Semiring (Fin 2) ▶
[] [0.000069s] ✅ apply @NormedRing.toRing to Ring (Fin 2) ▶
[] [0.000052s] ✅ apply @NormedCommRing.toNormedRing to NormedRing (Fin 2) ▶
[] [0.000045s] ✅ apply @NormedDivisionRing.toNormedRing to NormedRing (Fin 2) ▶
[] [0.000058s] ✅ apply @SeminormedRing.toRing to Ring (Fin 2) ▶
[] [0.000047s] ✅ apply @SeminormedCommRing.toSeminormedRing to SeminormedRing (Fin 2) ▶
[] [0.000046s] ✅ apply @NormedRing.toSeminormedRing to SeminormedRing (Fin 2) ▶
[] [0.000404s] ❌ apply @DirectSum.GradeZero.ring to Ring (Fin 2) ▶
[] [0.000071s] ✅ apply @BooleanRing.toRing to Ring (Fin 2) ▶
[] [0.000052s] ✅ apply @DivisionRing.toRing to Ring (Fin 2) ▶
[] [0.000235s] ✅ apply @StrictOrderedRing.toRing to Ring (Fin 2) ▶
[] [0.000066s] ✅ apply @OrderedRing.toRing to Ring (Fin 2) ▶
[] [0.000052s] ✅ apply @CommRing.toRing to Ring (Fin 2) ▶
[resume] [0.000012s] propagating CommRing (Fin 2) to subgoal CommRing (Fin 2) of Ring (Fin 2) ▶
[resume] [0.000006s] propagating Ring (Fin 2) to subgoal Ring (Fin 2) of Semiring (Fin 2) ▶
[] [0.000051s] ✅ apply @instSemiring to Semiring (Fin 2) ▶
[resume] [0.000006s] propagating Ring (Fin 2) to subgoal Ring (Fin 2) of Semiring (Fin 2) ▶
[] [0.000090s] ✅ apply @IsSimpleAddGroup.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000069s] ✅ apply @NormedAddGroup.toAddGroup to AddGroup (Fin 2) ▶
[] [0.000064s] ✅ apply @NormedAddCommGroup.toNormedAddGroup to NormedAddGroup (Fin 2) ▶
[] [0.000062s] ✅ apply @NormedLatticeAddCommGroup.toNormedAddCommGroup to NormedAddCommGroup (Fin 2) ▶
[] [0.000058s] ✅ apply @NormedOrderedAddGroup.toNormedAddCommGroup to NormedAddCommGroup (Fin 2) ▶
[] 936 more entries... ▼
[] [0.000058s] ✅ apply @NormedLinearOrderedAddGroup.toNormedOrderedAddGroup to NormedOrderedAddGroup (Fin 2) ▶
[] [0.000206s] ✅ apply @NonUnitalNormedRing.toNormedAddCommGroup to NormedAddCommGroup (Fin 2) ▶
[] [0.000080s] ✅ apply @NonUnitalNormedCommRing.toNonUnitalNormedRing to NonUnitalNormedRing (Fin 2) ▶
[] [0.000058s] ✅ apply @NormedCommRing.toNonUnitalNormedCommRing to NonUnitalNormedCommRing (Fin 2) ▶
[] [0.000051s] ✅ apply @NormedRing.toNonUnitalNormedRing to NonUnitalNormedRing (Fin 2) ▶
[] [0.000068s] ✅ apply @SeminormedAddGroup.toAddGroup to AddGroup (Fin 2) ▶
[] [0.000073s] ✅ apply @SeminormedAddCommGroup.toSeminormedAddGroup to SeminormedAddGroup (Fin 2) ▶
[] [0.000077s] ✅ apply @NonUnitalSeminormedRing.toSeminormedAddCommGroup to SeminormedAddCommGroup (Fin 2) ▶
[] [0.000063s] ✅ apply @NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing to NonUnitalSeminormedRing (Fin 2) ▶
[] [0.000055s] ✅ apply @SeminormedCommRing.toNonUnitalSeminormedCommRing to NonUnitalSeminormedCommRing (Fin 2) ▶
[] [0.000051s] ✅ apply @NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing to NonUnitalSeminormedCommRing (Fin 2) ▶
[] [0.000044s] ✅ apply @NonUnitalNormedRing.toNonUnitalSeminormedRing to NonUnitalSeminormedRing (Fin 2) ▶
[] [0.000046s] ✅ apply @SeminormedRing.toNonUnitalSeminormedRing to NonUnitalSeminormedRing (Fin 2) ▶
[] [0.000067s] ✅ apply @NormedAddCommGroup.toSeminormedAddCommGroup to SeminormedAddCommGroup (Fin 2) ▶
[] [0.000061s] ✅ apply @NormedAddGroup.toSeminormedAddGroup to SeminormedAddGroup (Fin 2) ▶
[] [0.000061s] ✅ apply @AddGroupWithOne.toAddGroup to AddGroup (Fin 2) ▶
[] [0.000049s] ✅ apply @Ring.toAddGroupWithOne to AddGroupWithOne (Fin 2) ▶
[resume] [0.000008s] propagating Ring (Fin 2) to subgoal Ring (Fin 2) of AddGroupWithOne (Fin 2) ▶
[resume] [0.000005s] propagating AddGroupWithOne (Fin 2) to subgoal AddGroupWithOne (Fin 2) of AddGroup (Fin 2) ▶
[resume] [0.000016s] propagating AddGroup (Fin 2) to subgoal AddGroup (Fin 2) of Nontrivial (Fin 2) ▶
[] [0.000057s] ✅ apply @AddCommGroupWithOne.toAddGroupWithOne to AddGroupWithOne (Fin 2) ▶
[] [0.000068s] ✅ apply @NonAssocRing.toAddCommGroupWithOne to AddCommGroupWithOne (Fin 2) ▶
[] [0.000051s] ✅ apply @Ring.toNonAssocRing to NonAssocRing (Fin 2) ▶
[resume] [0.000006s] propagating Ring (Fin 2) to subgoal Ring (Fin 2) of NonAssocRing (Fin 2) ▶
[resume] [0.000005s] propagating NonAssocRing (Fin 2) to subgoal NonAssocRing (Fin 2) of AddCommGroupWithOne (Fin 2) ▶
[resume] [0.000005s] propagating AddCommGroupWithOne (Fin 2) to subgoal AddCommGroupWithOne (Fin 2) of AddGroupWithOne (Fin 2) ▶
[] [0.000046s] ✅ apply @CommRing.toAddCommGroupWithOne to AddCommGroupWithOne (Fin 2) ▶
[resume] [0.000005s] propagating CommRing (Fin 2) to subgoal CommRing (Fin 2) of AddCommGroupWithOne (Fin 2) ▶
[] [0.000074s] ✅ apply @AddCommGroup.toAddGroup to AddGroup (Fin 2) ▶
[] [0.000061s] ✅ apply Fin.addCommGroup to AddCommGroup (Fin 2) ▶
[resume] [0.000009s] propagating NeZero 2 to subgoal NeZero 2 of AddCommGroup (Fin 2) ▶
[resume] [0.000005s] propagating AddCommGroup (Fin 2) to subgoal AddCommGroup (Fin 2) of AddGroup (Fin 2) ▶
[resume] [0.000007s] propagating NeZero 2 to subgoal NeZero 2 of AddCommGroup (Fin 2) ▶
[resume] [0.000006s] propagating NeZero 2 to subgoal NeZero 2 of AddCommGroup (Fin 2) ▶
[resume] [0.000007s] propagating NeZero (1 + 1) to subgoal NeZero 2 of AddCommGroup (Fin 2) ▶
[] [0.000056s] ✅ apply @NormedAddCommGroup.toAddCommGroup to AddCommGroup (Fin 2) ▶
[] [0.000045s] ✅ apply @SeminormedAddCommGroup.toAddCommGroup to AddCommGroup (Fin 2) ▶
[] [0.000061s] ✅ apply @LieRing.toAddCommGroup to AddCommGroup (Fin 2) ▶
[] [0.000055s] ✅ apply @LieRing.ofAssociativeRing to LieRing (Fin 2) ▶
[resume] [0.000006s] propagating Ring (Fin 2) to subgoal Ring (Fin 2) of LieRing (Fin 2) ▶
[resume] [0.000005s] propagating LieRing (Fin 2) to subgoal LieRing (Fin 2) of AddCommGroup (Fin 2) ▶
[] [0.000069s] ✅ apply @OrderedAddCommGroup.toAddCommGroup to AddCommGroup (Fin 2) ▶
[] [0.000062s] ✅ apply @NormedOrderedAddGroup.toOrderedAddCommGroup to OrderedAddCommGroup (Fin 2) ▶
[] [0.000044s] ✅ apply @StrictOrderedRing.toOrderedAddCommGroup to OrderedAddCommGroup (Fin 2) ▶
[] [0.000044s] ✅ apply @OrderedRing.toOrderedAddCommGroup to OrderedAddCommGroup (Fin 2) ▶
[] [0.000062s] ✅ apply @LinearOrderedAddCommGroup.toOrderedAddCommGroup to OrderedAddCommGroup (Fin 2) ▶
[] [0.000059s] ✅ apply @NormedLinearOrderedAddGroup.toLinearOrderedAddCommGroup to LinearOrderedAddCommGroup (Fin 2) ▶
[] [0.000043s] ✅ apply @LinearOrderedRing.toLinearOrderedAddCommGroup to LinearOrderedAddCommGroup (Fin 2) ▶
[] [0.000070s] ✅ apply @StarOrderedRing.toOrderedAddCommGroup to OrderedAddCommGroup (Fin 2) ▶
[] [0.000061s] ✅ apply @NonUnitalNormedRing.toNonUnitalRing to NonUnitalRing (Fin 2) ▶
[] 886 more entries... ▼
[] [0.000046s] ✅ apply @NonUnitalSeminormedRing.toNonUnitalRing to NonUnitalRing (Fin 2) ▶
[] [0.000057s] ✅ apply @NonUnitalCommRing.toNonUnitalRing to NonUnitalRing (Fin 2) ▶
[] [0.000049s] ✅ apply @NonUnitalSeminormedCommRing.toNonUnitalCommRing to NonUnitalCommRing (Fin 2) ▶
[] [0.000043s] ✅ apply @CommRing.toNonUnitalCommRing to NonUnitalCommRing (Fin 2) ▶
[resume] [0.000007s] propagating CommRing (Fin 2) to subgoal CommRing (Fin 2) of NonUnitalCommRing (Fin 2) ▶
[resume] [0.000006s] propagating NonUnitalCommRing (Fin 2) to subgoal NonUnitalCommRing (Fin 2) of NonUnitalRing (Fin 2) ▶
[resume] [0.000035s] propagating NonUnitalRing (Fin 2) to subgoal NonUnitalRing (Fin 2) of OrderedAddCommGroup (Fin 2) ▶
[] [0.000066s] ✅ apply @Fin.instPartialOrderFin to PartialOrder (Fin 2) ▶
[resume] [0.000028s] propagating PartialOrder (Fin 2) to subgoal PartialOrder (Fin 2) of OrderedAddCommGroup (Fin 2) ▶
[] [0.006087s] ❌ apply @RCLike.toStarRing to StarRing (Fin 2) ▶
[] [0.000095s] ✅ apply @CompletePartialOrder.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000082s] ✅ apply @CompleteLattice.toCompletePartialOrder to CompletePartialOrder (Fin 2) ▶
[] [0.000083s] ✅ apply @CompletelyDistribLattice.toCompleteLattice to CompleteLattice (Fin 2) ▶
[] [0.000063s] ✅ apply @CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice to CompletelyDistribLattice (Fin 2) ▶
[] [0.000060s] ✅ apply @CompleteLinearOrder.toCompletelyDistribLattice to CompletelyDistribLattice (Fin 2) ▶
[] [0.000175s] ✅ apply @Fin.completeLinearOrder to CompleteLinearOrder (Fin 2) ▶
[resume] [0.000006s] propagating CompleteLinearOrder
(Fin
(1 +
1)) to subgoal CompleteLinearOrder
(Fin 2) of CompletelyDistribLattice (Fin 2) ▶
[resume] [0.000006s] propagating CompletelyDistribLattice
(Fin
2) to subgoal CompletelyDistribLattice
(Fin 2) of CompleteLattice (Fin 2) ▶
[resume] [0.000006s] propagating CompleteLattice (Fin 2) to subgoal CompleteLattice (Fin 2) of CompletePartialOrder (Fin 2) ▶
[resume] [0.000005s] propagating CompletePartialOrder (Fin 2) to subgoal CompletePartialOrder (Fin 2) of PartialOrder (Fin 2) ▶
[] [0.000069s] ✅ apply @Order.Coframe.toCompleteLattice to CompleteLattice (Fin 2) ▶
[] [0.000066s] ✅ apply @CompleteDistribLattice.toCoframe to Order.Coframe (Fin 2) ▶
[] [0.000062s] ✅ apply @CompleteBooleanAlgebra.toCompleteDistribLattice to CompleteDistribLattice (Fin 2) ▶
[] [0.000057s] ✅ apply @CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra to CompleteBooleanAlgebra (Fin 2) ▶
[] [0.000046s] ✅ apply @CompletelyDistribLattice.toCompleteDistribLattice to CompleteDistribLattice (Fin 2) ▶
[resume] [0.000007s] propagating CompletelyDistribLattice
(Fin
2) to subgoal CompletelyDistribLattice
(Fin 2) of CompleteDistribLattice (Fin 2) ▶
[resume] [0.000005s] propagating CompleteDistribLattice
(Fin
2) to subgoal CompleteDistribLattice
(Fin 2) of Order.Coframe (Fin 2) ▶
[resume] [0.000005s] propagating Order.Coframe (Fin 2) to subgoal Order.Coframe (Fin 2) of CompleteLattice (Fin 2) ▶
[] [0.000060s] ✅ apply @Order.Frame.toCompleteLattice to CompleteLattice (Fin 2) ▶
[] [0.000047s] ✅ apply @CompleteDistribLattice.toFrame to Order.Frame (Fin 2) ▶
[resume] [0.000005s] propagating CompleteDistribLattice (Fin 2) to subgoal CompleteDistribLattice (Fin 2) of Order.Frame (Fin 2) ▶
[resume] [0.000005s] propagating Order.Frame (Fin 2) to subgoal Order.Frame (Fin 2) of CompleteLattice (Fin 2) ▶
[] [0.000045s] ✅ apply @CompleteLinearOrder.toCompleteLattice to CompleteLattice (Fin 2) ▶
[resume] [0.000006s] propagating CompleteLinearOrder
(Fin
(1 +
1)) to subgoal CompleteLinearOrder
(Fin 2) of CompleteLattice (Fin 2) ▶
[] [0.000079s] ✅ apply @OmegaCompletePartialOrder.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000054s] ✅ apply @CompletePartialOrder.toOmegaCompletePartialOrder to OmegaCompletePartialOrder (Fin 2) ▶
[resume] [0.000006s] propagating CompletePartialOrder
(Fin
2) to subgoal CompletePartialOrder
(Fin 2) of OmegaCompletePartialOrder (Fin 2) ▶
[resume] [0.000005s] propagating OmegaCompletePartialOrder
(Fin
2) to subgoal OmegaCompletePartialOrder
(Fin 2) of PartialOrder (Fin 2) ▶
[] [0.000048s] ✅ apply CompleteLattice.instOmegaCompletePartialOrder to OmegaCompletePartialOrder (Fin 2) ▶
[resume] [0.000005s] propagating CompleteLattice (Fin 2) to subgoal CompleteLattice (Fin 2) of OmegaCompletePartialOrder (Fin 2) ▶
[] [0.000062s] ✅ apply @CompleteSemilatticeInf.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000047s] ✅ apply @CompleteLattice.toCompleteSemilatticeInf to CompleteSemilatticeInf (Fin 2) ▶
[resume] [0.000005s] propagating CompleteLattice (Fin 2) to subgoal CompleteLattice (Fin 2) of CompleteSemilatticeInf (Fin 2) ▶
[resume] [0.000004s] propagating CompleteSemilatticeInf (Fin 2) to subgoal CompleteSemilatticeInf (Fin 2) of PartialOrder (Fin 2) ▶
[] [0.000062s] ✅ apply @CompleteSemilatticeSup.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000049s] ✅ apply @CompleteLattice.toCompleteSemilatticeSup to CompleteSemilatticeSup (Fin 2) ▶
[resume] [0.000005s] propagating CompleteLattice (Fin 2) to subgoal CompleteLattice (Fin 2) of CompleteSemilatticeSup (Fin 2) ▶
[resume] [0.000004s] propagating CompleteSemilatticeSup (Fin 2) to subgoal CompleteSemilatticeSup (Fin 2) of PartialOrder (Fin 2) ▶
[] [0.000044s] ✅ apply @StrictOrderedRing.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000044s] ✅ apply @StrictOrderedSemiring.toPartialOrder to PartialOrder (Fin 2) ▶
[] 836 more entries... ▼
[] [0.000043s] ✅ apply @OrderedRing.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000046s] ✅ apply @OrderedSemiring.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000061s] ✅ apply @OrderedCommGroup.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000071s] ✅ apply @NormedOrderedGroup.toOrderedCommGroup to OrderedCommGroup (Fin 2) ▶
[] [0.000060s] ✅ apply @NormedLinearOrderedGroup.toNormedOrderedGroup to NormedOrderedGroup (Fin 2) ▶
[] [0.000077s] ✅ apply @LinearOrderedCommGroup.toOrderedCommGroup to OrderedCommGroup (Fin 2) ▶
[] [0.000057s] ✅ apply @NormedLinearOrderedGroup.toLinearOrderedCommGroup to LinearOrderedCommGroup (Fin 2) ▶
[] [0.000048s] ✅ apply @OrderedAddCommGroup.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000058s] ✅ apply @OrderedCommMonoid.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000064s] ✅ apply @CanonicallyOrderedCommMonoid.toOrderedCommMonoid to OrderedCommMonoid (Fin 2) ▶
[] [0.000056s] ✅ apply @CanonicallyLinearOrderedCommMonoid.toCanonicallyOrderedCommMonoid to CanonicallyOrderedCommMonoid
(Fin 2) ▶
[] [0.000060s] ✅ apply @LinearOrderedCommMonoid.toOrderedCommMonoid to OrderedCommMonoid (Fin 2) ▶
[] [0.000060s] ✅ apply @LinearOrderedCommMonoidWithZero.toLinearOrderedCommMonoid to LinearOrderedCommMonoid (Fin 2) ▶
[] [0.000057s] ✅ apply @LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero to LinearOrderedCommMonoidWithZero
(Fin 2) ▶
[] [0.000055s] ✅ apply @CanonicallyLinearOrderedSemifield.toLinearOrderedCommGroupWithZero to LinearOrderedCommGroupWithZero
(Fin 2) ▶
[] [0.000054s] ✅ apply @CanonicallyLinearOrderedCommMonoid.toLinearOrderedCommMonoid to LinearOrderedCommMonoid (Fin 2) ▶
[] [0.000065s] ✅ apply @LinearOrderedCancelCommMonoid.toLinearOrderedCommMonoid to LinearOrderedCommMonoid (Fin 2) ▶
[] [0.000050s] ✅ apply @LinearOrderedCommGroup.toLinearOrderedCancelCommMonoid to LinearOrderedCancelCommMonoid (Fin 2) ▶
[] [0.000054s] ✅ apply @OrderedCancelCommMonoid.toOrderedCommMonoid to OrderedCommMonoid (Fin 2) ▶
[] [0.000047s] ✅ apply @LinearOrderedCancelCommMonoid.toOrderedCancelCommMonoid to OrderedCancelCommMonoid (Fin 2) ▶
[] [0.000044s] ✅ apply @OrderedCommGroup.toOrderedCancelCommMonoid to OrderedCancelCommMonoid (Fin 2) ▶
[] [0.000046s] ✅ apply @CanonicallyOrderedCommSemiring.toOrderedCommMonoid to OrderedCommMonoid (Fin 2) ▶
[] [0.000059s] ✅ apply @OrderedAddCommMonoid.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000055s] ✅ apply @OrderedSemiring.toOrderedAddCommMonoid to OrderedAddCommMonoid (Fin 2) ▶
[] [0.000060s] ✅ apply @CanonicallyOrderedAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid (Fin 2) ▶
[] [0.000051s] ✅ apply @CanonicallyOrderedCommSemiring.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid
(Fin 2) ▶
[] [0.000056s] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid
(Fin 2) ▶
[] [0.000053s] ✅ apply @CanonicallyLinearOrderedSemifield.toCanonicallyLinearOrderedAddCommMonoid to CanonicallyLinearOrderedAddCommMonoid
(Fin 2) ▶
[] [0.000043s] ✅ apply @IdemSemiring.toCanonicallyOrderedAddCommMonoid to CanonicallyOrderedAddCommMonoid (Fin 2) ▶
[] [0.000060s] ✅ apply @LinearOrderedAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid (Fin 2) ▶
[] [0.000063s] ✅ apply @LinearOrderedSemiring.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid (Fin 2) ▶
[] [0.000044s] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid
(Fin 2) ▶
[] [0.000054s] ✅ apply @LinearOrderedAddCommMonoidWithTop.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid
(Fin 2) ▶
[] [0.000057s] ✅ apply @LinearOrderedAddCommGroupWithTop.toLinearOrderedAddCommMonoidWithTop to LinearOrderedAddCommMonoidWithTop
(Fin 2) ▶
[] [0.000058s] ✅ apply @LinearOrderedCancelAddCommMonoid.toLinearOrderedAddCommMonoid to LinearOrderedAddCommMonoid (Fin 2) ▶
[] [0.000052s] ✅ apply @LinearOrderedCommSemiring.toLinearOrderedCancelAddCommMonoid to LinearOrderedCancelAddCommMonoid
(Fin 2) ▶
[] [0.000045s] ✅ apply @LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid to LinearOrderedCancelAddCommMonoid
(Fin 2) ▶
[] [0.000062s] ✅ apply @OrderedCancelAddCommMonoid.toOrderedAddCommMonoid to OrderedAddCommMonoid (Fin 2) ▶
[] [0.000055s] ✅ apply @StrictOrderedSemiring.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid (Fin 2) ▶
[] [0.000046s] ✅ apply @LinearOrderedCancelAddCommMonoid.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid (Fin 2) ▶
[] [0.000046s] ✅ apply @OrderedAddCommGroup.toOrderedCancelAddCommMonoid to OrderedCancelAddCommMonoid (Fin 2) ▶
[] [0.000067s] ✅ apply @StarOrderedRing.toOrderedAddCommMonoid to OrderedAddCommMonoid (Fin 2) ▶
[] [0.000060s] ✅ apply @NonUnitalCommSemiring.toNonUnitalSemiring to NonUnitalSemiring (Fin 2) ▶
[] [0.000050s] ✅ apply @NonUnitalCommRing.toNonUnitalCommSemiring to NonUnitalCommSemiring (Fin 2) ▶
[resume] [0.000008s] propagating NonUnitalCommRing (Fin 2) to subgoal NonUnitalCommRing (Fin 2) of NonUnitalCommSemiring (Fin 2) ▶
[resume] [0.000005s] propagating NonUnitalCommSemiring
(Fin
2) to subgoal NonUnitalCommSemiring
(Fin 2) of NonUnitalSemiring (Fin 2) ▶
[resume] [0.000003s] propagating NonUnitalSemiring (Fin 2) to subgoal NonUnitalSemiring (Fin 2) of OrderedAddCommMonoid (Fin 2) ▶
[resume] [0.000023s] propagating PartialOrder (Fin 2) to subgoal PartialOrder (Fin 2) of OrderedAddCommMonoid (Fin 2) ▶
[] [0.012673s] ❌ apply @RCLike.toStarRing to StarRing (Fin 2) ▶
[] [0.000087s] ✅ apply @CommSemiring.toNonUnitalCommSemiring to NonUnitalCommSemiring (Fin 2) ▶
[] 786 more entries... ▼
[resume] [0.000008s] propagating CommSemiring (Fin 2) to subgoal CommSemiring (Fin 2) of NonUnitalCommSemiring (Fin 2) ▶
[] [0.000066s] ✅ apply @Semiring.toNonUnitalSemiring to NonUnitalSemiring (Fin 2) ▶
[resume] [0.000007s] propagating Semiring (Fin 2) to subgoal Semiring (Fin 2) of NonUnitalSemiring (Fin 2) ▶
[] [0.000047s] ✅ apply @NonUnitalRing.toNonUnitalSemiring to NonUnitalSemiring (Fin 2) ▶
[resume] [0.000006s] propagating NonUnitalRing (Fin 2) to subgoal NonUnitalRing (Fin 2) of NonUnitalSemiring (Fin 2) ▶
[] [0.000066s] ✅ apply @SemilatticeInf.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000077s] ✅ apply @Lattice.toSemilatticeInf to SemilatticeInf (Fin 2) ▶
[] [0.000163s] ✅ apply @Fin.instLatticeFinHAddNatInstHAddInstAddNatOfNat to Lattice (Fin 2) ▶
[resume] [0.000006s] propagating Lattice (Fin (1 + 1)) to subgoal Lattice (Fin 2) of SemilatticeInf (Fin 2) ▶
[resume] [0.000006s] propagating SemilatticeInf (Fin 2) to subgoal SemilatticeInf (Fin 2) of PartialOrder (Fin 2) ▶
[] [0.000066s] ✅ apply @NormedLatticeAddCommGroup.toLattice to Lattice (Fin 2) ▶
[] [0.000061s] ✅ apply @ConditionallyCompleteLattice.toLattice to Lattice (Fin 2) ▶
[] [0.000067s] ✅ apply @ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice to ConditionallyCompleteLattice
(Fin 2) ▶
[] [0.000061s] ✅ apply @ConditionallyCompleteLinearOrderedField.toConditionallyCompleteLinearOrder to ConditionallyCompleteLinearOrder
(Fin 2) ▶
[] [0.000067s] ✅ apply @ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder to ConditionallyCompleteLinearOrder
(Fin 2) ▶
[] [0.000053s] ✅ apply @CompleteLinearOrder.toConditionallyCompleteLinearOrderBot to ConditionallyCompleteLinearOrderBot
(Fin 2) ▶
[resume] [0.000008s] propagating CompleteLinearOrder
(Fin
(1 +
1)) to subgoal CompleteLinearOrder
(Fin
2) of ConditionallyCompleteLinearOrderBot
(Fin 2) ▶
[resume] [0.000006s] propagating ConditionallyCompleteLinearOrderBot
(Fin
2) to subgoal ConditionallyCompleteLinearOrderBot
(Fin
2) of ConditionallyCompleteLinearOrder
(Fin 2) ▶
[resume] [0.000005s] propagating ConditionallyCompleteLinearOrder
(Fin
2) to subgoal ConditionallyCompleteLinearOrder
(Fin
2) of ConditionallyCompleteLattice (Fin 2) ▶
[resume] [0.000005s] propagating ConditionallyCompleteLattice
(Fin
2) to subgoal ConditionallyCompleteLattice
(Fin 2) of Lattice (Fin 2) ▶
[resume] [0.000005s] propagating Lattice (Fin 2) to subgoal Lattice (Fin 2) of SemilatticeInf (Fin 2) ▶
[] [0.000050s] ✅ apply @CompleteLattice.toConditionallyCompleteLattice to ConditionallyCompleteLattice (Fin 2) ▶
[resume] [0.000005s] propagating CompleteLattice
(Fin
2) to subgoal CompleteLattice
(Fin
2) of ConditionallyCompleteLattice (Fin 2) ▶
[] [0.000054s] ✅ apply @CompleteLattice.toLattice to Lattice (Fin 2) ▶
[resume] [0.000005s] propagating CompleteLattice (Fin 2) to subgoal CompleteLattice (Fin 2) of Lattice (Fin 2) ▶
[] [0.000059s] ✅ apply @GeneralizedCoheytingAlgebra.toLattice to Lattice (Fin 2) ▶
[] [0.000060s] ✅ apply @CoheytingAlgebra.toGeneralizedCoheytingAlgebra to GeneralizedCoheytingAlgebra (Fin 2) ▶
[] [0.000074s] ✅ apply @BiheytingAlgebra.toCoheytingAlgebra to CoheytingAlgebra (Fin 2) ▶
[] [0.000062s] ✅ apply @BooleanAlgebra.toBiheytingAlgebra to BiheytingAlgebra (Fin 2) ▶
[] [0.000049s] ✅ apply @CompleteBooleanAlgebra.toBooleanAlgebra to BooleanAlgebra (Fin 2) ▶
[] [0.000064s] ✅ apply @GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra to GeneralizedCoheytingAlgebra (Fin 2) ▶
[] [0.000069s] ✅ apply @BooleanAlgebra.toGeneralizedBooleanAlgebra to GeneralizedBooleanAlgebra (Fin 2) ▶
[] [0.000083s] ✅ apply @GeneralizedHeytingAlgebra.toLattice to Lattice (Fin 2) ▶
[] [0.000064s] ✅ apply @HeytingAlgebra.toGeneralizedHeytingAlgebra to GeneralizedHeytingAlgebra (Fin 2) ▶
[] [0.000057s] ✅ apply @BiheytingAlgebra.toHeytingAlgebra to HeytingAlgebra (Fin 2) ▶
[] [0.000065s] ✅ apply @DistribLattice.toLattice to Lattice (Fin 2) ▶
[] [0.000058s] ✅ apply @BooleanAlgebra.toDistribLattice to DistribLattice (Fin 2) ▶
[] [0.000045s] ✅ apply @GeneralizedBooleanAlgebra.toDistribLattice to DistribLattice (Fin 2) ▶
[] [0.000042s] ✅ apply @Coframe.toDistribLattice to DistribLattice (Fin 2) ▶
[resume] [0.000007s] propagating Order.Coframe (Fin 2) to subgoal Order.Coframe (Fin 2) of DistribLattice (Fin 2) ▶
[resume] [0.000005s] propagating DistribLattice (Fin 2) to subgoal DistribLattice (Fin 2) of Lattice (Fin 2) ▶
[] [0.000042s] ✅ apply @Frame.toDistribLattice to DistribLattice (Fin 2) ▶
[resume] [0.000005s] propagating Order.Frame (Fin 2) to subgoal Order.Frame (Fin 2) of DistribLattice (Fin 2) ▶
[] [0.000047s] ✅ apply @CoheytingAlgebra.toDistribLattice to DistribLattice (Fin 2) ▶
[] [0.000044s] ✅ apply @GeneralizedCoheytingAlgebra.toDistribLattice to DistribLattice (Fin 2) ▶
[] [0.000044s] ✅ apply @GeneralizedHeytingAlgebra.toDistribLattice to DistribLattice (Fin 2) ▶
[] [0.000076s] ✅ apply @instDistribLattice to DistribLattice (Fin 2) ▶
[] [0.000056s] ✅ apply @Fin.instLinearOrderFin to LinearOrder (Fin 2) ▶
[resume] [0.000005s] propagating LinearOrder (Fin 2) to subgoal LinearOrder (Fin 2) of DistribLattice (Fin 2) ▶
[] [0.000047s] ✅ apply @NonemptyFiniteLinearOrder.toLinearOrder to LinearOrder (Fin 2) ▶
[] 736 more entries... ▼
[resume] [0.000007s] propagating NonemptyFiniteLinearOrder
(Fin
(1 +
1)) to subgoal NonemptyFiniteLinearOrder
(Fin 2) of LinearOrder (Fin 2) ▶
[] [0.000055s] ✅ apply instLinearOrder to LinearOrder (Fin 2) ▶
[resume] [0.000005s] propagating ConditionallyCompleteLinearOrder
(Fin
2) to subgoal ConditionallyCompleteLinearOrder
(Fin 2) of LinearOrder (Fin 2) ▶
[] [0.000055s] ✅ apply @CompleteLinearOrder.toLinearOrder to LinearOrder (Fin 2) ▶
[resume] [0.000021s] propagating CompleteLinearOrder (Fin (1 + 1)) to subgoal CompleteLinearOrder (Fin 2) of LinearOrder (Fin 2) ▶
[] [0.000134s] ✅ apply @LinearOrderedRing.toLinearOrder to LinearOrder (Fin 2) ▶
[] [0.000064s] ✅ apply @LinearOrderedCommGroup.toLinearOrder to LinearOrder (Fin 2) ▶
[] [0.000046s] ✅ apply @LinearOrderedAddCommGroup.toLinearOrder to LinearOrder (Fin 2) ▶
[] [0.000047s] ✅ apply @LinearOrderedCommMonoid.toLinearOrder to LinearOrder (Fin 2) ▶
[] [0.000054s] ✅ apply @LinearOrderedAddCommMonoid.toLinearOrder to LinearOrder (Fin 2) ▶
[] [0.000045s] ✅ apply @LinearOrder.toLattice to Lattice (Fin 2) ▶
[resume] [0.000008s] propagating LinearOrder (Fin 2) to subgoal LinearOrder (Fin 2) of Lattice (Fin 2) ▶
[] [0.000074s] ✅ apply @SemilatticeSup.toPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000082s] ✅ apply @IdemCommSemiring.toSemilatticeSup to SemilatticeSup (Fin 2) ▶
[] [0.000045s] ✅ apply @IdemSemiring.toSemilatticeSup to SemilatticeSup (Fin 2) ▶
[] [0.000053s] ✅ apply @Lattice.toSemilatticeSup to SemilatticeSup (Fin 2) ▶
[resume] [0.000007s] propagating Lattice (Fin 2) to subgoal Lattice (Fin 2) of SemilatticeSup (Fin 2) ▶
[resume] [0.000012s] propagating SemilatticeSup (Fin 2) to subgoal SemilatticeSup (Fin 2) of PartialOrder (Fin 2) ▶
[resume] [0.000005s] propagating Lattice (Fin (1 + 1)) to subgoal Lattice (Fin 2) of SemilatticeSup (Fin 2) ▶
[] [0.000051s] ✅ apply @CanonicallyLinearOrderedAddCommMonoid.semilatticeSup to SemilatticeSup (Fin 2) ▶
[] [0.000058s] ✅ apply @CanonicallyLinearOrderedCommMonoid.semilatticeSup to SemilatticeSup (Fin 2) ▶
[] [0.000042s] ✅ apply @LinearOrder.toPartialOrder to PartialOrder (Fin 2) ▶
[resume] [0.000006s] propagating LinearOrder (Fin 2) to subgoal LinearOrder (Fin 2) of PartialOrder (Fin 2) ▶
[] [0.000072s] ✅ apply @SetLike.instPartialOrder to PartialOrder (Fin 2) ▶
[] [0.000058s] ✅ apply @Ring.toNonUnitalRing to NonUnitalRing (Fin 2) ▶
[resume] [0.000008s] propagating Ring (Fin 2) to subgoal Ring (Fin 2) of NonUnitalRing (Fin 2) ▶
[] [0.000059s] ✅ apply @NormedLatticeAddCommGroup.toOrderedAddCommGroup to OrderedAddCommGroup (Fin 2) ▶
[] [0.000050s] ✅ apply @Ring.toAddCommGroup to AddCommGroup (Fin 2) ▶
[resume] [0.000005s] propagating Ring (Fin 2) to subgoal Ring (Fin 2) of AddCommGroup (Fin 2) ▶
[] [0.000063s] ✅ apply @NonUnitalNonAssocRing.toAddCommGroup to AddCommGroup (Fin 2) ▶
[] [0.000371s] ❌ apply @DirectSum.GradeZero.nonUnitalNonAssocRing to NonUnitalNonAssocRing (Fin 2) ▶
[] [0.000072s] ✅ apply @NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing to NonUnitalNonAssocRing (Fin 2) ▶
[] [0.000052s] ✅ apply @NonUnitalCommRing.toNonUnitalNonAssocCommRing to NonUnitalNonAssocCommRing (Fin 2) ▶
[resume] [0.000009s] propagating NonUnitalCommRing
(Fin
2) to subgoal NonUnitalCommRing
(Fin
2) of NonUnitalNonAssocCommRing (Fin 2) ▶
[resume] [0.000005s] propagating NonUnitalNonAssocCommRing
(Fin
2) to subgoal NonUnitalNonAssocCommRing
(Fin 2) of NonUnitalNonAssocRing (Fin 2) ▶
[resume] [0.000006s] propagating NonUnitalNonAssocRing (Fin 2) to subgoal NonUnitalNonAssocRing (Fin 2) of AddCommGroup (Fin 2) ▶
[] [0.000048s] ✅ apply @NonAssocRing.toNonUnitalNonAssocRing to NonUnitalNonAssocRing (Fin 2) ▶
[resume] [0.000005s] propagating NonAssocRing (Fin 2) to subgoal NonAssocRing (Fin 2) of NonUnitalNonAssocRing (Fin 2) ▶
[] [0.000044s] ✅ apply @NonUnitalRing.toNonUnitalNonAssocRing to NonUnitalNonAssocRing (Fin 2) ▶
[resume] [0.000004s] propagating NonUnitalRing (Fin 2) to subgoal NonUnitalRing (Fin 2) of NonUnitalNonAssocRing (Fin 2) ▶
[] [0.000044s] ✅ apply @AddCommGroupWithOne.toAddCommGroup to AddCommGroup (Fin 2) ▶
[resume] [0.000005s] propagating AddCommGroupWithOne (Fin 2) to subgoal AddCommGroupWithOne (Fin 2) of AddCommGroup (Fin 2) ▶
[] [0.000077s] ✅ apply @IsSimpleGroup.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000061s] ✅ apply @NormedGroup.toGroup to Group (Fin 2) ▶
[] [0.000063s] ✅ apply @NormedCommGroup.toNormedGroup to NormedGroup (Fin 2) ▶
[] [0.000050s] ✅ apply @NormedOrderedGroup.toNormedCommGroup to NormedCommGroup (Fin 2) ▶
[] [0.000057s] ✅ apply @SeminormedGroup.toGroup to Group (Fin 2) ▶
[] [0.000057s] ✅ apply @SeminormedCommGroup.toSeminormedGroup to SeminormedGroup (Fin 2) ▶
[] [0.000047s] ✅ apply @NormedCommGroup.toSeminormedCommGroup to SeminormedCommGroup (Fin 2) ▶
[] [0.000049s] ✅ apply @NormedGroup.toSeminormedGroup to SeminormedGroup (Fin 2) ▶
[] 686 more entries... ▼
[] [0.000061s] ✅ apply @CommGroup.toGroup to Group (Fin 2) ▶
[] [0.000062s] ✅ apply @NormedCommGroup.toCommGroup to CommGroup (Fin 2) ▶
[] [0.000041s] ✅ apply @SeminormedCommGroup.toCommGroup to CommGroup (Fin 2) ▶
[] [0.000039s] ✅ apply @OrderedCommGroup.toCommGroup to CommGroup (Fin 2) ▶
[] [0.000067s] ✅ apply @IsSimpleOrder.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000060s] ✅ apply @instLEFin to LE (Fin 2) ▶
[resume] [0.000031s] propagating LE (Fin 2) to subgoal LE (Fin 2) of Nontrivial (Fin 2) ▶
[] [0.000247s] ✅ apply @Fin.instBoundedOrderFinHAddNatInstHAddInstAddNatOfNatInstLEFin to BoundedOrder (Fin 2) ▶
[resume] [0.000020s] propagating BoundedOrder (Fin (1 + 1)) to subgoal BoundedOrder (Fin 2) of Nontrivial (Fin 2) ▶
[] [0.001530s] ✅ apply NonemptyFiniteLinearOrder.toBoundedOrder to BoundedOrder (Fin 2) ▶
[resume] [0.000021s] propagating BoundedOrder (Fin 2) to subgoal BoundedOrder (Fin 2) of Nontrivial (Fin 2) ▶
[] [0.001466s] ✅ apply @CompleteLattice.toBoundedOrder to BoundedOrder (Fin 2) ▶
[resume] [0.000021s] propagating BoundedOrder (Fin 2) to subgoal BoundedOrder (Fin 2) of Nontrivial (Fin 2) ▶
[] [0.000769s] ❌ apply @BooleanAlgebra.toBoundedOrder to BoundedOrder (Fin 2) ▶
[] [0.000902s] ❌ apply @CoheytingAlgebra.toBoundedOrder to BoundedOrder (Fin 2) ▶
[] [0.000899s] ❌ apply @HeytingAlgebra.toBoundedOrder to BoundedOrder (Fin 2) ▶
[] [0.000076s] ✅ apply @Preorder.toLE to LE (Fin 2) ▶
[] [0.000048s] ✅ apply @PartialOrder.toPreorder to Preorder (Fin 2) ▶
[resume] [0.000008s] propagating PartialOrder (Fin 2) to subgoal PartialOrder (Fin 2) of Preorder (Fin 2) ▶
[resume] [0.000006s] propagating Preorder (Fin 2) to subgoal Preorder (Fin 2) of LE (Fin 2) ▶
[] [0.000049s] ✅ apply @EuclideanDomain.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000055s] ✅ apply @CanonicallyLinearOrderedSemifield.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000061s] ✅ apply @Field.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000047s] ✅ apply @Semifield.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000041s] ✅ apply @DivisionRing.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000042s] ✅ apply @DivisionSemiring.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000066s] ✅ apply @instNontrivial to Nontrivial (Fin 2) ▶
[] [0.000059s] ✅ apply Fin.instAddMonoidWithOne to AddMonoidWithOne (Fin 2) ▶
[resume] [0.000008s] propagating NeZero 2 to subgoal NeZero 2 of AddMonoidWithOne (Fin 2) ▶
[resume] [0.000032s] propagating AddMonoidWithOne (Fin 2) to subgoal AddMonoidWithOne (Fin 2) of Nontrivial (Fin 2) ▶
[resume] [0.000007s] propagating NeZero 2 to subgoal NeZero 2 of AddMonoidWithOne (Fin 2) ▶
[resume] [0.000006s] propagating NeZero 2 to subgoal NeZero 2 of AddMonoidWithOne (Fin 2) ▶
[resume] [0.000005s] propagating NeZero (1 + 1) to subgoal NeZero 2 of AddMonoidWithOne (Fin 2) ▶
[] [0.001045s] ❌ apply @NumberField.to_charZero to CharZero (Fin 2) ▶
[] [0.001371s] ❌ apply @RCLike.charZero_rclike to CharZero (Fin 2) ▶
[] [0.001862s] ❌ apply @StrictOrderedSemiring.to_charZero to CharZero (Fin 2) ▶
[] [0.000069s] ✅ apply @AddGroupWithOne.toAddMonoidWithOne to AddMonoidWithOne (Fin 2) ▶
[resume] [0.000008s] propagating AddGroupWithOne (Fin 2) to subgoal AddGroupWithOne (Fin 2) of AddMonoidWithOne (Fin 2) ▶
[] [0.000068s] ✅ apply @AddCommMonoidWithOne.toAddMonoidWithOne to AddMonoidWithOne (Fin 2) ▶
[] [0.000077s] ✅ apply @NonAssocSemiring.toAddCommMonoidWithOne to AddCommMonoidWithOne (Fin 2) ▶
[] [0.000052s] ✅ apply @Semiring.toNonAssocSemiring to NonAssocSemiring (Fin 2) ▶
[resume] [0.000007s] propagating Semiring (Fin 2) to subgoal Semiring (Fin 2) of NonAssocSemiring (Fin 2) ▶
[resume] [0.000005s] propagating NonAssocSemiring (Fin 2) to subgoal NonAssocSemiring (Fin 2) of AddCommMonoidWithOne (Fin 2) ▶
[resume] [0.000005s] propagating AddCommMonoidWithOne (Fin 2) to subgoal AddCommMonoidWithOne (Fin 2) of AddMonoidWithOne (Fin 2) ▶
[] [0.000046s] ✅ apply @NonAssocRing.toNonAssocSemiring to NonAssocSemiring (Fin 2) ▶
[resume] [0.000005s] propagating NonAssocRing (Fin 2) to subgoal NonAssocRing (Fin 2) of NonAssocSemiring (Fin 2) ▶
[] [0.000045s] ✅ apply @AddCommGroupWithOne.toAddCommMonoidWithOne to AddCommMonoidWithOne (Fin 2) ▶
[resume] [0.000005s] propagating AddCommGroupWithOne
(Fin
2) to subgoal AddCommGroupWithOne
(Fin 2) of AddCommMonoidWithOne (Fin 2) ▶
[] [0.000044s] ✅ apply @StrictOrderedRing.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000051s] ✅ apply @StrictOrderedSemiring.toNontrivial to Nontrivial (Fin 2) ▶
[] 636 more entries... ▼
[] [0.000043s] ✅ apply @LinearOrderedCommGroupWithZero.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000054s] ✅ apply @LinearOrderedAddCommGroupWithTop.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000045s] ✅ apply @IsDomain.toNontrivial to Nontrivial (Fin 2) ▶
[resume] [0.000005s] propagating Semiring (Fin 2) to subgoal Semiring (Fin 2) of Nontrivial (Fin 2) ▶
[] [0.000056s] ✅ apply @CommGroupWithZero.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000060s] ✅ apply @Semifield.toCommGroupWithZero to CommGroupWithZero (Fin 2) ▶
[] [0.000044s] ✅ apply @LinearOrderedCommGroupWithZero.toCommGroupWithZero to CommGroupWithZero (Fin 2) ▶
[] [0.000101s] ✅ apply @GroupWithZero.toNontrivial to Nontrivial (Fin 2) ▶
[] [0.000082s] ✅ apply @DivisionSemiring.toGroupWithZero to GroupWithZero (Fin 2) ▶
[] [0.000045s] ✅ apply @CommGroupWithZero.toGroupWithZero to GroupWithZero (Fin 2) ▶
[] [0.000061s] ✅ apply instNontrivial_1 to Nontrivial (Fin 2) ▶
[resume] [0.000032s] propagating Ring (Fin 2) to subgoal Ring (Fin 2) of Nontrivial (Fin 2) ▶
[] [0.003544s] ✅ apply @IsDomain.hasRankNullity to HasRankNullity.{?u.7096, 0} (Fin 2) ▶
[] [0.000287s] ✅ apply @IsDedekindDomain.toIsDomain to IsDomain (Fin 2) ▶
[] [0.000355s] ✅ apply instIsDedekindDomain to IsDedekindDomain (Fin 2) ▶
[] [0.000205s] ✅ apply IsPrincipalIdealRing.isDedekindDomain to IsDedekindDomain (Fin 2) ▶
[] [0.020643s] ❌ apply @Field.isDomain to IsDomain (Fin 2) ▶
[] [0.011801s] ❌ apply @DivisionRing.isDomain to IsDomain (Fin 2) ▶
[] [0.005463s] ❌ apply @LinearOrderedRing.isDomain to IsDomain (Fin 2) ▶
[] [0.024717s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain (Fin 2) ▶
[] [0.006845s] ❌ apply @DivisionRing.hasRankNullity to HasRankNullity.{?u.4667, 0} (Fin 2) ▶
[] [0.000141s] ✅ apply Infinite.instNontrivial to Nontrivial (Fin 2) ▶
[] [0.000068s] ✅ apply @IsAlgClosed.instInfinite to Infinite (Fin 2) ▶
[] [0.000053s] ✅ apply CharZero.infinite to Infinite (Fin 2) ▶
[resume] [0.000007s] propagating AddMonoidWithOne (Fin 2) to subgoal AddMonoidWithOne (Fin 2) of Infinite (Fin 2) ▶
[] [0.000069s] ✅ apply @Denumerable.instInfinite to Infinite (Fin 2) ▶
[] [0.000073s] ✅ apply @instInfinite to Infinite (Fin 2) ▶
[] [0.000050s] ✅ apply NontriviallyNormedField.infinite to Infinite (Fin 2) ▶
[] [0.000105s] ✅ apply @CategoryTheory.IsConnected.is_nonempty to Nonempty (Fin 2) ▶
[] [0.000102s] ✅ apply @CategoryTheory.Groupoid.toCategory to CategoryTheory.Category.{?u.7451, 0} (Fin 2) ▶
[] [0.000103s] ✅ apply CategoryTheory.StrictBicategory.category to CategoryTheory.Category.{?u.7449, 0} (Fin 2) ▶
[] [0.000071s] ✅ apply Preorder.smallCategory to CategoryTheory.Category.{0, 0} (Fin 2) ▶
[resume] [0.000013s] propagating Preorder (Fin 2) to subgoal Preorder (Fin 2) of CategoryTheory.Category.{0, 0} (Fin 2) ▶
[resume] [0.000023s] propagating CategoryTheory.SmallCategory
(Fin
2) to subgoal CategoryTheory.Category.{0,
0}
(Fin 2) of Nonempty (Fin 2) ▶
[] [0.000101s] ✅ apply @AddTorsor.nonempty to Nonempty (Fin 2) ▶
[] [0.000316s] ✅ apply @NormedAddTorsor.toAddTorsor to AddTorsor ?m.7473 (Fin 2) ▶
[] [0.000071s] ✅ apply @SeminormedRing.toPseudoMetricSpace to PseudoMetricSpace (Fin 2) ▶
[] [0.000055s] ✅ apply @NonUnitalSeminormedRing.toPseudoMetricSpace to PseudoMetricSpace (Fin 2) ▶
[] [0.000056s] ✅ apply @SeminormedCommGroup.toPseudoMetricSpace to PseudoMetricSpace (Fin 2) ▶
[] [0.000059s] ✅ apply @SeminormedAddCommGroup.toPseudoMetricSpace to PseudoMetricSpace (Fin 2) ▶
[] [0.000053s] ✅ apply @SeminormedGroup.toPseudoMetricSpace to PseudoMetricSpace (Fin 2) ▶
[] [0.000045s] ✅ apply @SeminormedAddGroup.toPseudoMetricSpace to PseudoMetricSpace (Fin 2) ▶
[] [0.000084s] ✅ apply @MetricSpace.toPseudoMetricSpace to PseudoMetricSpace (Fin 2) ▶
[] [0.000078s] ✅ apply @UpgradedPolishSpace.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000071s] ✅ apply @NormedLinearOrderedField.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000069s] ✅ apply @NormedLinearOrderedGroup.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000066s] ✅ apply @NormedLinearOrderedAddGroup.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000046s] ✅ apply @NormedOrderedGroup.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000045s] ✅ apply @NormedOrderedAddGroup.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000045s] ✅ apply @NormedField.toMetricSpace to MetricSpace (Fin 2) ▶
[] 586 more entries... ▼
[] [0.000047s] ✅ apply @NormedDivisionRing.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000047s] ✅ apply @NormedRing.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000051s] ✅ apply @NonUnitalNormedRing.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000044s] ✅ apply @NormedCommGroup.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000044s] ✅ apply @NormedAddCommGroup.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000046s] ✅ apply @NormedGroup.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000049s] ✅ apply @NormedAddGroup.toMetricSpace to MetricSpace (Fin 2) ▶
[] [0.000156s] ✅ apply addGroupIsAddTorsor to AddTorsor (Fin 2) (Fin 2) ▶
[resume] [0.000008s] propagating AddGroup (Fin 2) to subgoal AddGroup (Fin 2) of AddTorsor (Fin 2) (Fin 2) ▶
[resume] [0.000015s] propagating AddTorsor (Fin 2) (Fin 2) to subgoal AddTorsor (Fin 2) (Fin 2) of Nonempty (Fin 2) ▶
[] [0.000203s] ✅ apply @NormedAddTorsor.toAddTorsor' to AddTorsor ?m.7562 (Fin 2) ▶
[] [0.000089s] ✅ apply bot_nonempty to Nonempty (Fin 2) ▶
[] [0.000066s] ✅ apply @ConditionallyCompleteLinearOrderBot.toBot to Bot (Fin 2) ▶
[resume] [0.000008s] propagating ConditionallyCompleteLinearOrderBot
(Fin
2) to subgoal ConditionallyCompleteLinearOrderBot
(Fin 2) of Bot (Fin 2) ▶
[resume] [0.000005s] propagating Bot (Fin 2) to subgoal Bot (Fin 2) of Nonempty (Fin 2) ▶
[] [0.000052s] ✅ apply @CompleteLattice.toBot to Bot (Fin 2) ▶
[resume] [0.000006s] propagating CompleteLattice (Fin 2) to subgoal CompleteLattice (Fin 2) of Bot (Fin 2) ▶
[] [0.000048s] ✅ apply @BooleanAlgebra.toBot to Bot (Fin 2) ▶
[] [0.000046s] ✅ apply @GeneralizedBooleanAlgebra.toBot to Bot (Fin 2) ▶
[] [0.000052s] ✅ apply @OrderBot.toBot to Bot (Fin 2) ▶
[resume] [0.000042s] propagating LE (Fin 2) to subgoal LE (Fin 2) of Bot (Fin 2) ▶
[] [0.000787s] ❌ apply @HeytingAlgebra.toOrderBot to OrderBot (Fin 2) ▶
[] [0.000124s] ✅ apply @BoundedOrder.toOrderBot to OrderBot (Fin 2) ▶
[resume] [0.000010s] propagating BoundedOrder (Fin 2) to subgoal BoundedOrder (Fin 2) of OrderBot (Fin 2) ▶
[resume] [0.000014s] propagating OrderBot (Fin 2) to subgoal OrderBot (Fin 2) of Bot (Fin 2) ▶
[resume] [0.000008s] propagating BoundedOrder (Fin 2) to subgoal BoundedOrder (Fin 2) of OrderBot (Fin 2) ▶
[resume] [0.000006s] propagating BoundedOrder (Fin (1 + 1)) to subgoal BoundedOrder (Fin 2) of OrderBot (Fin 2) ▶
[] [0.000566s] ❌ apply @IdemSemiring.toOrderBot to OrderBot (Fin 2) ▶
[] [0.001371s] ✅ apply @ConditionallyCompleteLinearOrderBot.toOrderBot to OrderBot (Fin 2) ▶
[resume] [0.000007s] propagating OrderBot (Fin 2) to subgoal OrderBot (Fin 2) of Bot (Fin 2) ▶
[] [0.000481s] ❌ apply @CanonicallyOrderedCommMonoid.toOrderBot to OrderBot (Fin 2) ▶
[] [0.000861s] ❌ apply @CanonicallyOrderedAddCommMonoid.toOrderBot to OrderBot (Fin 2) ▶
[] [0.000878s] ❌ apply @GeneralizedBooleanAlgebra.toOrderBot to OrderBot (Fin 2) ▶
[] [0.000904s] ❌ apply @GeneralizedCoheytingAlgebra.toOrderBot to OrderBot (Fin 2) ▶
[] [0.000090s] ✅ apply top_nonempty to Nonempty (Fin 2) ▶
[] [0.000067s] ✅ apply @CompleteLattice.toTop to Top (Fin 2) ▶
[resume] [0.000008s] propagating CompleteLattice (Fin 2) to subgoal CompleteLattice (Fin 2) of Top (Fin 2) ▶
[resume] [0.000006s] propagating Top (Fin 2) to subgoal Top (Fin 2) of Nonempty (Fin 2) ▶
[] [0.000053s] ✅ apply @BooleanAlgebra.toTop to Top (Fin 2) ▶
[] [0.000053s] ✅ apply @OrderTop.toTop to Top (Fin 2) ▶
[resume] [0.000027s] propagating LE (Fin 2) to subgoal LE (Fin 2) of Top (Fin 2) ▶
[] [0.000552s] ❌ apply @LinearOrderedAddCommMonoidWithTop.toOrderTop to OrderTop (Fin 2) ▶
[] [0.000495s] ❌ apply @CoheytingAlgebra.toOrderTop to OrderTop (Fin 2) ▶
[] [0.000101s] ✅ apply @BoundedOrder.toOrderTop to OrderTop (Fin 2) ▶
[resume] [0.000009s] propagating BoundedOrder (Fin 2) to subgoal BoundedOrder (Fin 2) of OrderTop (Fin 2) ▶
[resume] [0.000006s] propagating OrderTop (Fin 2) to subgoal OrderTop (Fin 2) of Top (Fin 2) ▶
[resume] [0.000006s] propagating BoundedOrder (Fin 2) to subgoal BoundedOrder (Fin 2) of OrderTop (Fin 2) ▶
[resume] [0.000005s] propagating BoundedOrder (Fin (1 + 1)) to subgoal BoundedOrder (Fin 2) of OrderTop (Fin 2) ▶
[] [0.000803s] ❌ apply @GeneralizedHeytingAlgebra.toOrderTop to OrderTop (Fin 2) ▶
[] [0.000095s] ✅ apply @ConnectedSpace.toNonempty to Nonempty (Fin 2) ▶
[] 536 more entries... ▼
[] [0.000072s] ✅ apply @instTopologicalSpaceFin to TopologicalSpace (Fin 2) ▶
[resume] [0.000032s] propagating TopologicalSpace (Fin 2) to subgoal TopologicalSpace (Fin 2) of Nonempty (Fin 2) ▶
[] [0.000123s] ✅ apply @PathConnectedSpace.connectedSpace to ConnectedSpace (Fin 2) ▶
[] [0.000113s] ✅ apply @SimplyConnectedSpace.instPathConnectedSpace to PathConnectedSpace (Fin 2) ▶
[] [0.000104s] ✅ apply SimplyConnectedSpace.ofContractible to SimplyConnectedSpace (Fin 2) ▶
[] [0.000126s] ✅ apply @ContractibleSpace.instContractibleSpace to ContractibleSpace (Fin 2) ▶
[] [0.000123s] ✅ apply @RealTopologicalVectorSpace.contractibleSpace to ContractibleSpace (Fin 2) ▶
[resume] [0.000046s] propagating AddCommGroup (Fin 2) to subgoal AddCommGroup (Fin 2) of ContractibleSpace (Fin 2) ▶
[] [0.015572s] ❌ apply @NormedSpace.toModule to Module ℝ (Fin 2) ▶
[] [0.004780s] ✅ apply @LieAlgebra.toModule to Module ℝ (Fin 2) ▶
[] [0.000246s] ✅ apply @LieAlgebra.ofAssociativeAlgebra to LieAlgebra ℝ (Fin 2) ▶
[] [0.000256s] ✅ apply @Bialgebra.toAlgebra to Algebra ℝ (Fin 2) ▶
[] [0.000183s] ✅ apply @HopfAlgebra.toBialgebra to Bialgebra ℝ (Fin 2) ▶
[] [0.000081s] ❌ apply CommSemiring.toHopfAlgebra to HopfAlgebra ℝ (Fin 2) ▶
[] [0.000068s] ❌ apply CommSemiring.toBialgebra to Bialgebra ℝ (Fin 2) ▶
[] [0.011814s] ❌ apply @NormedAlgebra.toAlgebra to Algebra ℝ (Fin 2) ▶
[] [0.000090s] ❌ apply Algebra.id to Algebra ℝ (Fin 2) ▶
[] [0.000215s] ✅ apply @Algebra.complexToReal to Algebra ℝ (Fin 2) ▶
[] [0.000164s] ✅ apply @Bialgebra.toAlgebra to Algebra ℂ (Fin 2) ▶
[] [0.000156s] ✅ apply @HopfAlgebra.toBialgebra to Bialgebra ℂ (Fin 2) ▶
[] [0.000080s] ❌ apply CommSemiring.toHopfAlgebra to HopfAlgebra ℂ (Fin 2) ▶
[] [0.000063s] ❌ apply CommSemiring.toBialgebra to Bialgebra ℂ (Fin 2) ▶
[] [0.011176s] ❌ apply @NormedAlgebra.toAlgebra to Algebra ℂ (Fin 2) ▶
[] [0.000098s] ❌ apply Algebra.id to Algebra ℂ (Fin 2) ▶
[] [0.000127s] ❌ apply @DirectSum.GradeZero.module to Module ℝ (Fin 2) ▶
[] [0.000066s] ❌ apply @Semiring.toModule to Module ℝ (Fin 2) ▶
[] [0.000164s] ✅ apply Module.complexToReal to Module ℝ (Fin 2) ▶
[] [0.013198s] ❌ apply @NormedSpace.toModule to Module ℂ (Fin 2) ▶
[] [0.000868s] ✅ apply @LieAlgebra.toModule to Module ℂ (Fin 2) ▶
[] [0.000189s] ✅ apply @LieAlgebra.ofAssociativeAlgebra to LieAlgebra ℂ (Fin 2) ▶
[] [0.000153s] ✅ apply @Bialgebra.toAlgebra to Algebra ℂ (Fin 2) ▶
[] [0.000150s] ✅ apply @HopfAlgebra.toBialgebra to Bialgebra ℂ (Fin 2) ▶
[] [0.000069s] ❌ apply CommSemiring.toHopfAlgebra to HopfAlgebra ℂ (Fin 2) ▶
[] [0.000060s] ❌ apply CommSemiring.toBialgebra to Bialgebra ℂ (Fin 2) ▶
[] [0.011170s] ❌ apply @NormedAlgebra.toAlgebra to Algebra ℂ (Fin 2) ▶
[] [0.000095s] ❌ apply Algebra.id to Algebra ℂ (Fin 2) ▶
[] [0.000092s] ❌ apply @DirectSum.GradeZero.module to Module ℂ (Fin 2) ▶
[] [0.000068s] ❌ apply @Semiring.toModule to Module ℂ (Fin 2) ▶
[] [0.006091s] ✅ apply @Algebra.toModule to Module ℂ (Fin 2) ▶
[] [0.000149s] ✅ apply @Bialgebra.toAlgebra to Algebra ℂ (Fin 2) ▶
[] [0.000141s] ✅ apply @HopfAlgebra.toBialgebra to Bialgebra ℂ (Fin 2) ▶
[] [0.000070s] ❌ apply CommSemiring.toHopfAlgebra to HopfAlgebra ℂ (Fin 2) ▶
[] [0.000061s] ❌ apply CommSemiring.toBialgebra to Bialgebra ℂ (Fin 2) ▶
[] [0.010745s] ❌ apply @NormedAlgebra.toAlgebra to Algebra ℂ (Fin 2) ▶
[] [0.000092s] ❌ apply Algebra.id to Algebra ℂ (Fin 2) ▶
[] [0.014845s] ❌ apply @NormedSpace.toModule' to Module ℂ (Fin 2) ▶
[] [0.000787s] ✅ apply @Algebra.toModule to Module ℝ (Fin 2) ▶
[] [0.000177s] ✅ apply @Bialgebra.toAlgebra to Algebra ℝ (Fin 2) ▶
[] [0.000139s] ✅ apply @HopfAlgebra.toBialgebra to Bialgebra ℝ (Fin 2) ▶
[] [0.000109s] ❌ apply CommSemiring.toHopfAlgebra to HopfAlgebra ℝ (Fin 2) ▶
[] 486 more entries... ▼
[] [0.000061s] ❌ apply CommSemiring.toBialgebra to Bialgebra ℝ (Fin 2) ▶
[] [0.012791s] ❌ apply @NormedAlgebra.toAlgebra to Algebra ℝ (Fin 2) ▶
[] [0.000105s] ❌ apply Algebra.id to Algebra ℝ (Fin 2) ▶
[] [0.000111s] ✅ apply @Algebra.complexToReal to Algebra ℝ (Fin 2) ▶
[] [0.013311s] ❌ apply @NormedSpace.toModule' to Module ℝ (Fin 2) ▶
[] [0.000120s] ✅ apply @ContractibleSpace.instPathConnectedSpace to PathConnectedSpace (Fin 2) ▶
[] [0.001887s] ❌ apply @NormedSpace.instPathConnectedSpace to PathConnectedSpace (Fin 2) ▶
[] [0.000117s] ✅ apply IrreducibleSpace.connectedSpace to ConnectedSpace (Fin 2) ▶
[] [0.000063s] ✅ apply @AlexandrovDiscreteSpace.toTopologicalSpace to TopologicalSpace (Fin 2) ▶
[] [0.000073s] ✅ apply Scott.topologicalSpace to TopologicalSpace (Fin 2) ▶
[resume] [0.000008s] propagating OmegaCompletePartialOrder
(Fin
2) to subgoal OmegaCompletePartialOrder
(Fin
2) of TopologicalSpace (Fin 2) ▶
[resume] [0.000022s] propagating TopologicalSpace (Scott (Fin 2)) to subgoal TopologicalSpace (Fin 2) of Nonempty (Fin 2) ▶
[] [0.000101s] ✅ apply @PathConnectedSpace.connectedSpace to ConnectedSpace (Fin 2) ▶
[] [0.000100s] ✅ apply @SimplyConnectedSpace.instPathConnectedSpace to PathConnectedSpace (Fin 2) ▶
[] [0.000086s] ✅ apply SimplyConnectedSpace.ofContractible to SimplyConnectedSpace (Fin 2) ▶
[] [0.000090s] ✅ apply @ContractibleSpace.instContractibleSpace to ContractibleSpace (Fin 2) ▶
[] [0.000112s] ✅ apply @RealTopologicalVectorSpace.contractibleSpace to ContractibleSpace (Fin 2) ▶
[resume] [0.000006s] propagating AddCommGroup (Fin 2) to subgoal AddCommGroup (Fin 2) of ContractibleSpace (Fin 2) ▶
[] [0.000067s] ✅ apply @ContractibleSpace.instPathConnectedSpace to PathConnectedSpace (Fin 2) ▶
[] [0.000404s] ❌ apply @NormedSpace.instPathConnectedSpace to PathConnectedSpace (Fin 2) ▶
[] [0.000103s] ✅ apply IrreducibleSpace.connectedSpace to ConnectedSpace (Fin 2) ▶
[] [0.000067s] ✅ apply @UpgradedStandardBorel.toTopologicalSpace to TopologicalSpace (Fin 2) ▶
[] [0.000079s] ✅ apply @UniformSpace.toTopologicalSpace to TopologicalSpace (Fin 2) ▶
[] [0.000125s] ✅ apply @Valued.toUniformSpace to UniformSpace (Fin 2) ▶
[resume] [0.000025s] propagating Ring (Fin 2) to subgoal Ring (Fin 2) of UniformSpace (Fin 2) ▶
[] [0.000045s] ✅ apply @PseudoMetricSpace.toUniformSpace to UniformSpace (Fin 2) ▶
[] [0.000063s] ✅ apply @PseudoEMetricSpace.toUniformSpace to UniformSpace (Fin 2) ▶
[] [0.000078s] ✅ apply @EMetricSpace.toPseudoEMetricSpace to PseudoEMetricSpace (Fin 2) ▶
[] [0.000071s] ✅ apply @MetricSpace.toEMetricSpace to EMetricSpace (Fin 2) ▶
[] [0.000045s] ✅ apply @PseudoMetricSpace.toPseudoEMetricSpace to PseudoEMetricSpace (Fin 2) ▶
[] [0.000054s] ✅ apply WithIdeal.instUniformSpace to UniformSpace (Fin 2) ▶
[resume] [0.000017s] propagating CommRing (Fin 2) to subgoal CommRing (Fin 2) of UniformSpace (Fin 2) ▶
[] [0.000053s] ✅ apply WithIdeal.instTopologicalSpace to TopologicalSpace (Fin 2) ▶
[resume] [0.000010s] propagating CommRing (Fin 2) to subgoal CommRing (Fin 2) of TopologicalSpace (Fin 2) ▶
[] [0.000051s] ✅ apply @IrreducibleSpace.toNonempty to Nonempty (Fin 2) ▶
[resume] [0.000013s] propagating TopologicalSpace (Scott (Fin 2)) to subgoal TopologicalSpace (Fin 2) of Nonempty (Fin 2) ▶
[resume] [0.000010s] propagating TopologicalSpace (Fin 2) to subgoal TopologicalSpace (Fin 2) of Nonempty (Fin 2) ▶
[] [0.000085s] ✅ apply supSet_to_nonempty to Nonempty (Fin 2) ▶
[] [0.000067s] ✅ apply @CompletePartialOrder.toSupSet to SupSet (Fin 2) ▶
[resume] [0.000008s] propagating CompletePartialOrder (Fin 2) to subgoal CompletePartialOrder (Fin 2) of SupSet (Fin 2) ▶
[resume] [0.000005s] propagating SupSet (Fin 2) to subgoal SupSet (Fin 2) of Nonempty (Fin 2) ▶
[] [0.000059s] ✅ apply @ConditionallyCompleteLinearOrderedField.toSupSet to SupSet (Fin 2) ▶
[] [0.000047s] ✅ apply @ConditionallyCompleteLattice.toSupSet to SupSet (Fin 2) ▶
[resume] [0.000006s] propagating ConditionallyCompleteLattice
(Fin
2) to subgoal ConditionallyCompleteLattice
(Fin 2) of SupSet (Fin 2) ▶
[] [0.000050s] ✅ apply @CompleteBooleanAlgebra.toSupSet to SupSet (Fin 2) ▶
[] [0.000048s] ✅ apply @CompleteLattice.toSupSet to SupSet (Fin 2) ▶
[resume] [0.000006s] propagating CompleteLattice (Fin 2) to subgoal CompleteLattice (Fin 2) of SupSet (Fin 2) ▶
[] [0.000046s] ✅ apply @CompleteSemilatticeSup.toSupSet to SupSet (Fin 2) ▶
[resume] [0.000005s] propagating CompleteSemilatticeSup (Fin 2) to subgoal CompleteSemilatticeSup (Fin 2) of SupSet (Fin 2) ▶
[] [0.000067s] ✅ apply infSet_to_nonempty to Nonempty (Fin 2) ▶
[] 436 more entries... ▼
[] [0.000077s] ✅ apply @ConditionallyCompleteLinearOrderedField.toInfSet to InfSet (Fin 2) ▶
[] [0.000045s] ✅ apply @ConditionallyCompleteLattice.toInfSet to InfSet (Fin 2) ▶
[resume] [0.000006s] propagating ConditionallyCompleteLattice
(Fin
2) to subgoal ConditionallyCompleteLattice
(Fin 2) of InfSet (Fin 2) ▶
[resume] [0.000005s] propagating InfSet (Fin 2) to subgoal InfSet (Fin 2) of Nonempty (Fin 2) ▶
[] [0.000046s] ✅ apply @CompleteBooleanAlgebra.toInfSet to InfSet (Fin 2) ▶
[] [0.000055s] ✅ apply @CompleteLattice.toInfSet to InfSet (Fin 2) ▶
[resume] [0.000005s] propagating CompleteLattice (Fin 2) to subgoal CompleteLattice (Fin 2) of InfSet (Fin 2) ▶
[] [0.000045s] ✅ apply @CompleteSemilatticeInf.toInfSet to InfSet (Fin 2) ▶
[resume] [0.000005s] propagating CompleteSemilatticeInf (Fin 2) to subgoal CompleteSemilatticeInf (Fin 2) of InfSet (Fin 2) ▶
[] [0.000073s] ✅ apply @One.instNonempty to Nonempty (Fin 2) ▶
[] [0.000067s] ✅ apply @Fin.instOneFin to One (Fin 2) ▶
[resume] [0.000007s] propagating NeZero 2 to subgoal NeZero 2 of One (Fin 2) ▶
[resume] [0.000004s] propagating One (Fin 2) to subgoal One (Fin 2) of Nonempty (Fin 2) ▶
[resume] [0.000007s] propagating NeZero 2 to subgoal NeZero 2 of One (Fin 2) ▶
[resume] [0.000006s] propagating NeZero 2 to subgoal NeZero 2 of One (Fin 2) ▶
[resume] [0.000005s] propagating NeZero (1 + 1) to subgoal NeZero 2 of One (Fin 2) ▶
[] [0.000066s] ✅ apply @UnitalShelf.toOne to One (Fin 2) ▶
[] [0.000713s] ❌ apply @GradedMonoid.GradeZero.one to One (Fin 2) ▶
[] [0.000056s] ✅ apply @CanonicallyOrderedCommSemiring.toOne to One (Fin 2) ▶
[] [0.000043s] ✅ apply @Semiring.toOne to One (Fin 2) ▶
[resume] [0.000008s] propagating Semiring (Fin 2) to subgoal Semiring (Fin 2) of One (Fin 2) ▶
[] [0.000056s] ✅ apply @NonAssocRing.toOne to One (Fin 2) ▶
[resume] [0.000006s] propagating NonAssocRing (Fin 2) to subgoal NonAssocRing (Fin 2) of One (Fin 2) ▶
[] [0.000043s] ✅ apply @NonAssocSemiring.toOne to One (Fin 2) ▶
[resume] [0.000013s] propagating NonAssocSemiring (Fin 2) to subgoal NonAssocSemiring (Fin 2) of One (Fin 2) ▶
[] [0.000041s] ✅ apply @AddCommGroupWithOne.toOne to One (Fin 2) ▶
[resume] [0.000005s] propagating AddCommGroupWithOne (Fin 2) to subgoal AddCommGroupWithOne (Fin 2) of One (Fin 2) ▶
[] [0.000045s] ✅ apply @AddMonoidWithOne.toOne to One (Fin 2) ▶
[resume] [0.000005s] propagating AddMonoidWithOne (Fin 2) to subgoal AddMonoidWithOne (Fin 2) of One (Fin 2) ▶
[] [0.000060s] ✅ apply @InvOneClass.toOne to One (Fin 2) ▶
[] [0.000065s] ✅ apply @DivInvOneMonoid.toInvOneClass to InvOneClass (Fin 2) ▶
[] [0.000061s] ✅ apply @DivisionMonoid.toDivInvOneMonoid to DivInvOneMonoid (Fin 2) ▶
[] [0.000061s] ✅ apply @DivisionCommMonoid.toDivisionMonoid to DivisionMonoid (Fin 2) ▶
[] [0.000048s] ✅ apply @CommGroupWithZero.toDivisionCommMonoid to DivisionCommMonoid (Fin 2) ▶
[] [0.000044s] ✅ apply @CommGroup.toDivisionCommMonoid to DivisionCommMonoid (Fin 2) ▶
[] [0.000048s] ✅ apply @GroupWithZero.toDivisionMonoid to DivisionMonoid (Fin 2) ▶
[] [0.000045s] ✅ apply @Group.toDivisionMonoid to DivisionMonoid (Fin 2) ▶
[] [0.000052s] ✅ apply @RightCancelMonoid.toOne to One (Fin 2) ▶
[] [0.000072s] ✅ apply @CancelMonoid.toRightCancelMonoid to RightCancelMonoid (Fin 2) ▶
[] [0.000047s] ✅ apply @Group.toCancelMonoid to CancelMonoid (Fin 2) ▶
[] [0.000053s] ✅ apply CancelCommMonoid.toCancelMonoid to CancelMonoid (Fin 2) ▶
[] [0.000042s] ✅ apply @OrderedCancelCommMonoid.toCancelCommMonoid to CancelCommMonoid (Fin 2) ▶
[] [0.000040s] ✅ apply @CommGroup.toCancelCommMonoid to CancelCommMonoid (Fin 2) ▶
[] [0.000051s] ✅ apply @LeftCancelMonoid.toOne to One (Fin 2) ▶
[] [0.000047s] ✅ apply @CancelCommMonoid.toLeftCancelMonoid to LeftCancelMonoid (Fin 2) ▶
[] [0.000043s] ✅ apply @CancelMonoid.toLeftCancelMonoid to LeftCancelMonoid (Fin 2) ▶
[] [0.000064s] ✅ apply @Monoid.toOne to One (Fin 2) ▶
[] [0.000384s] ❌ apply @GradedMonoid.GradeZero.monoid to Monoid (Fin 2) ▶
[] [0.000072s] ✅ apply @MonoidWithZero.toMonoid to Monoid (Fin 2) ▶
[] [0.000049s] ✅ apply @Semiring.toMonoidWithZero to MonoidWithZero (Fin 2) ▶
[] 386 more entries... ▼
[resume] [0.000008s] propagating Semiring (Fin 2) to subgoal Semiring (Fin 2) of MonoidWithZero (Fin 2) ▶
[resume] [0.000006s] propagating MonoidWithZero (Fin 2) to subgoal MonoidWithZero (Fin 2) of Monoid (Fin 2) ▶
[resume] [0.000005s] propagating Monoid (Fin 2) to subgoal Monoid (Fin 2) of One (Fin 2) ▶
[] [0.000047s] ✅ apply @GroupWithZero.toMonoidWithZero to MonoidWithZero (Fin 2) ▶
[] [0.000057s] ✅ apply @CommMonoidWithZero.toMonoidWithZero to MonoidWithZero (Fin 2) ▶
[] [0.000049s] ✅ apply @LinearOrderedCommMonoidWithZero.toCommMonoidWithZero to CommMonoidWithZero (Fin 2) ▶
[] [0.000041s] ✅ apply @CommGroupWithZero.toCommMonoidWithZero to CommMonoidWithZero (Fin 2) ▶
[] [0.000040s] ✅ apply @CommSemiring.toCommMonoidWithZero to CommMonoidWithZero (Fin 2) ▶
[resume] [0.000006s] propagating CommSemiring (Fin 2) to subgoal CommSemiring (Fin 2) of CommMonoidWithZero (Fin 2) ▶
[resume] [0.000005s] propagating CommMonoidWithZero (Fin 2) to subgoal CommMonoidWithZero (Fin 2) of MonoidWithZero (Fin 2) ▶
[] [0.000058s] ✅ apply @CancelCommMonoidWithZero.toCommMonoidWithZero to CommMonoidWithZero (Fin 2) ▶
[] [0.000053s] ✅ apply @IsDomain.toCancelCommMonoidWithZero to CancelCommMonoidWithZero (Fin 2) ▶
[resume] [0.000005s] propagating CommSemiring (Fin 2) to subgoal CommSemiring (Fin 2) of CancelCommMonoidWithZero (Fin 2) ▶
[] [0.000045s] ✅ apply @CommGroupWithZero.toCancelCommMonoidWithZero to CancelCommMonoidWithZero (Fin 2) ▶
[] [0.000061s] ✅ apply @CancelMonoidWithZero.toMonoidWithZero to MonoidWithZero (Fin 2) ▶
[] [0.000057s] ✅ apply @IsDomain.toCancelMonoidWithZero to CancelMonoidWithZero (Fin 2) ▶
[resume] [0.000004s] propagating Semiring (Fin 2) to subgoal Semiring (Fin 2) of CancelMonoidWithZero (Fin 2) ▶
[] [0.000044s] ✅ apply @CancelCommMonoidWithZero.toCancelMonoidWithZero to CancelMonoidWithZero (Fin 2) ▶
[] [0.000039s] ✅ apply @GroupWithZero.toCancelMonoidWithZero to CancelMonoidWithZero (Fin 2) ▶
[] [0.000054s] ✅ apply @DivInvMonoid.toMonoid to Monoid (Fin 2) ▶
[] [0.000050s] ✅ apply @DivisionRing.toDivInvMonoid to DivInvMonoid (Fin 2) ▶
[] [0.000044s] ✅ apply @GroupWithZero.toDivInvMonoid to DivInvMonoid (Fin 2) ▶
[] [0.000043s] ✅ apply @Group.toDivInvMonoid to DivInvMonoid (Fin 2) ▶
[] [0.000040s] ✅ apply @DivisionMonoid.toDivInvMonoid to DivInvMonoid (Fin 2) ▶
[] [0.000047s] ✅ apply @DivInvOneMonoid.toDivInvMonoid to DivInvMonoid (Fin 2) ▶
[] [0.000069s] ✅ apply @CommMonoid.toMonoid to Monoid (Fin 2) ▶
[] [0.000460s] ❌ apply @GradedMonoid.GradeZero.commMonoid to CommMonoid (Fin 2) ▶
[] [0.000061s] ✅ apply @LinearOrderedCommRing.toCommMonoid to CommMonoid (Fin 2) ▶
[] [0.000045s] ✅ apply @OrderedCommMonoid.toCommMonoid to CommMonoid (Fin 2) ▶
[] [0.000047s] ✅ apply @CommRing.toCommMonoid to CommMonoid (Fin 2) ▶
[resume] [0.000008s] propagating CommRing (Fin 2) to subgoal CommRing (Fin 2) of CommMonoid (Fin 2) ▶
[resume] [0.000005s] propagating CommMonoid (Fin 2) to subgoal CommMonoid (Fin 2) of Monoid (Fin 2) ▶
[] [0.000051s] ✅ apply @CommSemiring.toCommMonoid to CommMonoid (Fin 2) ▶
[resume] [0.000005s] propagating CommSemiring (Fin 2) to subgoal CommSemiring (Fin 2) of CommMonoid (Fin 2) ▶
[] [0.000041s] ✅ apply @CommMonoidWithZero.toCommMonoid to CommMonoid (Fin 2) ▶
[resume] [0.000004s] propagating CommMonoidWithZero (Fin 2) to subgoal CommMonoidWithZero (Fin 2) of CommMonoid (Fin 2) ▶
[] [0.000045s] ✅ apply @CommGroup.toCommMonoid to CommMonoid (Fin 2) ▶
[] [0.000045s] ✅ apply @DivisionCommMonoid.toCommMonoid to CommMonoid (Fin 2) ▶
[] [0.000049s] ✅ apply @CancelCommMonoid.toCommMonoid to CommMonoid (Fin 2) ▶
[] [0.000043s] ✅ apply @RightCancelMonoid.toMonoid to Monoid (Fin 2) ▶
[] [0.000041s] ✅ apply @LeftCancelMonoid.toMonoid to Monoid (Fin 2) ▶
[] [0.000067s] ✅ apply @MulOneClass.toOne to One (Fin 2) ▶
[] [0.000064s] ✅ apply @MulZeroOneClass.toMulOneClass to MulOneClass (Fin 2) ▶
[] [0.000046s] ✅ apply @NonAssocSemiring.toMulZeroOneClass to MulZeroOneClass (Fin 2) ▶
[resume] [0.000007s] propagating NonAssocSemiring (Fin 2) to subgoal NonAssocSemiring (Fin 2) of MulZeroOneClass (Fin 2) ▶
[resume] [0.000005s] propagating MulZeroOneClass (Fin 2) to subgoal MulZeroOneClass (Fin 2) of MulOneClass (Fin 2) ▶
[resume] [0.000005s] propagating MulOneClass (Fin 2) to subgoal MulOneClass (Fin 2) of One (Fin 2) ▶
[] [0.000045s] ✅ apply @MonoidWithZero.toMulZeroOneClass to MulZeroOneClass (Fin 2) ▶
[resume] [0.000005s] propagating MonoidWithZero (Fin 2) to subgoal MonoidWithZero (Fin 2) of MulZeroOneClass (Fin 2) ▶
[] [0.000045s] ✅ apply @Monoid.toMulOneClass to MulOneClass (Fin 2) ▶
[] 336 more entries... ▼
[resume] [0.000005s] propagating Monoid (Fin 2) to subgoal Monoid (Fin 2) of MulOneClass (Fin 2) ▶
[] [0.000065s] ✅ apply @One.ofOfNat1 to One (Fin 2) ▶
[] [0.000082s] ✅ apply @Fin.instOfNatFin to OfNat (Fin 2) 1 ▶
[resume] [0.000007s] propagating NeZero 2 to subgoal NeZero 2 of OfNat (Fin 2) 1 ▶
[resume] [0.000006s] propagating OfNat (Fin 2) 1 to subgoal OfNat (Fin 2) 1 of One (Fin 2) ▶
[resume] [0.000006s] propagating NeZero 2 to subgoal NeZero 2 of OfNat (Fin 2) 1 ▶
[resume] [0.000007s] propagating NeZero 2 to subgoal NeZero 2 of OfNat (Fin 2) 1 ▶
[resume] [0.000007s] propagating NeZero (1 + 1) to subgoal NeZero 2 of OfNat (Fin 2) 1 ▶
[] [0.000147s] ✅ apply @Fin.instOfNat to OfNat (Fin 2) 1 ▶
[resume] [0.000006s] propagating OfNat (Fin (1 + 1)) 1 to subgoal OfNat (Fin 2) 1 of One (Fin 2) ▶
[] [0.000054s] ✅ apply @One.toOfNat1 to OfNat (Fin 2) 1 ▶
[resume] [0.000005s] propagating One (Fin 2) to subgoal One (Fin 2) of OfNat (Fin 2) 1 ▶
[] [0.000094s] ✅ apply @instOfNatAtLeastTwo to OfNat (Fin 2) 1 ▶
[] [0.000381s] ❌ apply @DirectSum.instNatCastOfNatToOfNat0ToZero to NatCast (Fin 2) ▶
[] [0.000057s] ✅ apply @CanonicallyOrderedCommSemiring.toNatCast to NatCast (Fin 2) ▶
[] [0.000046s] ✅ apply @Semiring.toNatCast to NatCast (Fin 2) ▶
[resume] [0.000008s] propagating Semiring (Fin 2) to subgoal Semiring (Fin 2) of NatCast (Fin 2) ▶
[resume] [0.000003s] propagating NatCast (Fin 2) to subgoal NatCast (Fin 2) of OfNat (Fin 2) 1 ▶
[] [0.000053s] ✅ apply @NonAssocRing.toNatCast to NatCast (Fin 2) ▶
[resume] [0.000006s] propagating NonAssocRing (Fin 2) to subgoal NonAssocRing (Fin 2) of NatCast (Fin 2) ▶
[] [0.000041s] ✅ apply @NonAssocSemiring.toNatCast to NatCast (Fin 2) ▶
[resume] [0.000004s] propagating NonAssocSemiring (Fin 2) to subgoal NonAssocSemiring (Fin 2) of NatCast (Fin 2) ▶
[] [0.000040s] ✅ apply @AddCommGroupWithOne.toNatCast to NatCast (Fin 2) ▶
[resume] [0.000005s] propagating AddCommGroupWithOne (Fin 2) to subgoal AddCommGroupWithOne (Fin 2) of NatCast (Fin 2) ▶
[] [0.000044s] ✅ apply @AddMonoidWithOne.toNatCast to NatCast (Fin 2) ▶
[resume] [0.000005s] propagating AddMonoidWithOne (Fin 2) to subgoal AddMonoidWithOne (Fin 2) of NatCast (Fin 2) ▶
[] [0.000081s] ✅ apply @Zero.instNonempty to Nonempty (Fin 2) ▶
[] [0.000074s] ✅ apply @MulZeroClass.toZero to Zero (Fin 2) ▶
[] [0.000076s] ✅ apply @NonUnitalNonAssocSemiring.toMulZeroClass to MulZeroClass (Fin 2) ▶
[] [0.000320s] ❌ apply @DirectSum.GradeZero.nonUnitalNonAssocSemiring to NonUnitalNonAssocSemiring (Fin 2) ▶
[] [0.000071s] ✅ apply @NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring to NonUnitalNonAssocSemiring (Fin 2) ▶
[] [0.000058s] ✅ apply @NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring to NonUnitalNonAssocCommSemiring (Fin 2) ▶
[resume] [0.000008s] propagating NonUnitalNonAssocCommRing
(Fin
2) to subgoal NonUnitalNonAssocCommRing
(Fin
2) of NonUnitalNonAssocCommSemiring
(Fin 2) ▶
[resume] [0.000005s] propagating NonUnitalNonAssocCommSemiring
(Fin
2) to subgoal NonUnitalNonAssocCommSemiring
(Fin
2) of NonUnitalNonAssocSemiring
(Fin 2) ▶
[resume] [0.000006s] propagating NonUnitalNonAssocSemiring
(Fin
2) to subgoal NonUnitalNonAssocSemiring
(Fin
2) of MulZeroClass
(Fin 2) ▶
[resume] [0.000005s] propagating MulZeroClass (Fin 2) to subgoal MulZeroClass (Fin 2) of Zero (Fin 2) ▶
[resume] [0.000005s] propagating Zero (Fin 2) to subgoal Zero (Fin 2) of Nonempty (Fin 2) ▶
[] [0.000052s] ✅ apply @NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring to NonUnitalNonAssocSemiring (Fin 2) ▶
[resume] [0.000006s] propagating NonUnitalNonAssocRing
(Fin
2) to subgoal NonUnitalNonAssocRing
(Fin
2) of NonUnitalNonAssocSemiring
(Fin 2) ▶
[] [0.000044s] ✅ apply @NonAssocSemiring.toNonUnitalNonAssocSemiring to NonUnitalNonAssocSemiring (Fin 2) ▶
[resume] [0.000005s] propagating NonAssocSemiring
(Fin
2) to subgoal NonAssocSemiring
(Fin
2) of NonUnitalNonAssocSemiring
(Fin 2) ▶
[] [0.000041s] ✅ apply @NonUnitalSemiring.toNonUnitalNonAssocSemiring to NonUnitalNonAssocSemiring (Fin 2) ▶
[resume] [0.000004s] propagating NonUnitalSemiring
(Fin
2) to subgoal NonUnitalSemiring
(Fin
2) of NonUnitalNonAssocSemiring
(Fin 2) ▶
[] [0.000046s] ✅ apply @MulZeroOneClass.toMulZeroClass to MulZeroClass (Fin 2) ▶
[resume] [0.000012s] propagating MulZeroOneClass (Fin 2) to subgoal MulZeroOneClass (Fin 2) of MulZeroClass (Fin 2) ▶
[] [0.000065s] ✅ apply @SemigroupWithZero.toMulZeroClass to MulZeroClass (Fin 2) ▶
[] [0.000062s] ✅ apply @NonUnitalSemiring.toSemigroupWithZero to SemigroupWithZero (Fin 2) ▶
[resume] [0.000005s] propagating NonUnitalSemiring (Fin 2) to subgoal NonUnitalSemiring (Fin 2) of SemigroupWithZero (Fin 2) ▶
[resume] [0.000004s] propagating SemigroupWithZero (Fin 2) to subgoal SemigroupWithZero (Fin 2) of MulZeroClass (Fin 2) ▶
[] [0.000044s] ✅ apply @MonoidWithZero.toSemigroupWithZero to SemigroupWithZero (Fin 2) ▶
[] 286 more entries... ▼
[resume] [0.000004s] propagating MonoidWithZero (Fin 2) to subgoal MonoidWithZero (Fin 2) of SemigroupWithZero (Fin 2) ▶
[] [0.000051s] ✅ apply @Fin.instZeroFin to Zero (Fin 2) ▶
[resume] [0.000006s] propagating NeZero 2 to subgoal NeZero 2 of Zero (Fin 2) ▶
[resume] [0.000006s] propagating NeZero 2 to subgoal NeZero 2 of Zero (Fin 2) ▶
[resume] [0.000005s] propagating NeZero 2 to subgoal NeZero 2 of Zero (Fin 2) ▶
[resume] [0.000005s] propagating NeZero (1 + 1) to subgoal NeZero 2 of Zero (Fin 2) ▶
[] [0.000068s] ✅ apply @LinearOrderedCommMonoidWithZero.toZero to Zero (Fin 2) ▶
[] [0.000046s] ✅ apply @CommMonoidWithZero.toZero to Zero (Fin 2) ▶
[resume] [0.000005s] propagating CommMonoidWithZero (Fin 2) to subgoal CommMonoidWithZero (Fin 2) of Zero (Fin 2) ▶
[] [0.000050s] ✅ apply @MonoidWithZero.toZero to Zero (Fin 2) ▶
[resume] [0.000006s] propagating MonoidWithZero (Fin 2) to subgoal MonoidWithZero (Fin 2) of Zero (Fin 2) ▶
[] [0.000049s] ✅ apply @MulZeroOneClass.toZero to Zero (Fin 2) ▶
[resume] [0.000005s] propagating MulZeroOneClass (Fin 2) to subgoal MulZeroOneClass (Fin 2) of Zero (Fin 2) ▶
[] [0.000045s] ✅ apply @SemigroupWithZero.toZero to Zero (Fin 2) ▶
[resume] [0.000005s] propagating SemigroupWithZero (Fin 2) to subgoal SemigroupWithZero (Fin 2) of Zero (Fin 2) ▶
[] [0.000074s] ✅ apply @NegZeroClass.toZero to Zero (Fin 2) ▶
[] [0.000122s] ✅ apply @SubNegZeroMonoid.toNegZeroClass to NegZeroClass (Fin 2) ▶
[] [0.000079s] ✅ apply @SubtractionMonoid.toSubNegZeroMonoid to SubNegZeroMonoid (Fin 2) ▶
[] [0.000254s] ✅ apply @SubtractionCommMonoid.toSubtractionMonoid to SubtractionMonoid (Fin 2) ▶
[] [0.000103s] ✅ apply @AddCommGroup.toDivisionAddCommMonoid to SubtractionCommMonoid (Fin 2) ▶
[resume] [0.000008s] propagating AddCommGroup (Fin 2) to subgoal AddCommGroup (Fin 2) of SubtractionCommMonoid (Fin 2) ▶
[resume] [0.000005s] propagating SubtractionCommMonoid
(Fin
2) to subgoal SubtractionCommMonoid
(Fin
2) of SubtractionMonoid
(Fin 2) ▶
[resume] [0.000004s] propagating SubtractionMonoid (Fin 2) to subgoal SubtractionMonoid (Fin 2) of SubNegZeroMonoid (Fin 2) ▶
[resume] [0.000005s] propagating SubNegZeroMonoid (Fin 2) to subgoal SubNegZeroMonoid (Fin 2) of NegZeroClass (Fin 2) ▶
[resume] [0.000004s] propagating NegZeroClass (Fin 2) to subgoal NegZeroClass (Fin 2) of Zero (Fin 2) ▶
[] [0.000053s] ✅ apply @AddGroup.toSubtractionMonoid to SubtractionMonoid (Fin 2) ▶
[resume] [0.000005s] propagating AddGroup (Fin 2) to subgoal AddGroup (Fin 2) of SubtractionMonoid (Fin 2) ▶
[] [0.000066s] ✅ apply @MulZeroClass.negZeroClass to NegZeroClass (Fin 2) ▶
[resume] [0.000039s] propagating MulZeroClass (Fin 2) to subgoal MulZeroClass (Fin 2) of NegZeroClass (Fin 2) ▶
[] [0.000497s] ✅ apply Fin.instHasDistribNeg to HasDistribNeg (Fin 2) ▶
[resume] [0.000007s] propagating HasDistribNeg (Fin 2) to subgoal HasDistribNeg (Fin 2) of NegZeroClass (Fin 2) ▶
[] [0.002454s] ✅ apply @NonUnitalNonAssocRing.toHasDistribNeg to HasDistribNeg (Fin 2) ▶
[resume] [0.000007s] propagating HasDistribNeg (Fin 2) to subgoal HasDistribNeg (Fin 2) of NegZeroClass (Fin 2) ▶
[] [0.000089s] ✅ apply @AddRightCancelMonoid.toZero to Zero (Fin 2) ▶
[] [0.000086s] ✅ apply @AddCancelMonoid.toAddRightCancelMonoid to AddRightCancelMonoid (Fin 2) ▶
[] [0.000062s] ✅ apply @AddGroup.toAddCancelMonoid to AddCancelMonoid (Fin 2) ▶
[resume] [0.000007s] propagating AddGroup (Fin 2) to subgoal AddGroup (Fin 2) of AddCancelMonoid (Fin 2) ▶
[resume] [0.000004s] propagating AddCancelMonoid (Fin 2) to subgoal AddCancelMonoid (Fin 2) of AddRightCancelMonoid (Fin 2) ▶
[resume] [0.000005s] propagating AddRightCancelMonoid (Fin 2) to subgoal AddRightCancelMonoid (Fin 2) of Zero (Fin 2) ▶
[] [0.000064s] ✅ apply AddCancelCommMonoid.toAddCancelMonoid to AddCancelMonoid (Fin 2) ▶
[] [0.000070s] ✅ apply @OrderedCancelAddCommMonoid.toCancelAddCommMonoid to AddCancelCommMonoid (Fin 2) ▶
[] [0.000060s] ✅ apply @AddCommGroup.toAddCancelCommMonoid to AddCancelCommMonoid (Fin 2) ▶
[resume] [0.000006s] propagating AddCommGroup (Fin 2) to subgoal AddCommGroup (Fin 2) of AddCancelCommMonoid (Fin 2) ▶
[resume] [0.000004s] propagating AddCancelCommMonoid (Fin 2) to subgoal AddCancelCommMonoid (Fin 2) of AddCancelMonoid (Fin 2) ▶
[] [0.000062s] ✅ apply @AddLeftCancelMonoid.toZero to Zero (Fin 2) ▶
[] [0.000062s] ✅ apply @AddCancelCommMonoid.toAddLeftCancelMonoid to AddLeftCancelMonoid (Fin 2) ▶
[resume] [0.000005s] propagating AddCancelCommMonoid
(Fin
2) to subgoal AddCancelCommMonoid
(Fin
2) of AddLeftCancelMonoid
(Fin 2) ▶
[resume] [0.000004s] propagating AddLeftCancelMonoid (Fin 2) to subgoal AddLeftCancelMonoid (Fin 2) of Zero (Fin 2) ▶
[] [0.000044s] ✅ apply @AddCancelMonoid.toAddLeftCancelMonoid to AddLeftCancelMonoid (Fin 2) ▶
[resume] [0.000004s] propagating AddCancelMonoid (Fin 2) to subgoal AddCancelMonoid (Fin 2) of AddLeftCancelMonoid (Fin 2) ▶
[] 236 more entries... ▼
[] [0.000071s] ✅ apply @AddMonoid.toZero to Zero (Fin 2) ▶
[] [0.000057s] ✅ apply @AddMonoidWithOne.toAddMonoid to AddMonoid (Fin 2) ▶
[resume] [0.000006s] propagating AddMonoidWithOne (Fin 2) to subgoal AddMonoidWithOne (Fin 2) of AddMonoid (Fin 2) ▶
[resume] [0.000005s] propagating AddMonoid (Fin 2) to subgoal AddMonoid (Fin 2) of Zero (Fin 2) ▶
[] [0.000056s] ✅ apply @SubNegMonoid.toAddMonoid to AddMonoid (Fin 2) ▶
[] [0.000066s] ✅ apply @LinearOrderedAddCommGroupWithTop.toSubNegMonoid to SubNegMonoid (Fin 2) ▶
[] [0.000054s] ✅ apply @AddGroup.toSubNegMonoid to SubNegMonoid (Fin 2) ▶
[resume] [0.000005s] propagating AddGroup (Fin 2) to subgoal AddGroup (Fin 2) of SubNegMonoid (Fin 2) ▶
[resume] [0.000004s] propagating SubNegMonoid (Fin 2) to subgoal SubNegMonoid (Fin 2) of AddMonoid (Fin 2) ▶
[] [0.000052s] ✅ apply @SubtractionMonoid.toSubNegMonoid to SubNegMonoid (Fin 2) ▶
[resume] [0.000005s] propagating SubtractionMonoid (Fin 2) to subgoal SubtractionMonoid (Fin 2) of SubNegMonoid (Fin 2) ▶
[] [0.000045s] ✅ apply @SubNegZeroMonoid.toSubNegMonoid to SubNegMonoid (Fin 2) ▶
[resume] [0.000005s] propagating SubNegZeroMonoid (Fin 2) to subgoal SubNegZeroMonoid (Fin 2) of SubNegMonoid (Fin 2) ▶
[] [0.000067s] ✅ apply @AddCommMonoid.toAddMonoid to AddMonoid (Fin 2) ▶
[] [0.000058s] ✅ apply Fin.addCommMonoid to AddCommMonoid (Fin 2) ▶
[resume] [0.000006s] propagating NeZero 2 to subgoal NeZero 2 of AddCommMonoid (Fin 2) ▶
[resume] [0.000005s] propagating AddCommMonoid (Fin 2) to subgoal AddCommMonoid (Fin 2) of AddMonoid (Fin 2) ▶
[resume] [0.000006s] propagating NeZero 2 to subgoal NeZero 2 of AddCommMonoid (Fin 2) ▶
[resume] [0.000005s] propagating NeZero 2 to subgoal NeZero 2 of AddCommMonoid (Fin 2) ▶
[resume] [0.000007s] propagating NeZero (1 + 1) to subgoal NeZero 2 of AddCommMonoid (Fin 2) ▶
[] [0.000065s] ✅ apply @OrderedAddCommMonoid.toAddCommMonoid to AddCommMonoid (Fin 2) ▶
[] [0.000060s] ✅ apply @NonUnitalNonAssocSemiring.toAddCommMonoid to AddCommMonoid (Fin 2) ▶
[resume] [0.000006s] propagating NonUnitalNonAssocSemiring
(Fin
2) to subgoal NonUnitalNonAssocSemiring
(Fin
2) of AddCommMonoid
(Fin 2) ▶
[] [0.000056s] ✅ apply @AddCommMonoidWithOne.toAddCommMonoid to AddCommMonoid (Fin 2) ▶
[resume] [0.000005s] propagating AddCommMonoidWithOne (Fin 2) to subgoal AddCommMonoidWithOne (Fin 2) of AddCommMonoid (Fin 2) ▶
[] [0.000039s] ✅ apply @AddCommGroup.toAddCommMonoid to AddCommMonoid (Fin 2) ▶
[resume] [0.000005s] propagating AddCommGroup (Fin 2) to subgoal AddCommGroup (Fin 2) of AddCommMonoid (Fin 2) ▶
[] [0.000046s] ✅ apply @SubtractionCommMonoid.toAddCommMonoid to AddCommMonoid (Fin 2) ▶
[resume] [0.000004s] propagating SubtractionCommMonoid (Fin 2) to subgoal SubtractionCommMonoid (Fin 2) of AddCommMonoid (Fin 2) ▶
[] [0.000044s] ✅ apply @AddCancelCommMonoid.toAddCommMonoid to AddCommMonoid (Fin 2) ▶
[resume] [0.000005s] propagating AddCancelCommMonoid (Fin 2) to subgoal AddCancelCommMonoid (Fin 2) of AddCommMonoid (Fin 2) ▶
[] [0.000046s] ✅ apply @AddRightCancelMonoid.toAddMonoid to AddMonoid (Fin 2) ▶
[resume] [0.000005s] propagating AddRightCancelMonoid (Fin 2) to subgoal AddRightCancelMonoid (Fin 2) of AddMonoid (Fin 2) ▶
[] [0.000047s] ✅ apply @AddLeftCancelMonoid.toAddMonoid to AddMonoid (Fin 2) ▶
[resume] [0.000005s] propagating AddLeftCancelMonoid (Fin 2) to subgoal AddLeftCancelMonoid (Fin 2) of AddMonoid (Fin 2) ▶
[] [0.000065s] ✅ apply @AddZeroClass.toZero to Zero (Fin 2) ▶
[] [0.000060s] ✅ apply @AddMonoid.toAddZeroClass to AddZeroClass (Fin 2) ▶
[resume] [0.000007s] propagating AddMonoid (Fin 2) to subgoal AddMonoid (Fin 2) of AddZeroClass (Fin 2) ▶
[resume] [0.000004s] propagating AddZeroClass (Fin 2) to subgoal AddZeroClass (Fin 2) of Zero (Fin 2) ▶
[] [0.000073s] ✅ apply @Zero.ofOfNat0 to Zero (Fin 2) ▶
[] [0.000071s] ✅ apply @Fin.instOfNatFin to OfNat (Fin 2) 0 ▶
[resume] [0.000009s] propagating NeZero 2 to subgoal NeZero 2 of OfNat (Fin 2) 0 ▶
[resume] [0.000005s] propagating OfNat (Fin 2) 0 to subgoal OfNat (Fin 2) 0 of Zero (Fin 2) ▶
[resume] [0.000007s] propagating NeZero 2 to subgoal NeZero 2 of OfNat (Fin 2) 0 ▶
[resume] [0.000006s] propagating NeZero 2 to subgoal NeZero 2 of OfNat (Fin 2) 0 ▶
[resume] [0.000007s] propagating NeZero (1 + 1) to subgoal NeZero 2 of OfNat (Fin 2) 0 ▶
[] [0.000157s] ✅ apply @Fin.instOfNat to OfNat (Fin 2) 0 ▶
[resume] [0.000006s] propagating OfNat (Fin (1 + 1)) 0 to subgoal OfNat (Fin 2) 0 of Zero (Fin 2) ▶
[] [0.000061s] ✅ apply @Zero.toOfNat0 to OfNat (Fin 2) 0 ▶
[resume] [0.000008s] propagating Zero (Fin 2) to subgoal Zero (Fin 2) of OfNat (Fin 2) 0 ▶
[] 186 more entries... ▼
[] [0.000073s] ✅ apply @instOfNatAtLeastTwo to OfNat (Fin 2) 0 ▶
[resume] [0.000018s] propagating NatCast (Fin 2) to subgoal NatCast (Fin 2) of OfNat (Fin 2) 0 ▶
[] [0.000074s] ❌ apply @instNatAtLeastTwo to Nat.AtLeastTwo 0 ▶
[] [0.003097s] ✅ apply CharP.pi to CharP (Fin 2 → ℝ) 1 ▶
[resume] [0.000039s] propagating Nonempty (Fin 2) to subgoal Nonempty (Fin 2) of CharP (Fin 2 → ℝ) 1 ▶
[] [0.000084s] ✅ apply @Semiring.toNonAssocSemiring to NonAssocSemiring (Fin 2 → ℝ) ▶
[] [0.000107s] ✅ apply @Pi.semiring to Semiring (Fin 2 → ℝ) ▶
[resume] [0.000008s] propagating Fin 2 → Semiring ℝ to subgoal Fin 2 → Semiring ℝ of Semiring (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating Semiring (Fin 2 → ℝ) to subgoal Semiring (Fin 2 → ℝ) of NonAssocSemiring (Fin 2 → ℝ) ▶
[] [0.000061s] ❌ apply @DirectSum.GradeZero.semiring to Semiring (Fin 2 → ℝ) ▶
[] [0.000072s] ✅ apply @IdemSemiring.toSemiring to Semiring (Fin 2 → ℝ) ▶
[] [0.000092s] ✅ apply @Pi.instIdemSemiring to IdemSemiring (Fin 2 → ℝ) ▶
[] [0.000057s] ✅ apply @KleeneAlgebra.toIdemSemiring to IdemSemiring (Fin 2 → ℝ) ▶
[] [0.000103s] ✅ apply @Pi.instKleeneAlgebraForAll to KleeneAlgebra (Fin 2 → ℝ) ▶
[] [0.000058s] ✅ apply @IdemCommSemiring.toIdemSemiring to IdemSemiring (Fin 2 → ℝ) ▶
[] [0.000124s] ✅ apply @Pi.instIdemCommSemiringForAll to IdemCommSemiring (Fin 2 → ℝ) ▶
[] [0.000058s] ✅ apply @DivisionSemiring.toSemiring to Semiring (Fin 2 → ℝ) ▶
[] [0.000065s] ✅ apply @Semifield.toDivisionSemiring to DivisionSemiring (Fin 2 → ℝ) ▶
[] [0.000062s] ✅ apply @LinearOrderedSemifield.toSemifield to Semifield (Fin 2 → ℝ) ▶
[] [0.000057s] ✅ apply @CanonicallyLinearOrderedSemifield.toLinearOrderedSemifield to LinearOrderedSemifield (Fin 2 → ℝ) ▶
[] [0.000052s] ✅ apply @LinearOrderedField.toLinearOrderedSemifield to LinearOrderedSemifield (Fin 2 → ℝ) ▶
[] [0.000062s] ✅ apply @ConditionallyCompleteLinearOrderedField.toLinearOrderedField to LinearOrderedField (Fin 2 → ℝ) ▶
[] [0.000048s] ✅ apply @NormedLinearOrderedField.toLinearOrderedField to LinearOrderedField (Fin 2 → ℝ) ▶
[] [0.000054s] ✅ apply @Field.toSemifield to Semifield (Fin 2 → ℝ) ▶
[] [0.000056s] ✅ apply @NormedField.toField to Field (Fin 2 → ℝ) ▶
[] [0.000054s] ✅ apply @DenselyNormedField.toNormedField to NormedField (Fin 2 → ℝ) ▶
[] [0.000080s] ✅ apply @RCLike.toDenselyNormedField to DenselyNormedField (Fin 2 → ℝ) ▶
[] [0.000048s] ✅ apply @NontriviallyNormedField.toNormedField to NormedField (Fin 2 → ℝ) ▶
[] [0.000052s] ✅ apply @DenselyNormedField.toNontriviallyNormedField to NontriviallyNormedField (Fin 2 → ℝ) ▶
[] [0.000049s] ✅ apply NormedLinearOrderedField.toNormedField to NormedField (Fin 2 → ℝ) ▶
[] [0.000043s] ✅ apply @LinearOrderedField.toField to Field (Fin 2 → ℝ) ▶
[] [0.000061s] ✅ apply littleWedderburn to Field (Fin 2 → ℝ) ▶
[] [0.000057s] ✅ apply @NormedDivisionRing.toDivisionRing to DivisionRing (Fin 2 → ℝ) ▶
[] [0.000046s] ✅ apply @NormedField.toNormedDivisionRing to NormedDivisionRing (Fin 2 → ℝ) ▶
[] [0.000046s] ✅ apply @Field.toDivisionRing to DivisionRing (Fin 2 → ℝ) ▶
[] [0.000043s] ✅ apply @DivisionRing.toDivisionSemiring to DivisionSemiring (Fin 2 → ℝ) ▶
[] [0.000071s] ✅ apply @StrictOrderedSemiring.toSemiring to Semiring (Fin 2 → ℝ) ▶
[] [0.000054s] ✅ apply @LinearOrderedSemiring.toStrictOrderedSemiring to StrictOrderedSemiring (Fin 2 → ℝ) ▶
[] [0.000051s] ✅ apply @LinearOrderedCommSemiring.toLinearOrderedSemiring to LinearOrderedSemiring (Fin 2 → ℝ) ▶
[] [0.000046s] ✅ apply @LinearOrderedSemifield.toLinearOrderedCommSemiring to LinearOrderedCommSemiring (Fin 2 → ℝ) ▶
[] [0.000054s] ✅ apply @LinearOrderedCommRing.toLinearOrderedCommSemiring to LinearOrderedCommSemiring (Fin 2 → ℝ) ▶
[] [0.000045s] ✅ apply @LinearOrderedField.toLinearOrderedCommRing to LinearOrderedCommRing (Fin 2 → ℝ) ▶
[] [0.000049s] ✅ apply @LinearOrderedRing.toLinearOrderedSemiring to LinearOrderedSemiring (Fin 2 → ℝ) ▶
[] [0.000049s] ✅ apply @LinearOrderedCommRing.toLinearOrderedRing to LinearOrderedRing (Fin 2 → ℝ) ▶
[] [0.000053s] ✅ apply @StrictOrderedCommSemiring.toStrictOrderedSemiring to StrictOrderedSemiring (Fin 2 → ℝ) ▶
[] [0.000045s] ✅ apply @LinearOrderedCommSemiring.toStrictOrderedCommSemiring to StrictOrderedCommSemiring (Fin 2 → ℝ) ▶
[] [0.000059s] ✅ apply @StrictOrderedCommRing.toStrictOrderedCommSemiring to StrictOrderedCommSemiring (Fin 2 → ℝ) ▶
[] [0.000045s] ✅ apply @LinearOrderedCommRing.toStrictOrderedCommRing to StrictOrderedCommRing (Fin 2 → ℝ) ▶
[] [0.000050s] ✅ apply @StrictOrderedRing.toStrictOrderedSemiring to StrictOrderedSemiring (Fin 2 → ℝ) ▶
[] [0.000046s] ✅ apply @LinearOrderedRing.toStrictOrderedRing to StrictOrderedRing (Fin 2 → ℝ) ▶
[] 136 more entries... ▼
[] [0.000041s] ✅ apply @StrictOrderedCommRing.toStrictOrderedRing to StrictOrderedRing (Fin 2 → ℝ) ▶
[] [0.000063s] ✅ apply @OrderedSemiring.toSemiring to Semiring (Fin 2 → ℝ) ▶
[] [0.000106s] ✅ apply @Pi.orderedSemiring to OrderedSemiring (Fin 2 → ℝ) ▶
[resume] [0.000008s] propagating Fin 2 → OrderedSemiring ℝ to subgoal Fin 2 → OrderedSemiring ℝ of OrderedSemiring (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating OrderedSemiring (Fin 2 → ℝ) to subgoal OrderedSemiring (Fin 2 → ℝ) of Semiring (Fin 2 → ℝ) ▶
[] [0.000060s] ✅ apply @OrderedCommSemiring.toOrderedSemiring to OrderedSemiring (Fin 2 → ℝ) ▶
[] [0.000098s] ✅ apply @Pi.orderedCommSemiring to OrderedCommSemiring (Fin 2 → ℝ) ▶
[resume] [0.000006s] propagating Fin 2 →
OrderedCommSemiring
ℝ to subgoal Fin
2 →
OrderedCommSemiring
ℝ of OrderedCommSemiring
(Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating OrderedCommSemiring
(Fin 2 →
ℝ) to subgoal OrderedCommSemiring
(Fin 2 →
ℝ) of OrderedSemiring
(Fin 2 → ℝ) ▶
[] [0.000053s] ✅ apply @CanonicallyOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring (Fin 2 → ℝ) ▶
[] [0.000051s] ✅ apply @CanonicallyLinearOrderedSemifield.toCanonicallyOrderedCommSemiring to CanonicallyOrderedCommSemiring
(Fin 2 → ℝ) ▶
[] [0.000043s] ✅ apply @StrictOrderedCommSemiring.toOrderedCommSemiring to OrderedCommSemiring (Fin 2 → ℝ) ▶
[] [0.000052s] ✅ apply @OrderedCommRing.toOrderedCommSemiring to OrderedCommSemiring (Fin 2 → ℝ) ▶
[] [0.000089s] ✅ apply @Pi.orderedCommRing to OrderedCommRing (Fin 2 → ℝ) ▶
[resume] [0.000007s] propagating Fin 2 → OrderedCommRing ℝ to subgoal Fin 2 → OrderedCommRing ℝ of OrderedCommRing (Fin 2 → ℝ) ▶
[resume] [0.000004s] propagating OrderedCommRing
(Fin 2 →
ℝ) to subgoal OrderedCommRing
(Fin 2 →
ℝ) of OrderedCommSemiring
(Fin 2 → ℝ) ▶
[] [0.000055s] ✅ apply @StrictOrderedCommRing.toOrderedCommRing to OrderedCommRing (Fin 2 → ℝ) ▶
[] [0.000044s] ✅ apply @StrictOrderedSemiring.toOrderedSemiring to OrderedSemiring (Fin 2 → ℝ) ▶
[] [0.000056s] ✅ apply @OrderedRing.toOrderedSemiring to OrderedSemiring (Fin 2 → ℝ) ▶
[] [0.000103s] ✅ apply @Pi.orderedRing to OrderedRing (Fin 2 → ℝ) ▶
[resume] [0.000007s] propagating Fin 2 → OrderedRing ℝ to subgoal Fin 2 → OrderedRing ℝ of OrderedRing (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating OrderedRing (Fin 2 → ℝ) to subgoal OrderedRing (Fin 2 → ℝ) of OrderedSemiring (Fin 2 → ℝ) ▶
[] [0.000044s] ✅ apply @OrderedCommRing.toOrderedRing to OrderedRing (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating OrderedCommRing (Fin 2 → ℝ) to subgoal OrderedCommRing (Fin 2 → ℝ) of OrderedRing (Fin 2 → ℝ) ▶
[] [0.000049s] ✅ apply @StrictOrderedRing.toOrderedRing to OrderedRing (Fin 2 → ℝ) ▶
[] [0.000062s] ✅ apply @CommSemiring.toSemiring to Semiring (Fin 2 → ℝ) ▶
[] [0.000093s] ✅ apply @Pi.commSemiring to CommSemiring (Fin 2 → ℝ) ▶
[resume] [0.000006s] propagating Fin 2 → CommSemiring ℝ to subgoal Fin 2 → CommSemiring ℝ of CommSemiring (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating CommSemiring (Fin 2 → ℝ) to subgoal CommSemiring (Fin 2 → ℝ) of Semiring (Fin 2 → ℝ) ▶
[] [0.000066s] ❌ apply @DirectSum.GradeZero.commSemiring to CommSemiring (Fin 2 → ℝ) ▶
[] [0.000045s] ✅ apply @IdemCommSemiring.toCommSemiring to CommSemiring (Fin 2 → ℝ) ▶
[] [0.000044s] ✅ apply @Semifield.toCommSemiring to CommSemiring (Fin 2 → ℝ) ▶
[] [0.000044s] ✅ apply @CanonicallyOrderedCommSemiring.toCommSemiring to CommSemiring (Fin 2 → ℝ) ▶
[] [0.000041s] ✅ apply @StrictOrderedCommSemiring.toCommSemiring to CommSemiring (Fin 2 → ℝ) ▶
[] [0.000049s] ✅ apply @OrderedCommSemiring.toCommSemiring to CommSemiring (Fin 2 → ℝ) ▶
[resume] [0.000006s] propagating OrderedCommSemiring
(Fin 2 →
ℝ) to subgoal OrderedCommSemiring
(Fin 2 →
ℝ) of CommSemiring
(Fin 2 → ℝ) ▶
[] [0.000058s] ✅ apply @CommRing.toCommSemiring to CommSemiring (Fin 2 → ℝ) ▶
[] [0.000090s] ✅ apply @Pi.commRing to CommRing (Fin 2 → ℝ) ▶
[resume] [0.000007s] propagating Fin 2 → CommRing ℝ to subgoal Fin 2 → CommRing ℝ of CommRing (Fin 2 → ℝ) ▶
[resume] [0.000004s] propagating CommRing (Fin 2 → ℝ) to subgoal CommRing (Fin 2 → ℝ) of CommSemiring (Fin 2 → ℝ) ▶
[] [0.000074s] ❌ apply @DirectSum.GradeZero.commRing to CommRing (Fin 2 → ℝ) ▶
[] [0.000304s] ✅ apply @EuclideanDomain.toCommRing to CommRing (Fin 2 → ℝ) ▶
[] [0.000070s] ✅ apply @Field.toEuclideanDomain to EuclideanDomain (Fin 2 → ℝ) ▶
[] [0.000048s] ✅ apply @Field.toCommRing to CommRing (Fin 2 → ℝ) ▶
[] [0.000055s] ✅ apply @StrictOrderedCommRing.toCommRing to CommRing (Fin 2 → ℝ) ▶
[] [0.000043s] ✅ apply @OrderedCommRing.toCommRing to CommRing (Fin 2 → ℝ) ▶
[resume] [0.000008s] propagating OrderedCommRing (Fin 2 → ℝ) to subgoal OrderedCommRing (Fin 2 → ℝ) of CommRing (Fin 2 → ℝ) ▶
[] [0.000058s] ✅ apply @SeminormedCommRing.toCommRing to CommRing (Fin 2 → ℝ) ▶
[] [0.000129s] ✅ apply @Pi.seminormedCommRing to SeminormedCommRing (Fin 2 → ℝ) ▶
[] [0.000063s] ✅ apply Fin.fintype to Fintype (Fin 2) ▶
[] 86 more entries... ▼
[resume] [0.000029s] propagating Fintype (Fin 2) to subgoal Fintype (Fin 2) of SeminormedCommRing (Fin 2 → ℝ) ▶
[resume] [0.000007s] propagating Fin 2 →
SeminormedCommRing
ℝ to subgoal Fin
2 →
SeminormedCommRing
ℝ of SeminormedCommRing
(Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating SeminormedCommRing (Fin 2 → ℝ) to subgoal SeminormedCommRing (Fin 2 → ℝ) of CommRing (Fin 2 → ℝ) ▶
[] [0.000051s] ✅ apply @NonemptyFiniteLinearOrder.toFintype to Fintype (Fin 2) ▶
[resume] [0.000006s] propagating NonemptyFiniteLinearOrder
(Fin
(1 +
1)) to subgoal NonemptyFiniteLinearOrder
(Fin
2) of Fintype
(Fin 2) ▶
[] [0.000094s] ✅ apply @CategoryTheory.FinCategory.fintypeObj to Fintype (Fin 2) ▶
[] [0.000092s] ✅ apply @CategoryTheory.Groupoid.toCategory to CategoryTheory.SmallCategory (Fin 2) ▶
[] [0.000088s] ✅ apply CategoryTheory.StrictBicategory.category to CategoryTheory.SmallCategory (Fin 2) ▶
[] [0.000078s] ✅ apply Preorder.smallCategory to CategoryTheory.SmallCategory (Fin 2) ▶
[resume] [0.000007s] propagating Preorder (Fin 2) to subgoal Preorder (Fin 2) of CategoryTheory.SmallCategory (Fin 2) ▶
[resume] [0.000020s] propagating CategoryTheory.SmallCategory
(Fin
2) to subgoal CategoryTheory.SmallCategory
(Fin
2) of Fintype
(Fin 2) ▶
[] [0.000064s] ✅ apply @Unique.fintype to Fintype (Fin 2) ▶
[] [0.000094s] ✅ apply @IsSimpleOrder.instFintype to Fintype (Fin 2) ▶
[] [0.000180s] ✅ apply instDecidableEqFin to DecidableEq (Fin 2) ▶
[resume] [0.000004s] propagating (a b : Fin 2) → Decidable (a = b) to subgoal DecidableEq (Fin 2) of Fintype (Fin 2) ▶
[resume] [0.000004s] propagating LE (Fin 2) to subgoal LE (Fin 2) of Fintype (Fin 2) ▶
[resume] [0.000026s] propagating BoundedOrder (Fin 2) to subgoal BoundedOrder (Fin 2) of Fintype (Fin 2) ▶
[resume] [0.000016s] propagating BoundedOrder (Fin 2) to subgoal BoundedOrder (Fin 2) of Fintype (Fin 2) ▶
[resume] [0.000013s] propagating BoundedOrder (Fin (1 + 1)) to subgoal BoundedOrder (Fin 2) of Fintype (Fin 2) ▶
[] [0.000210s] ✅ apply @instDecidableEq to DecidableEq (Fin 2) ▶
[resume] [0.000014s] propagating Fin 2 →
Fin 2 →
LinearOrder
(Fin
2) to subgoal Fin
2 →
Fin 2 →
LinearOrder
(Fin
2) of DecidableEq
(Fin 2) ▶
[] [0.000171s] ✅ apply @FinEnum.decEq to DecidableEq (Fin 2) ▶
[] [0.000065s] ✅ apply @FinEnum.fin to FinEnum (Fin 2) ▶
[resume] [0.000016s] propagating FinEnum (Fin 2) to subgoal FinEnum (Fin 2) of DecidableEq (Fin 2) ▶
[resume] [0.000014s] propagating Fin 2 →
Fin 2 →
FinEnum
(Fin
2) to subgoal Fin
2 →
Fin 2 →
FinEnum
(Fin
2) of DecidableEq
(Fin 2) ▶
[] [0.000187s] ✅ apply @RCLike.toDecidableEq to DecidableEq (Fin 2) ▶
[] [0.000170s] ✅ apply @decidableEq_of_subsingleton to DecidableEq (Fin 2) ▶
[] [0.000046s] ❌ apply instSubsingleton to Subsingleton (Fin 2) ▶
[] [0.000052s] ✅ apply @CharP.CharOne.subsingleton to Subsingleton (Fin 2) ▶
[resume] [0.000031s] propagating NonAssocSemiring (Fin 2) to subgoal NonAssocSemiring (Fin 2) of Subsingleton (Fin 2) ▶
[] [0.000157s] ❌ apply Fin.charP to CharP (Fin 2) 1 ▶
[] [0.000072s] ✅ apply @Unique.instSubsingleton to Subsingleton (Fin 2) ▶
[] [0.000056s] ✅ apply @IsEmpty.instSubsingleton to Subsingleton (Fin 2) ▶
[] [0.000052s] ✅ apply @FinEnum.instFintype to Fintype (Fin 2) ▶
[resume] [0.000009s] propagating FinEnum (Fin 2) to subgoal FinEnum (Fin 2) of Fintype (Fin 2) ▶
[] [0.000089s] ✅ apply @SetLike.instFintype to Fintype (Fin 2) ▶
[] [0.000059s] ✅ apply @NormedCommRing.toSeminormedCommRing to SeminormedCommRing (Fin 2 → ℝ) ▶
[] [0.000103s] ✅ apply @Pi.normedCommutativeRing to NormedCommRing (Fin 2 → ℝ) ▶
[resume] [0.000020s] propagating Fintype (Fin 2) to subgoal Fintype (Fin 2) of NormedCommRing (Fin 2 → ℝ) ▶
[resume] [0.000009s] propagating Fin 2 → NormedCommRing ℝ to subgoal Fin 2 → NormedCommRing ℝ of NormedCommRing (Fin 2 → ℝ) ▶
[resume] [0.000006s] propagating NormedCommRing
(Fin 2 →
ℝ) to subgoal NormedCommRing
(Fin 2 →
ℝ) of SeminormedCommRing
(Fin 2 → ℝ) ▶
[] [0.000059s] ✅ apply @NormedField.toNormedCommRing to NormedCommRing (Fin 2 → ℝ) ▶
[] [0.000057s] ✅ apply @BooleanRing.toCommRing to CommRing (Fin 2 → ℝ) ▶
[] [0.000062s] ✅ apply @Ring.toSemiring to Semiring (Fin 2 → ℝ) ▶
[] [0.000108s] ✅ apply @Pi.ring to Ring (Fin 2 → ℝ) ▶
[resume] [0.000008s] propagating Fin 2 → Ring ℝ to subgoal Fin 2 → Ring ℝ of Ring (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating Ring (Fin 2 → ℝ) to subgoal Ring (Fin 2 → ℝ) of Semiring (Fin 2 → ℝ) ▶
[] [0.000058s] ✅ apply @NormedRing.toRing to Ring (Fin 2 → ℝ) ▶
[] [0.000075s] ✅ apply @Pi.normedRing to NormedRing (Fin 2 → ℝ) ▶
[resume] [0.000015s] propagating Fintype (Fin 2) to subgoal Fintype (Fin 2) of NormedRing (Fin 2 → ℝ) ▶
[] 36 more entries... ▼
[resume] [0.000008s] propagating Fin 2 → NormedRing ℝ to subgoal Fin 2 → NormedRing ℝ of NormedRing (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating NormedRing (Fin 2 → ℝ) to subgoal NormedRing (Fin 2 → ℝ) of Ring (Fin 2 → ℝ) ▶
[] [0.000045s] ✅ apply @NormedCommRing.toNormedRing to NormedRing (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating NormedCommRing (Fin 2 → ℝ) to subgoal NormedCommRing (Fin 2 → ℝ) of NormedRing (Fin 2 → ℝ) ▶
[] [0.000062s] ✅ apply @NormedDivisionRing.toNormedRing to NormedRing (Fin 2 → ℝ) ▶
[] [0.000056s] ✅ apply @SeminormedRing.toRing to Ring (Fin 2 → ℝ) ▶
[] [0.000088s] ✅ apply @Pi.seminormedRing to SeminormedRing (Fin 2 → ℝ) ▶
[resume] [0.000018s] propagating Fintype (Fin 2) to subgoal Fintype (Fin 2) of SeminormedRing (Fin 2 → ℝ) ▶
[resume] [0.000007s] propagating Fin 2 → SeminormedRing ℝ to subgoal Fin 2 → SeminormedRing ℝ of SeminormedRing (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating SeminormedRing (Fin 2 → ℝ) to subgoal SeminormedRing (Fin 2 → ℝ) of Ring (Fin 2 → ℝ) ▶
[] [0.000043s] ✅ apply @SeminormedCommRing.toSeminormedRing to SeminormedRing (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating SeminormedCommRing
(Fin 2 →
ℝ) to subgoal SeminormedCommRing
(Fin 2 →
ℝ) of SeminormedRing
(Fin 2 → ℝ) ▶
[] [0.000048s] ✅ apply @NormedRing.toSeminormedRing to SeminormedRing (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating NormedRing (Fin 2 → ℝ) to subgoal NormedRing (Fin 2 → ℝ) of SeminormedRing (Fin 2 → ℝ) ▶
[] [0.000063s] ❌ apply @DirectSum.GradeZero.ring to Ring (Fin 2 → ℝ) ▶
[] [0.000065s] ✅ apply @BooleanRing.toRing to Ring (Fin 2 → ℝ) ▶
[] [0.000042s] ✅ apply @DivisionRing.toRing to Ring (Fin 2 → ℝ) ▶
[] [0.000041s] ✅ apply @StrictOrderedRing.toRing to Ring (Fin 2 → ℝ) ▶
[] [0.000040s] ✅ apply @OrderedRing.toRing to Ring (Fin 2 → ℝ) ▶
[resume] [0.000006s] propagating OrderedRing (Fin 2 → ℝ) to subgoal OrderedRing (Fin 2 → ℝ) of Ring (Fin 2 → ℝ) ▶
[] [0.000044s] ✅ apply @CommRing.toRing to Ring (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating CommRing (Fin 2 → ℝ) to subgoal CommRing (Fin 2 → ℝ) of Ring (Fin 2 → ℝ) ▶
[] [0.000048s] ✅ apply @instSemiring to Semiring (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating Ring (Fin 2 → ℝ) to subgoal Ring (Fin 2 → ℝ) of Semiring (Fin 2 → ℝ) ▶
[] [0.000059s] ✅ apply @NonAssocRing.toNonAssocSemiring to NonAssocSemiring (Fin 2 → ℝ) ▶
[] [0.000096s] ✅ apply @Pi.nonAssocRing to NonAssocRing (Fin 2 → ℝ) ▶
[resume] [0.000006s] propagating Fin 2 → NonAssocRing ℝ to subgoal Fin 2 → NonAssocRing ℝ of NonAssocRing (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating NonAssocRing (Fin 2 → ℝ) to subgoal NonAssocRing (Fin 2 → ℝ) of NonAssocSemiring (Fin 2 → ℝ) ▶
[] [0.000052s] ✅ apply @Ring.toNonAssocRing to NonAssocRing (Fin 2 → ℝ) ▶
[resume] [0.000005s] propagating Ring (Fin 2 → ℝ) to subgoal Ring (Fin 2 → ℝ) of NonAssocRing (Fin 2 → ℝ) ▶
[] [0.000063s] ✅ apply @Unique.instSubsingleton to Subsingleton (Fin 2 → ℝ) ▶
[] [0.000112s] ✅ apply @Pi.uniqueOfIsEmpty to Unique (Fin 2 → ℝ) ▶
[] [0.000094s] ✅ apply @Pi.unique to Unique (Fin 2 → ℝ) ▶
[] [0.000054s] ✅ apply @IsEmpty.instSubsingleton to Subsingleton (Fin 2 → ℝ) ▶
[] [0.000098s] ✅ apply @instIsEmptyForAll to IsEmpty (Fin 2 → ℝ) ▶
[resume] [0.000022s] propagating Nonempty (Fin 2) to subgoal Nonempty (Fin 2) of IsEmpty (Fin 2 → ℝ) ▶
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment