And here is another short and simple example of some Agda code (Did you know you can open modules in a type signature‽):

    -- An element has at most one two-sided inverse.
    inverse-unique : ∀ (M : Monoid) (open Reasoning M)
                       (x y z : type M)
                   → y ⋆ x ＝ unit M
                   → x ⋆ z ＝ unit M
                   → y ＝ z
    inverse-unique M x y z leftInverse rightInverse =
      begin
        y                ⟪ sym (unitᵣAt y)           ⟫
        y ⋆ unit M       ⟪ mapᵣ (sym rightInverse)   ⟫
        y ⋆ (x ⋆ z)      ⟪ sym (associativeAt y x z) ⟫
        (y ⋆ x) ⋆ z      ⟪ mapₗ leftInverse          ⟫
        unit M ⋆ z       ⟪ unitₗAt z                 ⟫
        z
      ∎
      where open Reasoning M

Not sure if all the unicode characters will render on HN, but the things left of the ⟪ ⟫-brackets is exactly what a text book in mathematics will have. While the things inside the brackets are just a functional-programming way of saying out the argument which would be left for the reader to make in their head for why each step holds.

(If you know Agda, I dare you to look carefully at this example!)