mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
This PR implements `fin_cases` from mathlib3. It largely follows the original idea behind Scott's code. There are a few notable details for this PR - To have `fin_cases`s full functionality,...
Added the substs tactic, which just applies subst to multiple hypotheses at once. This is my first PR to mathlib; let me know what needs to change!
`norm_num` needs to support - ``, `≠` - Ring operations: `Neg`, `Sub`, `%` - Field operations: `/`, `⁻¹` - Reals and rationals
This isn't ready to be merged yet. I'm going to port `data.bool.basic` and improve those instances, which are necessary for the mathlib test case. Looking for comments on my implementation!
The notation for `abs` clashes with some variants of the match notation: ``` import Mathbin.Algebra.Abs -- works if this is not imported def test : Nat → Nat | 0...
We've recently changed `classical` in mathlib to so that it no longer overrides the existing decidable instances. mathlib4 should be adapterd. https://github.com/leanprover-community/mathlib/pull/14122 ```lean import Mathlib.Tactic.Basic example : (by classical; exact...
The `∉` precedence was wrong: https://github.com/leanprover-community/mathlib3port/commit/d3886c253aee234456e6ee149c6a1bea9570c689#r67303397 Other notation probably have the wrong precedence as well.
I've got an Abel tactic working, but just for groups and not monoids right now. The comments are all horrible because I cut and pasted the `ring` tactic and adapted...
