Zulip Chat Archive

Stream: mathlib4

Topic: how to fix: updating mathlib breaks this code


Asei Inoue (Jan 10 2026 at 12:19):

import Mathlib.Tactic.FinCases

example {n : ℕ} (h : n ∈ ({2, 4, 42} : Finset ℕ)) : 2 ∣ n := by
  fin_cases h
  all_goals decide

Asei Inoue (Jan 10 2026 at 12:20):

After updating Mathlib4, this code no longer works.
How can I fix it?

Vlad Tsyrklevich (Jan 10 2026 at 14:49):

changing the import to import Mathlib fixes it, #min_imports shows the import you now need.

Asei Inoue (Jan 10 2026 at 15:03):

Thank you!!


Last updated: Feb 28 2026 at 14:05 UTC