Commit 2023-11-02 05:05 6f355e37

View on Github →

feat: patch for std4#196 (more min/max lemmas for Nat) (#8074)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Func.lean

Modified Mathlib/Data/Nat/Basic.lean

deleted theorem Nat.max_succ_succ

Modified Mathlib/Data/Nat/Order/Basic.lean

deleted theorem Nat.zero_max

Modified Mathlib/Data/Stream/Init.lean

Modified Mathlib/Init/Data/List/Lemmas.lean

Modified Mathlib/Init/Data/Nat/Lemmas.lean

Modified Mathlib/Tactic/Backtrack.lean

deleted def Lean.MVarId.firstContinuation

deleted def Mathlib.Tactic.ppMVarIds

Modified lake-manifest.json