Commit 2021-05-09 22:49 b4c2d601

View on Github →

feat(Logic/Basic): import init.logic

Estimated changes

Modified Mathlib/Logic/Basic.lean

added def And.elim

added theorem And.imp

added theorem And.symm

added def Decidable.by_cases

added def Decidable.by_contradiction

added def Decidable.not_and

added def Decidable.of_not_not

added theorem Eq.to_iff

added theorem Exists.imp

added theorem Exists.nonempty

added theorem ExistsUnique.exists

added theorem ExistsUnique.intro

added theorem ExistsUnique.unique

added def ExistsUnique

added def Iff.elim

added theorem Ne.def

added def Not.elim

added theorem Not.intro

added def Or.by_cases'

added def Or.by_cases

added theorem Or.elim

added theorem Or.imp

added theorem Or.imp_left

modified theorem Or.imp_right

added theorem Or.neg_resolve_left

added theorem Or.neg_resolve_right

added theorem Or.resolve_left

added theorem Or.resolve_right

modified theorem Or.symm

added theorem and_assoc

added theorem and_comm

added theorem and_congr

added theorem and_congr_right

added theorem and_false

added theorem and_iff_left

added theorem and_iff_right

added theorem and_left_comm

added theorem and_not_self

added theorem and_self

added theorem and_true

added def cast_eq

added def cast_heq

added theorem cast_proof_irrel

added def congr_arg

added def congr_fun

added theorem dif_eq_if

added def dif_neg

added def dif_pos

added theorem eq_comm

added def eq_of_heq

added def eq_rec_heq

added theorem eq_self_iff_true

added theorem exists_congr

added theorem exists_unique_congr

added theorem false_and

added theorem false_iff

added theorem false_imp_iff

added def false_of_ne

added theorem false_or

added theorem forall_congr

added theorem forall_not_of_not_exists

added def heq_of_eq

added def heq_of_eq_of_heq

added theorem heq_of_eq_rec_left

added theorem heq_of_eq_rec_right

added def heq_of_heq_of_eq

added theorem heq_self_iff_true

added theorem if_false

added def if_neg

added def if_pos

added theorem if_true

added theorem iff_comm

added theorem iff_congr

added theorem iff_false

added theorem iff_false_intro

added theorem iff_iff_implies_and_implies

added theorem iff_not_self

added theorem iff_self

added theorem iff_true

added theorem iff_true_intro

added theorem imp_congr

added theorem imp_congr_ctx

added theorem imp_congr_left

added theorem imp_congr_right

added theorem imp_true_iff

added theorem ite_id

added def ne_false_of_self

added theorem ne_self_iff_false

added def ne_true_of_not

added theorem neq_of_not_iff

added theorem not_and_self

added theorem not_congr

added def not_false

added theorem not_false_iff

added theorem not_iff_false_intro

added theorem not_iff_self

added theorem not_not_em

added theorem not_not_intro

added theorem not_not_not

added theorem not_of_eq_false

added theorem not_of_iff_false

added theorem not_or

added theorem not_or_intro

added theorem not_true

added def of_eq_true

added theorem of_heq_true

added theorem of_iff_true

added theorem optParam_eq

modified theorem or_assoc

added theorem or_comm

added theorem or_congr

added theorem or_false

added theorem or_left_comm

added theorem or_self

added theorem or_true

added theorem plift.down_up

added theorem plift.up_down

added structure plift

added def proof_irrel

added theorem true_and

added theorem true_iff

added def true_ne_false

added theorem true_or

added def type_eq_of_heq

added theorem ulift.down_up

added theorem ulift.up_down

added structure ulift.{r,

Modified Mathlib/Tactic/Basic.lean