Weirdness with cutsat

Stream: new members

[Ilmārs Cīrulis]

import Mathlib

theorem T.extracted_1_7 {a : ℕ} (ha : 0 < a) (H : a ^ 2 = 2 ^ a) : a = 4 :=
  have h₁ : a = 1 ∨ a = 2 ∨ 3 ≤ a := by cutsat -- fails
  sorry

If I remove hypothesis H, cutsat works again.

import Mathlib

theorem T.extracted_1_7 {a : ℕ} (ha : 0 < a) : a = 4 :=
  have h₁ : a = 1 ∨ a = 2 ∨ 3 ≤ a := by cutsat
  sorry

[Snir Broshi]

This reproduces on the latest Mathlib nightly (ce00192bf8058fc20bcc4188abf983d16be18ff7)

[Kim Morrison]

Thanks for this report, investigating!