  * remove obsolete IsAssociative and IsCommutative

  * Fix "group" and other type class inheritance in lecture 13

  * Look for Prod.fst and Prod.snd and use this syntax for comprenehsions:
    {(s, t) | t = s[x ↦ a s]}

  * Use "proof animation" stuff? (Link posted by Henrik Böving.)

  * Use notation instead of macro for Hoare logic? And State? This way, I
    wouldn't lose our notations. Or use app_unexpander.

  * set_option linter.unusedVariables

  * 'sorry' instead of '_' when building terms/proofs?

  * thank Henrik Böving

  * In Exercice Sheet - Chapter 3 - 2.3:
    Swap the theorem statement to `add (mul n l) (mul n m) = mul (add l m) n`
    (or something similar) so that we actually need to specify which
    multiplication instance we want to rewrite.

  * head_head_cases and head_head_match don't need "cases"/"match", they go
    through with "rfl"

  * "Since the first argument, \li{m}, remains unchanged in the recursive call,
     \li{power m n}," is not accurate. Parameters can change in recursive calls.

  * Change the palindrome non-example (the one with "[x] ++ ys ++ [x]" on the
    LHS of a recursive function) now that Lean 4 allows nonpatterns.

  * Change the dependently typed "match n, ..." example with column of "_"'s now
    that this is no longer necessary in Lean 4.

  * Get rid of Set.ext, since Aesop does it.

  * Get rid of unhygienic option

  * Comments from Böving:

    I can go through all of them and look at what strikes me first but:

    https://github.com/lean-forward/logical_verification_2024/blob/main/lean/LoV
    e/LoVe01_TypesAndTerms_Demo.lean#L87 of course we would want to have
    hygiene enabled as it is one of the selling points vs systems like coq in
    terms of proof stability. Disabling autoImplicit is okay, mathlib does this
    too

    Yes sticking to mathlib naming conventions would be good, I've talked to
    Xavier and he seems to know that some of your lemmas have the "wrong name"
    so he can probably help with that

    The indentation conventions here are wrong:
    https://github.com/lean-forward/logical_verification_2024/blob/main/lean/LoV
    e/LoVe02_ProgramsAndTheorems_Demo.lean#L209-L211 refer to:
    https://leanprover-community.github.io/contribute/style.html
    https://github.com/lean-forward/logical_verification_2024/blob/main/lean/LoV
    e/LoVe03_BackwardProofs_Demo.lean#L185-L190 the syntax { } for addressing
    individual subgoals is outdated. We use the Coq dot, Xavier also knows
    about this

    this instance syntax is also outdated, we'd write it with the where syntax.

    The metaprogramming style is definitely not how most things would be
    written in practice. In general real tactics :tm: basically try to jump out
    of TacticM into MetaM as quickly as possible and tend to only provide a
    thing TacticM wrapper. However I think for educational purposes doing it
    like this can be perfectly fine.
