Feat: add List.perm_replicate_append_replicate (#1509)

This is a forward-port of leanprover-community/mathlib#18126

Also golf a proof.

Mathlib/Data/List/Basic.lean

@@ -329,6 +329,9 @@ theorem exists_mem_cons_iff (p : α → Prop) (a : α) (l : List α) :
 
 /-! ### list subset -/
 
+instance : IsTrans (List α) Subset where
+  trans := fun _ _ _ => List.Subset.trans
+
 #align list.subset_def List.subset_def
 
 #align list.subset_append_of_subset_left List.subset_append_of_subset_left

Mathlib/Data/List/Perm.lean

@@ -87,29 +87,25 @@ instance isSetoid (α) : Setoid (List α) :=
 #align list.is_setoid List.isSetoid
 
 -- Porting note: used rec_on in mathlib3; lean4 eqn compiler still doesn't like it
-theorem Perm.subset {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁ ⊆ l₂ := fun a =>
+theorem Perm.mem_iff {a : α} {l₁ l₂ : List α} (p : l₁ ~ l₂) : a ∈ l₁ ↔ a ∈ l₂ :=
   p.rec
-  (fun h => h)
-  (fun x l₁ l₂ _r hs h => by
-    cases h
-    . apply Mem.head
-    . apply Mem.tail
-      apply hs
-      assumption)
-  (fun x y l h => by
-    match h with
-    | .head _ => exact Mem.tail x (Mem.head l)
-    | .tail _ (.head _) => apply Mem.head
-    | .tail _ (.tail _ h) => exact Mem.tail x (Mem.tail y h))
-  (fun _ _ h₁ h₂ h => by
-    apply h₂
-    apply h₁
-    assumption)
+    Iff.rfl
+    (fun _ _ _ _ hs => by simp only [mem_cons, hs])
+    (fun _ _ _ => by simp only [mem_cons, or_left_comm])
+    (fun _ _ => Iff.trans)
+#align list.perm.mem_iff List.Perm.mem_iff
+
+theorem Perm.subset {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁ ⊆ l₂ :=
+  fun _ => p.mem_iff.mp
 #align list.perm.subset List.Perm.subset
 
-theorem Perm.mem_iff {a : α} {l₁ l₂ : List α} (h : l₁ ~ l₂) : a ∈ l₁ ↔ a ∈ l₂ :=
-  Iff.intro (fun m => h.subset m) fun m => h.symm.subset m
-#align list.perm.mem_iff List.Perm.mem_iff
+theorem Perm.subset_congr_left {l₁ l₂ l₃ : List α} (h : l₁ ~ l₂) : l₁ ⊆ l₃ ↔ l₂ ⊆ l₃ :=
+  ⟨h.symm.subset.trans, h.subset.trans⟩
+#align list.perm.subset_congr_left List.Perm.subset_congr_left
+
+theorem Perm.subset_congr_right {l₁ l₂ l₃ : List α} (h : l₁ ~ l₂) : l₃ ⊆ l₁ ↔ l₃ ⊆ l₂ :=
+  ⟨fun h' => h'.trans h.subset, fun h' => h'.trans h.symm.subset⟩
+#align list.perm.subset_congr_right List.Perm.subset_congr_right
 
 theorem Perm.append_right {l₁ l₂ : List α} (t₁ : List α) (p : l₁ ~ l₂) : l₁ ++ t₁ ~ l₂ ++ t₁ :=
   p.rec
@@ -889,6 +885,15 @@ theorem perm_iff_count {l₁ l₂ : List α} : l₁ ~ l₂ ↔ ∀ a, count a l
       by_cases b = a <;> simp [h] at H⊢ <;> assumption⟩
 #align list.perm_iff_count List.perm_iff_count
 
+theorem perm_replicate_append_replicate {l : List α} {a b : α} {m n : ℕ} (h : a ≠ b) :
+    l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b] := by
+  rw [perm_iff_count, ← Decidable.and_forall_ne a, ← Decidable.and_forall_ne b]
+  suffices : l ⊆ [a, b] ↔ ∀ c, c ≠ b → c ≠ a → c ∉ l
+  { simp (config := { contextual := true }) [count_replicate, h, h.symm, this] }
+  simp_rw [Ne.def, ← and_imp, ← not_or, Decidable.not_imp_not, subset_def, mem_cons,
+    not_mem_nil, or_false, or_comm]
+#align list.perm_replicate_append_replicate List.perm_replicate_append_replicate
+
 theorem Subperm.cons_right {α : Type _} {l l' : List α} (x : α) (h : l <+~ l') : l <+~ x :: l' :=
   h.trans (sublist_cons x l').subperm
 #align list.subperm.cons_right List.Subperm.cons_right

Mathlib/Logic/Basic.lean

@@ -613,8 +613,14 @@ theorem exists_unique_const (α) [i : Nonempty α] [Subsingleton α] :
 #align exists_and_distrib_left exists_and_left
 #align exists_and_distrib_right exists_and_right
 
-theorem and_forall_ne (a : α) : (p a ∧ ∀ (b) (_ : b ≠ a), p b) ↔ ∀ b, p b := by
-  simp only [← @forall_eq _ p a, ← forall_and, ← or_imp, Classical.em, forall_const]
+theorem Decidable.and_forall_ne [DecidableEq α] (a : α) {p : α → Prop} :
+    (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b := by
+  simp only [← @forall_eq _ p a, ← forall_and, ← or_imp, Decidable.em, forall_const]
+#align decidable.and_forall_ne Decidable.and_forall_ne
+
+theorem and_forall_ne (a : α) : (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b :=
+  Decidable.and_forall_ne a
+#align and_forall_ne and_forall_ne
 
 theorem Ne.ne_or_ne {x y : α} (z : α) (h : x ≠ y) : x ≠ z ∨ y ≠ z :=
   not_and_or.1 <| mt (and_imp.2 (· ▸ ·)) h.symm