"or" symbol instead of "and" in an example in Section 3[Typo]

[anton-mellit]

theorem onePlusOneAndLessThan : 1 + 1 = 2 ∨ 3 < 5 := by simp

[anton-mellit]

Actually, replacing ∨ by ∧ gives me "unsolved goals ⊢ 3 < 5". Also trying to prove only 3<5 gives "simp made no progress". Is this a bug? I tried by trivial instead of by simp and it worked.

[david-christiansen]

Thanks - I'll fix this on my next pass through, where I'll need to do a pretty big update to the structure of this section anyway due to various Lean changes.