mathlib4

mathlib4 copied to clipboard

feat(Mathlib/Tactic/PushNeg): implement the `push_neg` tactic

2

This PR implements the `push_neg` tactic. This code is based on https://github.com/leanprover-community/mathlib4/pull/193/ and on the original Lean 3 `push_neg` code. It notably implements a new feature: if `set_option push_neg.use_distrib true`...

dupuisf

Following a suggestion of @digama0 `recover` is implemented as wrapping tactics so that if goals are closed incorrectly they are reopened. Below are examples (test suggested by @gebner). Some code...

siddhartha-gadgil

Lean 3 version: https://github.com/leanprover-community/mathlib/blob/master/src/topology/unit_interval.lean#L148

j-loreaux

feat(Mathlib/Logic/Equiv/LocalEquiv): add the `mfld_set_tac` tactic

3

This PR adds the `mfld_set_tac` tactic. This tactic relies on a custom simp set which mostly contain lemmas about advanced math that is not yet in mathlib4. In the test...

dupuisf

Uncomment some codes marked with 'no function.injective?'

2

casavaca

feat: profunctor optics

2

A port of some of https://hackage.haskell.org/package/profunctor-optics-0.0.2/docs/Data-Profunctor-Optic-Traversal.html Just for fun. ## How should composition work? If anyone has a good idea for how to get optic composition to work smoothly I'd...

EdAyers

Add a nix flake build

9

Adding a nix flake to enable builds and dependency fetching with nix. This has several opinionated choices about structure which can be negotiated.

Anderssorby

gebner

feat: add on_goals tactic

1

This generalizes the `on_goal` tactic to allow targeting multiple goals at once, and it focuses on each of them when calling the given tactic sequence, like `all_goals` but for a...

digama0

feat(Mathlib/Tactic/TypeCheck): add `type_check` tactic

1

Lean 3 version: https://github.com/leanprover-community/lean/blob/master/library/init/meta/interactive.lean#L1664

j-loreaux