Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-25 15:43 85b5d5cb

View on Github →

refactor(logic/basic): turn prop_of into congr lemma (#6406) Alternative solution to the exists part of #6404.

Estimated changes

added theorem exists_false_left
added theorem exists_prop_congr'
added theorem exists_prop_congr
modified theorem exists_prop_of_false
modified theorem exists_prop_of_true
added theorem exists_true_left
added theorem forall_false_left
added theorem forall_prop_congr'
added theorem forall_prop_congr
modified theorem forall_prop_of_false
modified theorem forall_prop_of_true
added theorem forall_true_left