Skip to content

Instantly share code, notes, and snippets.

@alreadydone

alreadydone/covariantClass_le_of_lt-trace.txt

Created August 24, 2023 14:27
Show Gist options
  • Save alreadydone/fc6d4d99f30b2f16ac0610165ffcc3ff to your computer and use it in GitHub Desktop.
Save alreadydone/fc6d4d99f30b2f16ac0610165ffcc3ff to your computer and use it in GitHub Desktop.
Download ZIP
timeout caused by `covariantClass_le_of_lt`
Raw
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment