Commit 2023-12-17 21:55 2362ccdf

View on Github →

feat: make mod_cases work on Nat, in addition to Int (#3922) The current mod_cases, as implemented in #593, only works on integers. This pull request extends it to also work on natural numbers.

Estimated changes

Modified Mathlib/Tactic/ModCases.lean

added def Mathlib.Tactic.ModCases.IntMod.OnModCases

added def Mathlib.Tactic.ModCases.IntMod.modCases

added def Mathlib.Tactic.ModCases.IntMod.onModCases_start

added def Mathlib.Tactic.ModCases.IntMod.onModCases_stop

added def Mathlib.Tactic.ModCases.IntMod.onModCases_succ

added def Mathlib.Tactic.ModCases.NatMod.OnModCases

added def Mathlib.Tactic.ModCases.NatMod.modCases

added def Mathlib.Tactic.ModCases.NatMod.onModCases_start

added def Mathlib.Tactic.ModCases.NatMod.onModCases_stop

added def Mathlib.Tactic.ModCases.NatMod.onModCases_succ

deleted def Mathlib.Tactic.ModCases.OnModCases

deleted def Mathlib.Tactic.ModCases.onModCases_start

deleted def Mathlib.Tactic.ModCases.onModCases_stop

deleted def Mathlib.Tactic.ModCases.onModCases_succ

Modified test/mod_cases.lean