feat: update SHA from #18277 (#2653)

leanprover-community/mathlib#18277 backported a bug about classical which is already fixed in mathlib4, so these diffs simpy need a SHA update.

(Comment: This might not be the full PR #18277 yet, as I worked on a file-by-file base)

Mathlib/Data/Dfinsupp/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kenny Lau
 
 ! This file was ported from Lean 3 source module data.dfinsupp.basic
-! leanprover-community/mathlib commit e3d9ab8faa9dea8f78155c6c27d62a621f4c152d
+! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/Data/Finsupp/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Scott Morrison
 
 ! This file was ported from Lean 3 source module data.finsupp.defs
-! leanprover-community/mathlib commit 8631e2d5ea77f6c13054d9151d82b83069680cb1
+! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/Data/Fintype/Sum.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.fintype.sum
-! leanprover-community/mathlib commit 509de852e1de55e1efa8eacfa11df0823f26f226
+! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -47,8 +47,7 @@ def fintypeOfFintypeNe (a : α) (h : Fintype { b // b ≠ a }) : Fintype α :=
     classical exact (Equiv.sumCompl (· = a)).bijective
 #align fintype_of_fintype_ne fintypeOfFintypeNe
 
-open Classical in
-theorem image_subtype_ne_univ_eq_image_erase [Fintype α] (k : β) (b : α → β) :
+theorem image_subtype_ne_univ_eq_image_erase [Fintype α] [DecidableEq β] (k : β) (b : α → β) :
     image (fun i : { a // b a ≠ k } => b ↑i) univ = (image b univ).erase k := by
   apply subset_antisymm
   · rw [image_subset_iff]
@@ -61,8 +60,7 @@ theorem image_subtype_ne_univ_eq_image_erase [Fintype α] (k : β) (b : α → 
     exact ⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩
 #align image_subtype_ne_univ_eq_image_erase image_subtype_ne_univ_eq_image_erase
 
-open Classical in
-theorem image_subtype_univ_ssubset_image_univ [Fintype α] (k : β) (b : α → β)
+theorem image_subtype_univ_ssubset_image_univ [Fintype α] [DecidableEq β] (k : β) (b : α → β)
     (hk : k ∈ Finset.image b univ) (p : β → Prop) [DecidablePred p] (hp : ¬p k) :
     image (fun i : { a // p (b a) } => b ↑i) univ ⊂ image b univ := by
   constructor
@@ -79,10 +77,9 @@ theorem image_subtype_univ_ssubset_image_univ [Fintype α] (k : β) (b : α →
     exact hp (hj' ▸ j.2)
 #align image_subtype_univ_ssubset_image_univ image_subtype_univ_ssubset_image_univ
 
-open Classical in
 /-- Any injection from a finset `s` in a fintype `α` to a finset `t` of the same cardinality as `α`
 can be extended to a bijection between `α` and `t`. -/
-theorem Finset.exists_equiv_extend_of_card_eq [Fintype α] {t : Finset β}
+theorem Finset.exists_equiv_extend_of_card_eq [Fintype α] [DecidableEq β] {t : Finset β}
     (hαt : Fintype.card α = t.card) {s : Finset α} {f : α → β} (hfst : Finset.image f s ⊆ t)
     (hfs : Set.InjOn f s) : ∃ g : α ≃ t, ∀ i ∈ s, (g i : β) = f i := by
   classical

Mathlib/Data/Pi/Lex.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 
 ! This file was ported from Lean 3 source module data.pi.lex
-! leanprover-community/mathlib commit d4f69d96f3532729da8ebb763f4bc26fcf640f06
+! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/Order/OrderIsoNat.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module order.order_iso_nat
-! leanprover-community/mathlib commit 2445c98ae4b87eabebdde552593519b9b6dc350c
+! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -128,30 +128,34 @@ noncomputable def Subtype.orderIsoOfNat : ℕ ≃o s := by
       Nat.Subtype.ofNat_surjective
 #align nat.subtype.order_iso_of_nat Nat.Subtype.orderIsoOfNat
 
---porting note: Added the decidability requirement, I'm not sure how it worked in lean3 without it
-variable {s} [dP : DecidablePred (· ∈ s)]
+variable {s}
 
 @[simp]
-theorem coe_orderEmbeddingOfSet : ⇑(orderEmbeddingOfSet s) = (↑) ∘ Subtype.ofNat s :=
+theorem coe_orderEmbeddingOfSet [DecidablePred (· ∈ s)] :
+    ⇑(orderEmbeddingOfSet s) = (↑) ∘ Subtype.ofNat s :=
   rfl
 #align nat.coe_order_embedding_of_set Nat.coe_orderEmbeddingOfSet
 
-theorem orderEmbeddingOfSet_apply {n : ℕ} : orderEmbeddingOfSet s n = Subtype.ofNat s n :=
+theorem orderEmbeddingOfSet_apply [DecidablePred (· ∈ s)] {n : ℕ} :
+    orderEmbeddingOfSet s n = Subtype.ofNat s n :=
   rfl
 #align nat.order_embedding_of_set_apply Nat.orderEmbeddingOfSet_apply
 
 @[simp]
-theorem Subtype.orderIsoOfNat_apply {n : ℕ} : Subtype.orderIsoOfNat s n = Subtype.ofNat s n := by
+theorem Subtype.orderIsoOfNat_apply [dP : DecidablePred (· ∈ s)] {n : ℕ} :
+    Subtype.orderIsoOfNat s n = Subtype.ofNat s n := by
   simp only [orderIsoOfNat, RelIso.ofSurjective_apply,
     RelEmbedding.orderEmbeddingOfLTEmbedding_apply, RelEmbedding.coe_natLt]
   suffices (fun a => Classical.propDecidable (a ∈ s)) = (fun a => dP a) by
     rw [this]
   simp
+  -- Porting note: This proof was simply `by simp [orderIsoOfNat]; congr`
 #align nat.subtype.order_iso_of_nat_apply Nat.Subtype.orderIsoOfNat_apply
 
 variable (s)
 
-theorem orderEmbeddingOfSet_range : Set.range (Nat.orderEmbeddingOfSet s) = s :=
+theorem orderEmbeddingOfSet_range [DecidablePred (· ∈ s)] :
+    Set.range (Nat.orderEmbeddingOfSet s) = s :=
   Subtype.coe_comp_ofNat_range
 #align nat.order_embedding_of_set_range Nat.orderEmbeddingOfSet_range