Commit 2022-09-23 02:45 492d30e0

View on Github →

feat: minimal port of Fintype (#429) This is a bare minimum port of the definitions of Finset / Multiset / Fintype. I am hoping that these are enough to port the fin_cases tactic. (i.e. replacing the unfinished work in #346, which still had sorries in the corresponding material) Where possible I have started by copying and pasting the output from mathlib3port.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Basic.lean

added theorem Finset.mem_def

added structure Finset

Created Mathlib/Data/Fintype/Basic.lean

added theorem Finset.mem_univ

added def Finset.univ

Modified Mathlib/Data/List/Basic.lean

added theorem List.mem_split

Created Mathlib/Data/List/Pairwise.lean

added theorem List.pairwise_append

added theorem List.pairwise_append_comm

added theorem List.pairwise_middle

Modified Mathlib/Data/List/Perm.lean

added theorem List.Perm.cons_inv

added theorem List.Perm.eq_nil

added theorem List.Perm.length_eq

added theorem List.Perm.mem_iff

added theorem List.Perm.nil_eq

added theorem List.Perm.nodup_iff

added theorem List.Perm.pairwise_iff

added theorem List.perm_induction_on

added theorem List.perm_inv_core

Created Mathlib/Data/Multiset/Basic.lean

added def Mem

added def Multiset

Created Mathlib/Data/Multiset/Nodup.lean

added def Multiset.Nodup

Modified Mathlib/Logic/Basic.lean

added theorem forall_prop_of_false

added theorem forall_true_iff