Commit 2022-08-09 19:13 148380a4

View on Github →

port some lemmas for use in fin_cases (#350) Ports mem_cons_iff and forall_eq_or_imp, to be used in the proof of Chain.Pairwise in https://github.com/leanprover-community/mathlib4/pull/346.

Estimated changes

Modified Mathlib/Init/Data/List/Lemmas.lean

added theorem List.mem_cons_iff

Modified Mathlib/Logic/Basic.lean

added theorem forall_eq_or_imp