Commit 2022-10-24 15:16 9efcb950

View on Github →

feat: port Logic/Basic (#484) Two reasons to get this out of the way:

it's at the root of all our (non-tactic) import trees, so blocking almost everything
it's more complicated than most other things, because it contains a partial port of the mathlib3 content, but so does Std4 I've attempted to make sure everything from mathlib3's logic.basic is here, unless it is already in Std4. Additionally I've replaced some definitions with aliases. Thanks for @javra's work on this. Discussion of this PR is ongoing on zulip.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Data/List/Card.lean

Modified Mathlib/Data/List/Pairwise.lean

Modified Mathlib/Data/List/Range.lean

Modified Mathlib/Init/Align.lean

Created Mathlib/Init/Classical.lean

added theorem Classical.cases

added theorem Classical.cases_on

added theorem Classical.cases_true_false

added theorem Classical.eq_false_or_eq_true

Modified Mathlib/Init/Logic.lean

added theorem ExistsUnique.exists

added theorem ExistsUnique.unique

deleted theorem exists_of_exists_unique

deleted theorem unique_of_exists_unique

Modified Mathlib/Logic/Basic.lean

added theorem And.exists

added theorem BAll.imp_left

added theorem BAll.imp_right

added theorem BEx.elim

added theorem BEx.imp_left

added theorem BEx.imp_right

added theorem BEx.intro

deleted theorem Ball.imp_left

deleted theorem Ball.imp_right

added def Classical.choice_of_byContradiction'

added theorem Classical.some_spec₂

modified theorem Decidable.eq_or_ne

modified theorem Decidable.ne_or_eq

added theorem Eq.congr_left

added theorem Eq.congr_right

added theorem Exists.fst

added theorem Exists.snd

added theorem ExistsUnique.elim₂

deleted theorem ExistsUnique.exists

added theorem ExistsUnique.exists₂

added theorem ExistsUnique.intro2

added theorem ExistsUnique.unique2

added theorem Exists₂.imp

added theorem Exists₃.imp

added theorem Fact.elim

added def Function.swap₂

deleted theorem Iff.not

modified theorem Iff.not_left

modified theorem Iff.not_right

added theorem Imp.swap

added theorem Ne.ne_or_ne

modified theorem Or.elim3

added theorem PLift.down_inj

added theorem PLift.down_injective

added theorem ULift.down_inj

added theorem ULift.down_injective

added theorem and_forall_ne

modified theorem and_iff_not_or_not

added theorem apply_dite₂

added theorem apply_ite₂

added theorem ball_and_distrib

added theorem ball_cond_comm

added theorem ball_congr

added theorem ball_mem_comm

added theorem ball_of_forall

added theorem ball_or_left

added theorem ball_true_iff

added theorem bex_congr

added theorem bex_def

added theorem bex_eq_left

added theorem bex_imp

added theorem bex_of_exists

added theorem bex_or

added theorem bex_or_left

modified theorem by_contradiction

added theorem cast_cast

added theorem cast_eq_iff_heq

added theorem congr_arg_heq

added theorem congr_arg_refl

added theorem congr_fun_congr_arg

added theorem congr_fun_rfl

added theorem congr_fun₂

added theorem congr_fun₃

added theorem congr_heq

added theorem congr_refl_left

added theorem congr_refl_right

added theorem dite_apply

added theorem dite_dite_comm

added theorem dite_eq_iff'

added theorem dite_eq_iff

added theorem dite_eq_ite

added theorem dite_eq_left_iff

added theorem dite_eq_or_eq

added theorem dite_eq_right_iff

added theorem dite_ne_left_iff

added theorem dite_ne_right_iff

added theorem eq_equivalence

added theorem eq_iff_eq_cancel_left

added theorem eq_iff_eq_cancel_right

added theorem eq_mp_eq_cast

added theorem eq_mpr_eq_cast

modified theorem eq_or_ne

added theorem eq_true_eq_id

added theorem exists_apply_eq_apply'

added theorem exists_comm

added theorem exists_const

added theorem exists_eq_right'

added theorem exists_exists_and_eq_and

added theorem exists_exists_eq_and

added theorem exists_iff_of_forall

added theorem exists_of_bex

added theorem exists_or_eq_left'

added theorem exists_or_eq_left

added theorem exists_or_eq_right'

added theorem exists_or_eq_right

added theorem exists_prop_congr'

added theorem exists_prop_congr

added theorem exists_prop_of_false

added theorem exists_prop_of_true

added theorem exists_swap

added theorem exists_true_left

added theorem exists_unique_const

added theorem exists_unique_eq'

added theorem exists_unique_eq

added theorem exists_unique_false

added theorem exists_unique_iff_exists

added theorem exists_unique_prop

added theorem exists_unique_prop_of_true

added theorem exists₂_comm

added theorem fact_iff

added theorem forall_apply_eq_imp_iff'

added theorem forall_apply_eq_imp_iff

added theorem forall_apply_eq_imp_iff₂

added theorem forall_eq_apply_imp_iff'

added theorem forall_eq_apply_imp_iff

added theorem forall_exists_index

added theorem forall_imp_iff_exists_imp

added theorem forall_of_ball

added theorem forall_or_distrib_right

added theorem forall_or_left

added theorem forall_or_of_or_forall

added theorem forall_prop_congr'

added theorem forall_prop_congr

added theorem forall_true_iff'

modified theorem forall_true_iff

added theorem forall_true_left

added theorem forall₂_imp

added theorem forall₂_swap

added theorem forall₂_true_iff

added theorem forall₃_imp

added theorem forall₃_true_iff

added theorem funext₂

added theorem funext₃

added theorem heq_of_cast_eq

modified theorem iff_iff_and_or_not_and_not

modified theorem iff_iff_not_or_and_or_not

modified theorem iff_mpr_iff_true_intro

modified theorem iff_not_comm

added theorem imp_forall_iff

modified theorem imp_iff_not_or

added theorem imp_or'

added theorem imp_or

deleted theorem imp_or_distrib'

deleted theorem imp_or_distrib

added theorem ite_and

added theorem ite_apply

added theorem ite_eq_iff'

added theorem ite_eq_iff

added theorem ite_eq_left_iff

added theorem ite_eq_or_eq

added theorem ite_eq_right_iff

added theorem ite_ite_comm

added theorem ite_ne_left_iff

added theorem ite_ne_right_iff

added theorem ne_of_apply_ne

modified theorem ne_or_eq

deleted theorem not_and_distrib

modified theorem not_and_not_right

added theorem not_and_or

added theorem not_ball

added theorem not_ball_of_bex_not

added theorem not_bex

added theorem not_exists_not

modified theorem not_forall

added theorem not_forall_not

modified theorem not_iff

modified theorem not_iff_comm

modified theorem not_iff_not

modified theorem not_imp_comm

modified theorem not_imp_not

modified theorem not_imp_self

modified theorem not_ne_iff

modified theorem not_or_of_imp

added theorem not_xor

modified theorem of_not_imp

deleted theorem or_congr_left'

deleted theorem or_congr_right'

modified theorem or_iff_not_and_not

modified theorem or_iff_not_imp_left

modified theorem or_iff_not_imp_right

added theorem or_not_of_imp

added theorem pi_congr

added theorem rec_heq_of_heq

added theorem xor_iff_not_iff

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/Logic/IsEmpty.lean

Modified Mathlib/Tactic/PushNeg.lean

deleted theorem Mathlib.Tactic.PushNeg.not_and_distrib_eq

added theorem Mathlib.Tactic.PushNeg.not_and_or_eq

modified theorem Mathlib.Tactic.PushNeg.not_or_eq