chore(Data/S*): process a batch of porting notes (#22765)

Author: jcommelin

Mathlib/Data/Semiquot.lean

@@ -22,7 +22,6 @@ predicate `S`) but are not completely determined.
   of the set `s`. The specific element of `s` that the VM computes
   is hidden by a quotient construction, allowing for the representation
   of nondeterministic functions. -/
-  -- Porting note: removed universe parameter
 structure Semiquot (α : Type*) where mk' ::
   /-- Set containing some element of `α` -/
   s : Set α

Mathlib/Data/Seq/Computation.lean

@@ -35,7 +35,6 @@ variable {α : Type u} {β : Type v} {γ : Type w}
 
 -- constructors
 /-- `pure a` is the computation that immediately terminates with result `a`. -/
--- Porting note: `return` is reserved, so changed to `pure`
 def pure (a : α) : Computation α :=
   ⟨Stream'.const (some a), fun _ _ => id⟩
 
@@ -323,6 +322,10 @@ theorem ret_mem (a : α) : a ∈ pure a :=
 theorem eq_of_pure_mem {a a' : α} (h : a' ∈ pure a) : a' = a :=
   mem_unique h (ret_mem _)
 
+@[simp]
+theorem mem_pure_iff (a b : α) : a ∈ pure b ↔ a = b :=
+  ⟨eq_of_pure_mem, fun h => h ▸ ret_mem _⟩
+
 instance ret_terminates (a : α) : Terminates (pure a) :=
   terminates_of_mem (ret_mem _)
 
@@ -628,16 +631,9 @@ theorem bind_pure (f : α → β) (s) : bind s (pure ∘ f) = map f s := by
       · simpa using Or.inr ⟨s, rfl, rfl⟩
   · exact Or.inr ⟨s, rfl, rfl⟩
 
--- Porting note: used to use `rw [bind_pure]`
 @[simp]
 theorem bind_pure' (s : Computation α) : bind s pure = s := by
-  apply eq_of_bisim fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s
-  · intro c₁ c₂ h
-    match c₁, c₂, h with
-    | _, c₂, Or.inl (Eq.refl _) => rcases destruct c₂ with b | cb <;> simp
-    | _, _, Or.inr ⟨s, rfl, rfl⟩ =>
-      apply recOn s <;> intro s <;> simp
-  · exact Or.inr ⟨s, rfl, rfl⟩
+  simpa using bind_pure id s
 
 @[simp]
 theorem bind_assoc (s : Computation α) (f : α → Computation β) (g : β → Computation γ) :
@@ -781,21 +777,18 @@ instance instAlternativeComputation : Alternative Computation :=
     orElse := @orElse
     failure := @empty }
 
--- Porting note: Added unfolds as the code does not work without it
 @[simp]
 theorem ret_orElse (a : α) (c₂ : Computation α) : (pure a <|> c₂) = pure a :=
   destruct_eq_pure <| by
     unfold_projs
     simp [orElse]
 
--- Porting note: Added unfolds as the code does not work without it
 @[simp]
 theorem orElse_pure (c₁ : Computation α) (a : α) : (think c₁ <|> pure a) = pure a :=
   destruct_eq_pure <| by
     unfold_projs
     simp [orElse]
 
--- Porting note: Added unfolds as the code does not work without it
 @[simp]
 theorem orElse_think (c₁ c₂ : Computation α) : (think c₁ <|> think c₂) = think (c₁ <|> c₂) :=
   destruct_eq_think <| by
@@ -995,13 +988,9 @@ theorem liftRel_pure_left (R : α → β → Prop) (a : α) (cb : Computation β
 theorem liftRel_pure_right (R : α → β → Prop) (ca : Computation α) (b : β) :
     LiftRel R ca (pure b) ↔ ∃ a, a ∈ ca ∧ R a b := by rw [LiftRel.swap, liftRel_pure_left]
 
--- Porting note: `simpNF` wants to simplify based on `liftRel_pure_right` but point is to prove
--- a general invariant on `LiftRel`
-@[simp, nolint simpNF]
 theorem liftRel_pure (R : α → β → Prop) (a : α) (b : β) :
     LiftRel R (pure a) (pure b) ↔ R a b := by
-  rw [liftRel_pure_left]
-  exact ⟨fun ⟨b', mb', ab'⟩ => by rwa [eq_of_pure_mem mb'] at ab', fun ab => ⟨_, ret_mem _, ab⟩⟩
+  simp
 
 @[simp]
 theorem liftRel_think_left (R : α → β → Prop) (ca : Computation α) (cb : Computation β) :
