Commit 2026-02-13 18:17 d5bbce85

View on Github →

chore(Logic/IsEmpty): split file into Defs and Basic (#35137) This PR decreases the imports of the congr! and convert tactics by splitting Mathlib.Logic.IsEmpty into a Defs and a Basic file. Then, these tactics can import the Defs file which itself only imports Mathlib.Init. This reduces the longest pole.

Estimated changes

deleted theorem IsEmpty.exists_iff
deleted theorem IsEmpty.forall_iff
deleted theorem Subtype.isEmpty_of_false
deleted theorem biTotal_empty
deleted theorem biTotal_iff_isEmpty_left
deleted theorem biTotal_iff_isEmpty_right
deleted def isEmptyElim
deleted theorem isEmpty_Prop
deleted theorem isEmpty_fun
deleted theorem isEmpty_iff
deleted theorem isEmpty_or_nonempty
deleted theorem isEmpty_pi
deleted theorem isEmpty_plift
deleted theorem isEmpty_pprod
deleted theorem isEmpty_prod
deleted theorem isEmpty_psigma
deleted theorem isEmpty_psum
deleted theorem isEmpty_sigma
deleted theorem isEmpty_subtype
deleted theorem isEmpty_sum
deleted theorem isEmpty_ulift
deleted theorem leftTotal_empty
deleted theorem nonempty_fun
deleted theorem not_isEmpty_iff
deleted theorem not_isEmpty_of_nonempty
deleted theorem not_nonempty_iff
deleted theorem rightTotal_empty
deleted theorem wellFounded_of_isEmpty
added theorem biTotal_empty
added theorem isEmpty_Prop
added theorem isEmpty_fun
added theorem isEmpty_or_nonempty
added theorem isEmpty_pi
added theorem isEmpty_plift
added theorem isEmpty_pprod
added theorem isEmpty_prod
added theorem isEmpty_psigma
added theorem isEmpty_psum
added theorem isEmpty_sigma
added theorem isEmpty_subtype
added theorem isEmpty_sum
added theorem isEmpty_ulift
added theorem leftTotal_empty
added theorem nonempty_fun
added theorem not_isEmpty_iff
added theorem not_nonempty_iff
added theorem rightTotal_empty
added theorem wellFounded_of_isEmpty
added theorem IsEmpty.exists_iff
added theorem IsEmpty.forall_iff
added def isEmptyElim
added theorem isEmpty_iff