mathlib4

mathlib4 copied to clipboard

fix: apply multiple ext-lemmas in a row

1

gebner

From #348: Lean 4 defines `max` and `min` in the prelude, while Lean 3 (as of https://github.com/leanprover-community/lean/pull/609) defines them differently as part of `linear_order`. We will need to figure out...

gebner

chore: port lint-style.py from mathlib

2

Some of these are no longer relevant, but I want to see what works before cleaning up.

kim-em

feat: deriving optics

2

This file defines the `derive_optics T` command where `T` is an inductive datatype. For each constructor `𝑐` of `T` and each field `𝑎 : α` of `𝑐`, this will create...

EdAyers

feat: add commutative diagram widget

2

Adds a widget which displays certain kinds of goals in the language of category theory as commutative diagrams. Currently only squares and triangles are supported, but it should be easy...

Vtec234

`ring` doesn't support negation

1

Currently the implementation of `ring` is incomplete and has no understanding of subtraction or negation: ```lean import Mathlib.Tactic.Ring example (a b : ℤ) : a - b = a +...

digama0

feat(Tactic/ByContra): by_contra' tactic

3

Implementation of `by_contra'`. Note that it needs the (as yet unimplemented) `push_neg`.

kbuzzard

feat: propagate_tags tactic

1

Adds `propagate_tags`

Beanway144

feat: `symm` and `trans` tactics

13

I have implemented a symm tactic, using annotations for symm rules. This follows (including using code from) the ext implementation. I also have a couple of test examples

siddhartha-gadgil

feat: `rename_bvar` tactic

7

arthurpaulino