@@ -1028,15 +1017,8 @@ theorem liftRel_congr {R : α → β → Prop} {ca ca' : Computation α} {cb cb'
 theorem liftRel_map {δ} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α}
     {s2 : Computation β} {f1 : α → γ} {f2 : β → δ} (h1 : LiftRel R s1 s2)
     (h2 : ∀ {a b}, R a b → S (f1 a) (f2 b)) : LiftRel S (map f1 s1) (map f2 s2) := by
-  -- Porting note: The line below was:
-  -- rw [← bind_pure, ← bind_pure]; apply lift_rel_bind _ _ h1; simp; exact @h2
-  --
-  -- The code fails to work on the last exact.
-  rw [← bind_pure, ← bind_pure]; apply liftRel_bind _ _ h1
-  simp only [comp_apply, liftRel_pure_right]
-  intros a b h; exact ⟨f1 a, ⟨ret_mem _, @h2 a b h⟩⟩
+  rw [← bind_pure, ← bind_pure]; apply liftRel_bind _ _ h1; simp; exact @h2
 
--- Porting note: deleted initial arguments `(_R : α → α → Prop) (_S : β → β → Prop)`: unused
 theorem map_congr {s1 s2 : Computation α} {f : α → β}
     (h1 : s1 ~ s2) : map f s1 ~ map f s2 := by
   rw [← lift_eq_iff_equiv]
@@ -1052,9 +1034,6 @@ def LiftRelAux (R : α → β → Prop) (C : Computation α → Computation β 
 
 variable {R : α → β → Prop} {C : Computation α → Computation β → Prop}
 
--- Porting note: was attribute [simp] LiftRelAux
--- but right now `simp` on defs is a Lean 4 catastrophe
--- Instead we add the equation lemmas and tag them @[simp]
 @[simp] lemma liftRelAux_inl_inl {a : α} {b : β} :
   LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b := rfl
 @[simp] lemma liftRelAux_inl_inr {a : α} {cb} :

Mathlib/Data/Seq/Parallel.lean

@@ -60,7 +60,6 @@ theorem terminates_parallel.aux :
       simp only [parallel.aux1, rmap, corec_eq]
       rw [e]
     rw [this]
-    -- Porting note: This line is required.
     exact ret_terminates a
   intro l S c m T
   revert l S

Mathlib/Data/Seq/Seq.lean

@@ -1255,11 +1255,7 @@ theorem join_map_ret (s : Seq α) : Seq.join (Seq.map ret s) = s := by
 
 @[simp]
 theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s
-  | ⟨a, s⟩ => by
-    dsimp [bind, map]
-    -- Porting note: Was `rw [map_comp]; simp [Function.comp, ret]`
-    rw [map_comp, ret]
-    simp
+  | ⟨a, s⟩ => by simp [bind, map, map_comp, ret]
 
 @[simp]
 theorem ret_bind (a : α) (f : α → Seq1 β) : bind (ret a) f = f a := by
@@ -1317,7 +1313,6 @@ theorem join_join (SS : Seq (Seq1 (Seq1 α))) :
 theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) :
     bind (bind s f) g = bind s fun x : α => bind (f x) g := by
   obtain ⟨a, s⟩ := s
