def foo : Nat

Equations

• foo = 1

theorem test_theorem : 1 + 1 = 2

A highly non-trivial theorem

theorem test_theorem_with_hypothesis : True → 1 + 1 = 2

A highly non-trivial theorem with a helpful hypothesis

theorem test_theorem_with_hypotheses : True → False → 1 + 1 = 2

A highly non-trivial theorem with two helpful hypotheses

theorem test_lemma : 1 + 1 = 2

theorem test_theorem_with_docstring : 1 + 1 = 2

A highly non-trivial theorem with a helpful hypothesis

theorem test_2 : 1 + 1 = 2

@[simp]

theorem test_1 : 1 + 1 = 2

@[simp]

theorem test_3 : 1 + 1 = 2