Commit 2024-08-15 12:19 ebc084f3

View on Github →

chore: cleanup in Mathlib/Init/* (#15188) This moves some content out of Init, deprecates some material that was ported from Lean 3 but is used nowhere, and removes some attributes and instances which are duplicated from Lean or Batteries.

Estimated changes

added theorem List.le_eq_not_gt
added def List.getLastI
added def List.headI
added theorem List.headI_cons
added theorem List.headI_nil
added def Prod.mk.injArrow
added def Combinator.I
added def Combinator.K
added def Combinator.S
deleted theorem Classical.cases
deleted theorem Classical.cases_on
deleted def Combinator.I
deleted def Combinator.K
deleted def Combinator.S
deleted def PProd.mk.injArrow
deleted def Prod.mk.injArrow
deleted def List.getLastI
deleted def List.headI
deleted theorem List.headI_cons
deleted theorem List.headI_nil
deleted theorem List.le_eq_not_gt
modified theorem Nat.eq_zero_of_mul_eq_zero
deleted theorem ex_of_psig
deleted theorem PSigma.lex_wf
deleted theorem PSigma.revLex_wf
deleted theorem PSigma.skipLeft_wf
added theorem Classical.cases
added theorem Classical.cases_on
added theorem WellFounded.psigma_lex