-  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [bind, map]`.
   simp only [bind, map_pair, map_join]
   rw [← map_comp]
   simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]

Mathlib/Data/Seq/WSeq.lean

@@ -453,7 +453,6 @@ theorem liftRel_destruct_iff {R : α → β → Prop} {s : WSeq α} {t : WSeq β
       intro s t
       apply Or.inl⟩⟩
 
--- Porting note: To avoid ambiguous notation, `~` became `~ʷ`.
 @[inherit_doc] infixl:50 " ~ʷ " => Equiv
 
 theorem destruct_congr {s t : WSeq α} :
@@ -851,10 +850,7 @@ theorem mem_of_mem_dropn {s : WSeq α} {a} : ∀ {n}, a ∈ drop s n → a ∈ s
 
 theorem get?_mem {s : WSeq α} {a n} : some a ∈ get? s n → a ∈ s := by
   revert s; induction' n with n IH <;> intro s h
-  · -- Porting note: This line is required to infer metavariables in
-    --               `Computation.exists_of_mem_map`.
-    dsimp only [get?, head] at h
-    rcases Computation.exists_of_mem_map h with ⟨o, h1, h2⟩
+  · rcases Computation.exists_of_mem_map h with ⟨o, h1, h2⟩
     rcases o with - | o
     · injection h2
     injection h2 with h'
@@ -904,17 +900,12 @@ theorem liftRel_dropn_destruct {R : α → β → Prop} {s t} (H : LiftRel R s t
     · apply liftRel_dropn_destruct H n
     exact fun {a b} o =>
       match a, b, o with
-      | none, none, _ => by
-        -- Porting note: These 2 theorems should be excluded.
-        simp [-liftRel_pure_left, -liftRel_pure_right]
+      | none, none, _ => by simp
       | some (a, s), some (b, t), ⟨_, h2⟩ => by simpa [tail.aux] using liftRel_destruct h2
 
 theorem exists_of_liftRel_left {R : α → β → Prop} {s t} (H : LiftRel R s t) {a} (h : a ∈ s) :
     ∃ b, b ∈ t ∧ R a b := by
   let ⟨n, h⟩ := exists_get?_of_mem h
-  -- Porting note: This line is required to infer metavariables in
-  --               `Computation.exists_of_mem_map`.
-  dsimp only [get?, head] at h
   let ⟨some (_, s'), sd, rfl⟩ := Computation.exists_of_mem_map h
   let ⟨some (b, t'), td, ⟨ab, _⟩⟩ := (liftRel_dropn_destruct H n).left sd
   exact ⟨b, get?_mem (Computation.mem_map (Prod.fst.{v, v} <$> ·) td), ab⟩
@@ -942,16 +933,12 @@ theorem exists_of_mem_map {f} {b : β} : ∀ {s : WSeq α}, b ∈ map f s → 
 
 @[simp]
 theorem liftRel_nil (R : α → β → Prop) : LiftRel R nil nil := by
-  rw [liftRel_destruct_iff]
-  -- Porting note: These 2 theorems should be excluded.
-  simp [-liftRel_pure_left, -liftRel_pure_right]
+  simp [liftRel_destruct_iff]
 
 @[simp]
 theorem liftRel_cons (R : α → β → Prop) (a b s t) :
     LiftRel R (cons a s) (cons b t) ↔ R a b ∧ LiftRel R s t := by
-  rw [liftRel_destruct_iff]
-  -- Porting note: These 2 theorems should be excluded.
-  simp [-liftRel_pure_left, -liftRel_pure_right]
+  simp [liftRel_destruct_iff]
 
 @[simp]
 theorem liftRel_think_left (R : α → β → Prop) (s t) : LiftRel R (think s) t ↔ LiftRel R s t := by
@@ -1005,9 +992,7 @@ theorem liftRel_flatten {R : α → β → Prop} {c1 : Computation (WSeq α)} {c
       simp only [destruct_flatten]; apply liftRel_bind _ _ h
       intro a b ab; apply Computation.LiftRel.imp _ _ _ (liftRel_destruct ab)
       intro a b; apply LiftRelO.imp_right
-      intro s t h; refine ⟨Computation.pure s, Computation.pure t, ?_, ?_, ?_⟩ <;>
-        -- Porting note: These 2 theorems should be excluded.
-        simp [h, -liftRel_pure_left, -liftRel_pure_right]⟩
+      intro s t h; refine ⟨Computation.pure s, Computation.pure t, ?_, ?_, ?_⟩ <;> simp [h]⟩
 
 theorem flatten_congr {c1 c2 : Computation (WSeq α)} :
     Computation.LiftRel Equiv c1 c2 → flatten c1 ~ʷ flatten c2 :=
@@ -1273,12 +1258,8 @@ theorem exists_of_mem_join {a : α} : ∀ {S : WSeq (WSeq α)}, a ∈ join S →
       intro ej m <;> simp at ej <;> have := congr_arg Seq.destruct ej <;> simp at this <;>
       subst ss
     · apply Or.inr
-      -- Porting note: `exists_eq_or_imp` should be excluded.
-      simp [-exists_eq_or_imp] at m ⊢
-      rcases IH s S rfl m with as | ex
-      · exact ⟨s, Or.inl rfl, as⟩
-      · rcases ex with ⟨s', sS, as⟩
-        exact ⟨s', Or.inr sS, as⟩
+      simp only [join_cons, nil_append, mem_think, mem_cons_iff, exists_eq_or_imp] at m ⊢
+      exact IH s S rfl m
     · apply Or.inr
       simp? at m says simp only [join_think, nil_append, mem_think] at m
       rcases (IH nil S (by simp) (by simp [m])).resolve_left (not_mem_nil _) with ⟨s, sS, as⟩
@@ -1390,8 +1371,7 @@ theorem liftRel_append (R : α → β → Prop) {s1 s2 : WSeq α} {t1 t2 : WSeq
       · cases a; cases h
       · obtain ⟨a, s⟩ := a; obtain ⟨b, t⟩ := b
         obtain ⟨r, h⟩ := h
-        -- Porting note: These 2 theorems should be excluded.
-        simpa [-liftRel_pure_left, -liftRel_pure_right] using ⟨r, Or.inr ⟨s, rfl, t, rfl, h⟩⟩⟩
+        simpa using ⟨r, Or.inr ⟨s, rfl, t, rfl, h⟩⟩⟩
 
 theorem liftRel_join.lem (R : α → β → Prop) {S T} {U : WSeq α → WSeq β → Prop}
     (ST : LiftRel (LiftRel R) S T)
@@ -1455,8 +1435,7 @@ theorem liftRel_join (R : α → β → Prop) {S : WSeq (WSeq α)} {T : WSeq (WS
     exact fun {o p} h =>
       match o, p, h with
       | some (a, s), some (b, t), ⟨h1, h2⟩ => by
-        -- Porting note: These 2 theorems should be excluded.
-        simpa [-liftRel_pure_left, -liftRel_pure_right] using ⟨h1, s, t, S, rfl, T, rfl, h2, ST⟩
+        simpa using ⟨h1, s, t, S, rfl, T, rfl, h2, ST⟩
       | none, none, _ => by
         -- Porting note: `LiftRelO` should be excluded.
         dsimp [destruct_append.aux, Computation.LiftRel, -LiftRelO]; constructor
@@ -1495,13 +1474,10 @@ theorem join_map_ret (s : WSeq α) : join (map ret s) ~ʷ s := by
       match c1, c2, h with
       | _, _, ⟨s, rfl, rfl⟩ => by
         clear h
-        -- Porting note: `ret` is simplified in `simp` so `ret`s become `fun a => cons a nil` here.
-        have : ∀ s, ∃ s' : WSeq α,
-            (map (fun a => cons a nil) s).join.destruct =
-              (map (fun a => cons a nil) s').join.destruct ∧ destruct s = s'.destruct :=
-          fun s => ⟨s, rfl, rfl⟩
-        induction' s using WSeq.recOn with a s s <;>
-          simp (config := { unfoldPartialApp := true }) [ret, ret_mem, this, Option.exists]
+        have (s) : ∃ s' : WSeq α,
+            (map ret s).join.destruct = (map ret s').join.destruct ∧ destruct s = s'.destruct :=
+          ⟨s, rfl, rfl⟩
+        induction' s using WSeq.recOn with a s s <;> simp [ret, ret_mem, this, Option.exists]
   · exact ⟨s, rfl, rfl⟩
 
 @[simp]
@@ -1619,4 +1595,4 @@ end WSeq
 
 end Stream'
 
-set_option linter.style.longFile 1800
+set_option linter.style.longFile 1700

Mathlib/Data/Set/Enumerate.lean

@@ -25,7 +25,6 @@ namespace Set
 
 section Enumerate
 
-/- Porting note: The original used parameters -/
 variable {α : Type*} (sel : Set α → Option α)
 
 /-- Given a choice function `sel`, enumerates the elements of a set in the order
@@ -69,32 +68,22 @@ theorem enumerate_mem (h_sel : ∀ s a, sel s = some a → a ∈ s) :
 
 theorem enumerate_inj {n₁ n₂ : ℕ} {a : α} {s : Set α} (h_sel : ∀ s a, sel s = some a → a ∈ s)
     (h₁ : enumerate sel s n₁ = some a) (h₂ : enumerate sel s n₂ = some a) : n₁ = n₂ := by
-  /- Porting note: The `rcase, on_goal, all_goals` has been used instead of
-     the not-yet-ported `wlog` -/
-  rcases le_total n₁ n₂ with (hn|hn)
-  on_goal 2 => swap_var n₁ ↔ n₂, h₁ ↔ h₂
-  all_goals
-    rcases Nat.le.dest hn with ⟨m, rfl⟩
-    clear hn
-    induction n₁ generalizing s with
-    | zero =>
-      cases m with
-      | zero => rfl
-      | succ m =>
-        have h' : enumerate sel (s \ {a}) m = some a := by
-          simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂
-        have : a ∈ s \ {a} := enumerate_mem sel h_sel h'
-        simp_all [Set.mem_diff_singleton]
-    | succ k ih =>
-      cases h : sel s with
-      /- Porting note: The original covered both goals with just `simp_all <;> tauto` -/
-      | none =>
-        simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h,
-          reduceCtorEq]
-      | some =>
-        simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq,
-                       Nat.add_succ, Nat.succ.injEq]
-        exact ih h₁ h₂
+  wlog hn : n₁ ≤ n₂ generalizing n₁ n₂
+  · exact (this h₂ h₁ (lt_of_not_le hn).le).symm
+  rcases Nat.le.dest hn with ⟨m, rfl⟩
+  clear hn
+  induction n₁ generalizing s with
+  | zero =>
+    cases m with
+    | zero => rfl
+    | succ m =>
+      have h' : enumerate sel (s \ {a}) m = some a := by
+        simp_all only [enumerate, Nat.add_eq, zero_add]; exact h₂
+      have : a ∈ s \ {a} := enumerate_mem sel h_sel h'
+      simp_all [Set.mem_diff_singleton]
+  | succ k ih =>
+    rw [show k + 1 + m = (k + m) + 1 by omega] at h₂
+    cases h : sel s <;> simp_all [enumerate] ; tauto
 
 end Enumerate
 

Mathlib/Data/Set/Insert.lean

@@ -130,8 +130,6 @@ theorem forall_insert_of_forall {P : α → Prop} {a : α} {s : Set α} (H : ∀
     (x) (h : x ∈ insert a s) : P x :=
   h.elim (fun e => e.symm ▸ ha) (H _)
 
-/- Porting note: ∃ x ∈ insert a s, P x is parsed as ∃ x, x ∈ insert a s ∧ P x,
- where in Lean3 it was parsed as `∃ x, ∃ (h : x ∈ insert a s), P x` -/
 theorem exists_mem_insert {P : α → Prop} {a : α} {s : Set α} :
     (∃ x ∈ insert a s, P x) ↔ (P a ∨ ∃ x ∈ s, P x) := by
   simp [mem_insert_iff, or_and_right, exists_and_left, exists_or]
@@ -514,7 +512,6 @@ namespace Set
 
 variable {α : Type u} (s t : Set α) (a b : α)
 
--- Porting note: Lean 3 unfolded `{a}` before finding instances but Lean 4 needs additional help
 instance decidableSingleton [Decidable (a = b)] : Decidable (a ∈ ({b} : Set α)) :=
   inferInstanceAs (Decidable (a = b))
 

Mathlib/Data/Set/Pairwise/Lattice.lean

@@ -74,8 +74,8 @@ theorem PairwiseDisjoint.biUnion {s : Set ι'} {g : ι' → Set ι} {f : ι →
   · exact hg d hd (hcd ▸ ha) hb hab
   -- Porting note: the elaborator couldn't figure out `f` here.
   · exact (hs hc hd <| ne_of_apply_ne _ hcd).mono
-      (le_iSup₂ (f := fun i (_ : i ∈ g c) => f i) a ha)
-      (le_iSup₂ (f := fun i (_ : i ∈ g d) => f i) b hb)
+      (le_iSup₂ (f := fun i _ => f i) a ha)
+      (le_iSup₂ (f := fun i _ => f i) b hb)
 
 /-- If the suprema of columns are pairwise disjoint and suprema of rows as well, then everything is
 pairwise disjoint. Not to be confused with `Set.PairwiseDisjoint.prod`. -/

Mathlib/Data/Set/Subsingleton.lean

@@ -127,8 +127,6 @@ protected def Nontrivial (s : Set α) : Prop :=
 theorem nontrivial_of_mem_mem_ne {x y} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : s.Nontrivial :=
   ⟨x, hx, y, hy, hxy⟩
 
--- Porting note: following the pattern for `Exists`, we have renamed `some` to `choose`.
-
 /-- Extract witnesses from s.nontrivial. This function might be used instead of case analysis on the
 argument. Note that it makes a proof depend on the classical.choice axiom. -/
 protected noncomputable def Nontrivial.choose (hs : s.Nontrivial) : α × α :=

Mathlib/Data/SetLike/Basic.lean

@@ -173,8 +173,6 @@ theorem mem_coe {x : B} : x ∈ (p : Set B) ↔ x ∈ p :=
 theorem coe_eq_coe {x y : p} : (x : B) = y ↔ x = y :=
   Subtype.ext_iff_val.symm
 
--- Porting note: this is not necessary anymore due to the way coercions work
-
 @[simp]
 theorem coe_mem (x : p) : (x : B) ∈ p :=
   x.2