Frédéric Dupuis

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`...

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...

feat(ContinuousFunctionalCalculus): Define the real log based on the CFC

1

This PR defines `CFC.log` as `cfc Real.log`, and shows its basic properties, such as the fact that it's the inverse of `NormedSpace.exp ℝ`. Along the way, we also show that...