Commit 2024-07-21 18:57 1f79bd05

View on Github →

chore(Mathlib/Init/Meta/WellFoundedTactic): remove Mathlib.Init.Meta.WellFoundedTactic (#14980)

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Init/Meta/WellFoundedTactics.lean

deleted theorem Nat.lt_add_of_zero_lt_left

deleted theorem Nat.zero_lt_one_add