timeout caused by `covariantClass_le_of_lt`

covariantClass_le_of_lt-trace.txt

Before adding instance `covariantClass_le_of_lt`:

[Elab.command] [1.263200s] set_option profiler true in
    @[simp]
    theorem le_sub_one_iff {n : ℕ} {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 :=
      by
      cases n
      · simp [fin_one_eq_zero k]
      rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
      simp ▼
  [] [1.263039s] @[simp]
      theorem le_sub_one_iff {n : ℕ} {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 :=
        by
        cases n
        · simp [fin_one_eq_zero k]
        rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
        simp ▼
    [step] [0.015018s] expected type: Prop, term
        k ≤ k - 1 ↔ k = 0 ▶
    [step] [1.218654s] 
          cases n
          · simp [fin_one_eq_zero k]
          rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
          simp ▼
      [] [1.218601s] 
            cases n
            · simp [fin_one_eq_zero k]
            rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
            simp ▼
        [] [1.102324s] · simp [fin_one_eq_zero k] ▼
          [] [1.102280s] simp [fin_one_eq_zero k] ▼
            [] [1.102249s] simp [fin_one_eq_zero k] ▼
              [Meta.isDefEq] [0.012751s] ✅ 0 - ?a =?= 0 - 1 ▶
              [Meta.isDefEq] [0.012141s] ✅ 0 ≤ -?a =?= 0 ≤ -1 ▶
              [Meta.synthInstance] [0.594885s] ❌ CovariantClass (Fin (0 + 1)) (Fin (0 + 1)) (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▼
                [] [0.395171s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                      (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                [] [0.199529s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                      (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
              [Meta.synthInstance] [0.442868s] ❌ CovariantClass (Fin (0 + 1)) (Fin (0 + 1)) (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▼
                [] [0.364257s] ❌ apply OrderedAddCommMonoid.to_covariantClass_right to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                      (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                [] [0.025669s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                      (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                [] [0.021067s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                      (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                [] [0.021483s] ❌ apply covariant_swap_mul_le_of_covariant_mul_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                      (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
        [] [0.036886s] rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add] ▶
        [] [0.077574s] simp ▶
    [Kernel] [0.013276s] typechecking declaration 




After adding instance `covariantClass_le_of_lt`:

[Elab.command] [2.857197s] set_option profiler true in
    set_option synthInstance.maxHeartbeats 30000 in
    @[simp]
    theorem le_sub_one_iff {n : ℕ} {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 :=
      by
      cases n
      · simp [fin_one_eq_zero k]
      rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
      simp ▼
  [] [2.856683s] set_option synthInstance.maxHeartbeats 30000 in
      @[simp]
      theorem le_sub_one_iff {n : ℕ} {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 :=
        by
        cases n
        · simp [fin_one_eq_zero k]
        rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
        simp ▼
    [] [2.856592s] @[simp]
        theorem le_sub_one_iff {n : ℕ} {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 :=
          by
          cases n
          · simp [fin_one_eq_zero k]
          rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
          simp ▼
      [step] [2.830603s] 
            cases n
            · simp [fin_one_eq_zero k]
            rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
            simp ▼
        [] [2.830571s]   cases n
              · simp [fin_one_eq_zero k]
              rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add]
              simp ▼
          [] [2.781289s] · simp [fin_one_eq_zero k] ▼
            [] [2.781265s] simp [fin_one_eq_zero k] ▼
              [] [2.781249s] simp [fin_one_eq_zero k] ▼
                [Meta.synthInstance] [0.987670s] ❌ CovariantClass (Fin (0 + 1)) (Fin (0 + 1)) (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▼
                  [] [0.175717s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.088875s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.187840s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.084045s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.083262s] ❌ apply OrderedCancelAddCommMonoid.to_contravariantClass_left to ContravariantClass (Fin (0 + 1))
                        (Fin (0 + 1)) (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x < x_1 ▶
                  [] [0.184647s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.080370s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.087082s] ❌ apply @OrderedCancelAddCommMonoid.to_contravariantClass_le_left to ContravariantClass (Fin (0 + 1))
                        (Fin (0 + 1)) (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                [Meta.synthInstance] [1.763387s] ❌ CovariantClass (Fin (0 + 1)) (Fin (0 + 1)) (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▼
                  [] [0.172362s] ❌ apply OrderedAddCommMonoid.to_covariantClass_right to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.184068s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.089618s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.197193s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.089811s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.090304s] ❌ apply OrderedCancelAddCommMonoid.to_contravariantClass_left to ContravariantClass (Fin (0 + 1))
                        (Fin (0 + 1)) (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x < x_1 ▶
                  [] [0.251746s] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.080354s] ❌ apply OrderedAddCommMonoid.to_covariantClass_left to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.080917s] ❌ apply @OrderedCancelAddCommMonoid.to_contravariantClass_le_left to ContravariantClass (Fin (0 + 1))
                        (Fin (0 + 1)) (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.160366s] ❌ apply OrderedAddCommMonoid.to_covariantClass_right to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
                  [] [0.160543s] ❌ apply OrderedCancelAddCommMonoid.to_contravariantClass_right to ContravariantClass (Fin (0 + 1))
                        (Fin (0 + 1)) (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x < x_1 ▶
                  [] [0.161802s] ❌ apply OrderedAddCommMonoid.to_covariantClass_right to CovariantClass (Fin (0 + 1)) (Fin (0 + 1))
                        (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1 ▶
          [] [0.016301s] rw [← lt_sub_one_iff, le_iff_lt_or_eq, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm, sub_eq_iff_eq_add] ▶
          [] [0.032326s] simp