chore: update std4 to b197bd2, catching up to leanprover-community/batteries#427 (#8888)

Co-authored-by: James <jamesgallicchio@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com>

Author: 6 people

Mathlib/Combinatorics/SetFamily/Shadow.lean

@@ -211,7 +211,7 @@ theorem upShadow_monotone : Monotone (upShadow : Finset (Finset α) → Finset (
 
 /-- `t` is in the upper shadow of `𝒜` iff there is a `s ∈ 𝒜` from which we can remove one element
 to get `t`. -/
-lemma mem_upShadow_iff : t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a, a ∉ s ∧ insert a s = t := by
+lemma mem_upShadow_iff : t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t := by
   simp_rw [upShadow, mem_sup, mem_image, mem_compl]
 #align finset.mem_up_shadow_iff Finset.mem_upShadow_iff
 

Mathlib/Data/Finset/Basic.lean

@@ -1230,7 +1230,7 @@ theorem insert_inj_on (s : Finset α) : Set.InjOn (fun a => insert a s) sᶜ :=
   (insert_inj h).1
 #align finset.insert_inj_on Finset.insert_inj_on
 
-theorem ssubset_iff : s ⊂ t ↔ ∃ a, a ∉ s ∧insert a s ⊆ t := mod_cast @Set.ssubset_iff_insert α s t
+theorem ssubset_iff : s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t := mod_cast @Set.ssubset_iff_insert α s t
 #align finset.ssubset_iff Finset.ssubset_iff
 
 theorem ssubset_insert (h : a ∉ s) : s ⊂ insert a s :=

Mathlib/Data/Finset/Grade.lean

@@ -104,13 +104,13 @@ lemma covby_insert (ha : a ∉ s) : s ⋖ insert a s :=
 
 @[simp] lemma erase_covby (ha : a ∈ s) : s.erase a ⋖ s := ⟨erase_ssubset ha, (erase_wcovby _ _).2⟩
 
-lemma _root_.Covby.exists_finset_insert (h : s ⋖ t) : ∃ a, a ∉ s ∧ insert a s = t := by
+lemma _root_.Covby.exists_finset_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t := by
   simpa using h.exists_finset_cons
 
 lemma _root_.Covby.exists_finset_erase (h : s ⋖ t) : ∃ a ∈ t, t.erase a = s := by
   simpa only [← coe_inj, coe_erase] using h.finset_coe.exists_set_sdiff_singleton
 
-lemma covby_iff_exists_insert : s ⋖ t ↔ ∃ a, a ∉ s ∧ insert a s = t := by
+lemma covby_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t := by
   simp only [← coe_covby_coe, Set.covby_iff_exists_insert, ← coe_inj, coe_insert, mem_coe]
 
 lemma covby_iff_card_sdiff_eq_one : t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1 := by

Mathlib/Data/List/Perm.lean

@@ -229,7 +229,6 @@ lemma subperm_iff : l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l := by
   obtain ⟨l', h₂⟩ := h₂.exists_perm_append
   exact ⟨l₁ ++ l', (h₂.trans (h₁.append_right _)).symm, (prefix_append _ _).sublist⟩
 
-
 -- This is now in `Std`, but apparently misnamed as `List.subperm_singleton_iff`.
 lemma singleton_subperm_iff : [a] <+~ l ↔ a ∈ l :=
   ⟨fun ⟨s, hla, h⟩ ↦ by rwa [perm_singleton.1 hla, singleton_sublist] at h,

Mathlib/Data/Set/Basic.lean

@@ -1179,7 +1179,7 @@ theorem subset_insert_iff_of_not_mem (ha : a ∉ s) : s ⊆ insert a t ↔ s ⊆
   forall₂_congr <| fun _ hb => or_iff_right <| ne_of_mem_of_not_mem hb ha
 #align set.subset_insert_iff_of_not_mem Set.subset_insert_iff_of_not_mem
 
-theorem ssubset_iff_insert {s t : Set α} : s ⊂ t ↔ ∃ a, a ∉ s ∧ insert a s ⊆ t := by
+theorem ssubset_iff_insert {s t : Set α} : s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t := by
   simp only [insert_subset_iff, exists_and_right, ssubset_def, not_subset]
   aesop
 #align set.ssubset_iff_insert Set.ssubset_iff_insert

Mathlib/MeasureTheory/Integral/Marginal.lean

@@ -103,9 +103,7 @@ theorem _root_.Measurable.lmarginal (hf : Measurable f) : Measurable (∫⋯∫
 
 /-- The marginal distribution is independent of the variables in `s`. -/
 theorem lmarginal_congr {x y : ∀ i, π i} (f : (∀ i, π i) → ℝ≥0∞)
-    -- TODO: change back from `∀ i, i ∉ s →` to `∀ i ∉ s,` after bumping past
-    -- https://github.com/leanprover/std4/pull/427
-    (h : ∀ i, i ∉ s → x i = y i) :
+    (h : ∀ i ∉ s, x i = y i) :
     (∫⋯∫⁻_s, f ∂μ) x = (∫⋯∫⁻_s, f ∂μ) y := by
   dsimp [lmarginal, updateFinset_def]; rcongr; exact h _ ‹_›
 

Mathlib/Order/Cover.lean

@@ -501,7 +501,7 @@ variable {s t : Set α} {a : α}
 @[simp] lemma sdiff_singleton_covby (ha : a ∈ s) : s \ {a} ⋖ s :=
   ⟨sdiff_lt (singleton_subset_iff.2 ha) $ singleton_ne_empty _, (sdiff_singleton_wcovby _ _).2⟩
 
-lemma _root_.Covby.exists_set_insert (h : s ⋖ t) : ∃ a, a ∉ s ∧ insert a s = t :=
+lemma _root_.Covby.exists_set_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t :=
   let ⟨a, ha, hst⟩ := ssubset_iff_insert.1 h.lt
   ⟨a, ha, (hst.eq_of_not_ssuperset $ h.2 $ ssubset_insert ha).symm⟩
 
@@ -510,7 +510,7 @@ lemma _root_.Covby.exists_set_sdiff_singleton (h : s ⋖ t) : ∃ a ∈ t, t \ {
   ⟨a, ha, (hst.eq_of_not_ssubset fun h' ↦ h.2 h' $
     sdiff_lt (singleton_subset_iff.2 ha) $ singleton_ne_empty _).symm⟩
 
-lemma covby_iff_exists_insert : s ⋖ t ↔ ∃ a, a ∉ s ∧ insert a s = t :=
+lemma covby_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t :=
   ⟨Covby.exists_set_insert, by rintro ⟨a, ha, rfl⟩; exact covby_insert ha⟩
 
 lemma covby_iff_exists_sdiff_singleton : s ⋖ t ↔ ∃ a ∈ t, t \ {a} = s :=

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "63c387daa50f6d651effa5c7cf47647d5424f850",
+   "rev": "b197bd218dbab248ad8899404334d41da04f5d13",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

test/delaborators.lean

@@ -45,11 +45,9 @@ variable (P : Nat → Prop) (α : Nat → Type) (s : Set ℕ)
 #guard_msgs in
 #check ∀ x, x ∈ s → P x
 
--- TODO: uncomment after bumping past
--- https://github.com/leanprover/std4/pull/427
--- /-- info: ∀ x ∉ s, P x : Prop -/
--- #guard_msgs in
--- #check ∀ x ∉ s,P x
+/-- info: ∀ x ∉ s, P x : Prop -/
+#guard_msgs in
+#check ∀ x ∉ s,P x
 
 /-- info: ∀ x ∉ s, P x : Prop -/
 #guard_msgs in
@@ -149,11 +147,9 @@ section existential
 
 variable (s : Set ℕ) (P : ℕ → Prop) (Q : Set ℕ → Prop)
 
--- TODO: uncomment after bumping past
--- https://github.com/leanprover/std4/pull/427
--- /-- info: ∃ x ∉ s, P x : Prop -/
--- #guard_msgs in
--- #check ∃ x ∉ s, P x
+/-- info: ∃ x ∉ s, P x : Prop -/
+#guard_msgs in
+#check ∃ x ∉ s, P x
 
 /-- info: ∃ x ∉ s, P x : Prop -/
 #guard_msgs in