Merge pull request #17058 from leanprover-community/bump/nightly-2024…

…-09-23

chore: adaptations for nightly-2024-09-23

Mathlib/Algebra/Group/Hom/Defs.lean

@@ -143,8 +143,9 @@ homomorphisms.
 
 You should also extend this typeclass when you extend `AddMonoidHom`.
 -/
-class AddMonoidHomClass (F M N : Type*) [AddZeroClass M] [AddZeroClass N] [FunLike F M N]
-  extends AddHomClass F M N, ZeroHomClass F M N : Prop
+class AddMonoidHomClass (F : Type*) (M N : outParam Type*)
+    [AddZeroClass M] [AddZeroClass N] [FunLike F M N]
+    extends AddHomClass F M N, ZeroHomClass F M N : Prop
 
 -- Instances and lemmas are defined below through `@[to_additive]`.
 end add_zero

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -94,27 +94,27 @@ variable {A : Type*} [AddGroup A]
 section SubgroupClass
 
 /-- `InvMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under inverses. -/
-class InvMemClass (S G : Type*) [Inv G] [SetLike S G] : Prop where
+class InvMemClass (S : Type*) (G : outParam Type*) [Inv G] [SetLike S G] : Prop where
   /-- `s` is closed under inverses -/
   inv_mem : ∀ {s : S} {x}, x ∈ s → x⁻¹ ∈ s
 
 export InvMemClass (inv_mem)
 
 /-- `NegMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under negation. -/
-class NegMemClass (S G : Type*) [Neg G] [SetLike S G] : Prop where
+class NegMemClass (S : Type*) (G : outParam Type*) [Neg G] [SetLike S G] : Prop where
   /-- `s` is closed under negation -/
   neg_mem : ∀ {s : S} {x}, x ∈ s → -x ∈ s
 
 export NegMemClass (neg_mem)
 
 /-- `SubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are subgroups of `G`. -/
-class SubgroupClass (S G : Type*) [DivInvMonoid G] [SetLike S G] extends SubmonoidClass S G,
-  InvMemClass S G : Prop
+class SubgroupClass (S : Type*) (G : outParam Type*) [DivInvMonoid G] [SetLike S G]
+    extends SubmonoidClass S G, InvMemClass S G : Prop
 
 /-- `AddSubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are
 additive subgroups of `G`. -/
-class AddSubgroupClass (S G : Type*) [SubNegMonoid G] [SetLike S G] extends AddSubmonoidClass S G,
-  NegMemClass S G : Prop
+class AddSubgroupClass (S : Type*) (G : outParam Type*) [SubNegMonoid G] [SetLike S G]
+    extends AddSubmonoidClass S G, NegMemClass S G : Prop
 
 attribute [to_additive] InvMemClass SubgroupClass
 

Mathlib/Algebra/Group/Subgroup/Finite.lean

@@ -165,9 +165,11 @@ theorem pi_mem_of_mulSingle_mem_aux [DecidableEq η] (I : Finset η) {H : Subgro
     x ∈ H := by
   induction I using Finset.induction_on generalizing x with
   | empty =>
-    convert one_mem H
-    ext i
-    exact h1 i (Finset.not_mem_empty i)
+    have : x = 1 := by
+      ext i
+      exact h1 i (Finset.not_mem_empty i)
+    rw [this]
+    exact one_mem H
   | insert hnmem ih =>
     rename_i i I
     have : x = Function.update x i 1 * Pi.mulSingle i (x i) := by

Mathlib/Algebra/Order/Floor.lean

@@ -1706,4 +1706,4 @@ def evalIntCeil : PositivityExt where eval {u α} _zα _pα e := do
 
 end Mathlib.Meta.Positivity
 
-set_option linter.style.longFile 1700
+set_option linter.style.longFile 1800

Mathlib/Algebra/Order/Group/Cone.lean

@@ -18,8 +18,8 @@ cones in groups and the corresponding ordered groups.
 -/
 
 /-- `AddGroupConeClass S G` says that `S` is a type of cones in `G`. -/
-class AddGroupConeClass (S G : Type*) [AddCommGroup G] [SetLike S G] extends
-    AddSubmonoidClass S G : Prop where
+class AddGroupConeClass (S : Type*) (G : outParam Type*) [AddCommGroup G] [SetLike S G]
+    extends AddSubmonoidClass S G : Prop where
   eq_zero_of_mem_of_neg_mem {C : S} {a : G} : a ∈ C → -a ∈ C → a = 0
 
 /-- `GroupConeClass S G` says that `S` is a type of cones in `G`. -/

Mathlib/Algebra/Order/Hom/Basic.lean

@@ -73,29 +73,33 @@ variable {ι F α β γ δ : Type*}
 /-! ### Basics -/
 
 /-- `NonnegHomClass F α β` states that `F` is a type of nonnegative morphisms. -/
-class NonnegHomClass (F α β : Type*) [Zero β] [LE β] [FunLike F α β] : Prop where
+class NonnegHomClass (F : Type*) (α β : outParam Type*) [Zero β] [LE β] [FunLike F α β] : Prop where
   /-- the image of any element is non negative. -/
   apply_nonneg (f : F) : ∀ a, 0 ≤ f a
 
 /-- `SubadditiveHomClass F α β` states that `F` is a type of subadditive morphisms. -/
-class SubadditiveHomClass (F α β : Type*) [Add α] [Add β] [LE β] [FunLike F α β] : Prop where
+class SubadditiveHomClass (F : Type*) (α β : outParam Type*)
+    [Add α] [Add β] [LE β] [FunLike F α β] : Prop where
   /-- the image of a sum is less or equal than the sum of the images. -/
   map_add_le_add (f : F) : ∀ a b, f (a + b) ≤ f a + f b
 
 /-- `SubmultiplicativeHomClass F α β` states that `F` is a type of submultiplicative morphisms. -/
 @[to_additive SubadditiveHomClass]
-class SubmultiplicativeHomClass (F α β : Type*) [Mul α] [Mul β] [LE β] [FunLike F α β] : Prop where
+class SubmultiplicativeHomClass (F : Type*) (α β : outParam (Type*)) [Mul α] [Mul β] [LE β]
+    [FunLike F α β] : Prop where
   /-- the image of a product is less or equal than the product of the images. -/
   map_mul_le_mul (f : F) : ∀ a b, f (a * b) ≤ f a * f b
 
 /-- `MulLEAddHomClass F α β` states that `F` is a type of subadditive morphisms. -/
 @[to_additive SubadditiveHomClass]
-class MulLEAddHomClass (F α β : Type*) [Mul α] [Add β] [LE β] [FunLike F α β] : Prop where
+class MulLEAddHomClass (F : Type*) (α β : outParam Type*) [Mul α] [Add β] [LE β] [FunLike F α β] :
+    Prop where
   /-- the image of a product is less or equal than the sum of the images. -/
   map_mul_le_add (f : F) : ∀ a b, f (a * b) ≤ f a + f b
 
 /-- `NonarchimedeanHomClass F α β` states that `F` is a type of non-archimedean morphisms. -/
-class NonarchimedeanHomClass (F α β : Type*) [Add α] [LinearOrder β] [FunLike F α β] : Prop where
+class NonarchimedeanHomClass (F : Type*) (α β : outParam Type*)
+    [Add α] [LinearOrder β] [FunLike F α β] : Prop where
   /-- the image of a sum is less or equal than the maximum of the images. -/
   map_add_le_max (f : F) : ∀ a b, f (a + b) ≤ max (f a) (f b)
 
@@ -154,7 +158,8 @@ end Mathlib.Meta.Positivity
 group `α`.
 
 You should extend this class when you extend `AddGroupSeminorm`. -/
-class AddGroupSeminormClass (F α β : Type*) [AddGroup α] [OrderedAddCommMonoid β] [FunLike F α β]
+class AddGroupSeminormClass (F : Type*) (α β : outParam Type*)
+    [AddGroup α] [OrderedAddCommMonoid β] [FunLike F α β]
   extends SubadditiveHomClass F α β : Prop where
   /-- The image of zero is zero. -/
   map_zero (f : F) : f 0 = 0
@@ -165,7 +170,8 @@ class AddGroupSeminormClass (F α β : Type*) [AddGroup α] [OrderedAddCommMonoi
 
 You should extend this class when you extend `GroupSeminorm`. -/
 @[to_additive]
-class GroupSeminormClass (F α β : Type*) [Group α] [OrderedAddCommMonoid β] [FunLike F α β]
+class GroupSeminormClass (F : Type*) (α β : outParam Type*)
+    [Group α] [OrderedAddCommMonoid β] [FunLike F α β]
   extends MulLEAddHomClass F α β : Prop where
   /-- The image of one is zero. -/
   map_one_eq_zero (f : F) : f 1 = 0
@@ -176,7 +182,8 @@ class GroupSeminormClass (F α β : Type*) [Group α] [OrderedAddCommMonoid β]
 `α`.
 
 You should extend this class when you extend `AddGroupNorm`. -/
-class AddGroupNormClass (F α β : Type*) [AddGroup α] [OrderedAddCommMonoid β] [FunLike F α β]
+class AddGroupNormClass (F : Type*) (α β : outParam Type*)
+    [AddGroup α] [OrderedAddCommMonoid β] [FunLike F α β]
   extends AddGroupSeminormClass F α β : Prop where
   /-- The argument is zero if its image under the map is zero. -/
   eq_zero_of_map_eq_zero (f : F) {a : α} : f a = 0 → a = 0
@@ -185,7 +192,8 @@ class AddGroupNormClass (F α β : Type*) [AddGroup α] [OrderedAddCommMonoid β
 
 You should extend this class when you extend `GroupNorm`. -/
 @[to_additive]
-class GroupNormClass (F α β : Type*) [Group α] [OrderedAddCommMonoid β] [FunLike F α β]
+class GroupNormClass (F : Type*) (α β : outParam Type*)
+    [Group α] [OrderedAddCommMonoid β] [FunLike F α β]
   extends GroupSeminormClass F α β : Prop where
   /-- The argument is one if its image under the map is zero. -/
   eq_one_of_map_eq_zero (f : F) {a : α} : f a = 0 → a = 1
@@ -275,20 +283,23 @@ theorem map_pos_of_ne_one [Group α] [LinearOrderedAddCommMonoid β] [GroupNormC
 /-- `RingSeminormClass F α` states that `F` is a type of `β`-valued seminorms on the ring `α`.
 
 You should extend this class when you extend `RingSeminorm`. -/
-class RingSeminormClass (F α β : Type*) [NonUnitalNonAssocRing α] [OrderedSemiring β]
-  [FunLike F α β] extends AddGroupSeminormClass F α β, SubmultiplicativeHomClass F α β : Prop
+class RingSeminormClass (F : Type*) (α β : outParam Type*)
+    [NonUnitalNonAssocRing α] [OrderedSemiring β] [FunLike F α β]
+  extends AddGroupSeminormClass F α β, SubmultiplicativeHomClass F α β : Prop
 
 /-- `RingNormClass F α` states that `F` is a type of `β`-valued norms on the ring `α`.
 
 You should extend this class when you extend `RingNorm`. -/
-class RingNormClass (F α β : Type*) [NonUnitalNonAssocRing α] [OrderedSemiring β] [FunLike F α β]
+class RingNormClass (F : Type*) (α β : outParam Type*)
+    [NonUnitalNonAssocRing α] [OrderedSemiring β] [FunLike F α β]
   extends RingSeminormClass F α β, AddGroupNormClass F α β : Prop
 
 /-- `MulRingSeminormClass F α` states that `F` is a type of `β`-valued multiplicative seminorms
 on the ring `α`.
 
 You should extend this class when you extend `MulRingSeminorm`. -/
-class MulRingSeminormClass (F α β : Type*) [NonAssocRing α] [OrderedSemiring β] [FunLike F α β]
+class MulRingSeminormClass (F : Type*) (α β : outParam Type*)
+    [NonAssocRing α] [OrderedSemiring β] [FunLike F α β]
   extends AddGroupSeminormClass F α β, MonoidWithZeroHomClass F α β : Prop
 
 -- Lower the priority of these instances since they require synthesizing an order structure.
@@ -299,7 +310,8 @@ attribute [instance 50]
 ring `α`.
 
 You should extend this class when you extend `MulRingNorm`. -/
-class MulRingNormClass (F α β : Type*) [NonAssocRing α] [OrderedSemiring β] [FunLike F α β]
+class MulRingNormClass (F : Type*) (α β : outParam Type*)
+    [NonAssocRing α] [OrderedSemiring β] [FunLike F α β]
   extends MulRingSeminormClass F α β, AddGroupNormClass F α β : Prop
 
 -- See note [out-param inheritance]

Mathlib/Algebra/Order/Monoid/Prod.lean

@@ -40,7 +40,7 @@ instance [CanonicallyOrderedCommMonoid α] [CanonicallyOrderedCommMonoid β] :
     CanonicallyOrderedCommMonoid (α × β) :=
   { (inferInstance : OrderedCommMonoid _), (inferInstance : OrderBot _),
     (inferInstance : ExistsMulOfLE _) with
-      le_self_mul := fun _ _ ↦ ⟨le_self_mul, le_self_mul⟩ }
+      le_self_mul := fun _ _ ↦ le_def.mpr ⟨le_self_mul, le_self_mul⟩ }
 
 namespace Lex
 

Mathlib/Algebra/Order/Ring/Cone.lean

@@ -19,7 +19,7 @@ cones in rings and the corresponding ordered rings.
 -/
 
 /-- `RingConeClass S R` says that `S` is a type of cones in `R`. -/
-class RingConeClass (S R : Type*) [Ring R] [SetLike S R]
+class RingConeClass (S : Type*) (R : outParam Type*) [Ring R] [SetLike S R]
     extends AddGroupConeClass S R, SubsemiringClass S R : Prop
 
 /-- A (positive) cone in a ring is a subsemiring that

Mathlib/Algebra/Ring/CentroidHom.lean

@@ -61,8 +61,8 @@ attribute [nolint docBlame] CentroidHom.toAddMonoidHom
 /-- `CentroidHomClass F α` states that `F` is a type of centroid homomorphisms.
 
 You should extend this class when you extend `CentroidHom`. -/
-class CentroidHomClass (F α : Type*) [NonUnitalNonAssocSemiring α] [FunLike F α α] extends
-  AddMonoidHomClass F α α : Prop where
+class CentroidHomClass (F : Type*) (α : outParam Type*)
+    [NonUnitalNonAssocSemiring α] [FunLike F α α] extends AddMonoidHomClass F α α : Prop where
   /-- Commutativity of centroid homomorphims with left multiplication. -/
   map_mul_left (f : F) (a b : α) : f (a * b) = a * f b
   /-- Commutativity of centroid homomorphims with right multiplication. -/

Mathlib/Algebra/Ring/Subring/Basic.lean

@@ -72,7 +72,7 @@ section SubringClass
 
 /-- `SubringClass S R` states that `S` is a type of subsets `s ⊆ R` that
 are both a multiplicative submonoid and an additive subgroup. -/
-class SubringClass (S : Type*) (R : Type u) [Ring R] [SetLike S R] extends
+class SubringClass (S : Type*) (R : outParam (Type u)) [Ring R] [SetLike S R] extends
   SubsemiringClass S R, NegMemClass S R : Prop
 
 -- See note [lower instance priority]

Mathlib/Algebra/Ring/Subsemiring/Basic.lean

@@ -59,12 +59,12 @@ section SubsemiringClass
 
 /-- `SubsemiringClass S R` states that `S` is a type of subsets `s ⊆ R` that
 are both a multiplicative and an additive submonoid. -/
-class SubsemiringClass (S : Type*) (R : Type u) [NonAssocSemiring R]
+class SubsemiringClass (S : Type*) (R : outParam (Type u)) [NonAssocSemiring R]
   [SetLike S R] extends SubmonoidClass S R, AddSubmonoidClass S R : Prop
 
 -- See note [lower instance priority]
 instance (priority := 100) SubsemiringClass.addSubmonoidWithOneClass (S : Type*)
-    (R : Type u) [NonAssocSemiring R] [SetLike S R] [h : SubsemiringClass S R] :
+    (R : Type u) {_ : NonAssocSemiring R} [SetLike S R] [h : SubsemiringClass S R] :
     AddSubmonoidWithOneClass S R :=
   { h with }
 

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -294,7 +294,12 @@ theorem mem_carrier_iff_of_mem (hm : 0 < m) (q : Spec.T A⁰_ f) (a : A) {n} (hn
   trans (HomogeneousLocalization.mk ⟨m * n, ⟨proj 𝒜 n a ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
     ⟨f ^ n, by rw [mul_comm]; mem_tac⟩, ⟨_, rfl⟩⟩ : A⁰_ f) ∈ q.asIdeal
   · refine ⟨fun h ↦ h n, fun h i ↦ if hi : i = n then hi ▸ h else ?_⟩
-    convert zero_mem q.asIdeal
+    #adaptation_note
+    /--
+    After https://github.com/leanprover/lean4/pull/5376
+    we need to specify the implicit arguments by `inferInstance`.
+    -/
+    convert @zero_mem _ _ inferInstance inferInstance _ q.asIdeal
     apply HomogeneousLocalization.val_injective
     simp only [proj_apply, decompose_of_mem_ne _ hn (Ne.symm hi), zero_pow hm.ne',
       HomogeneousLocalization.val_mk, Localization.mk_zero, HomogeneousLocalization.val_zero]

Mathlib/AlgebraicGeometry/Pullbacks.lean

@@ -583,7 +583,8 @@ the morphism `Spec (S ⊗[R] T) ⟶ Spec T` obtained by applying `Spec.map` to t
 -/
 @[reassoc (attr := simp)]
 lemma pullbackSpecIso_inv_snd :
-    (pullbackSpecIso R S T).inv ≫ pullback.snd _ _ = Spec.map (ofHom (toRingHom includeRight)) :=
+    (pullbackSpecIso R S T).inv ≫ pullback.snd _ _ =
+      Spec.map (ofHom (R := T) (S := S ⊗[R] T) (toRingHom includeRight)) :=
   limit.isoLimitCone_inv_π _ _
 /--
 The composition of the isomorphism `pullbackSepcIso R S T` (from the pullback of

Mathlib/CategoryTheory/LiftingProperties/Basic.lean

@@ -41,7 +41,7 @@ class HasLiftingProperty : Prop where
   sq_hasLift : ∀ {f : A ⟶ X} {g : B ⟶ Y} (sq : CommSq f i p g), sq.HasLift
 
 instance (priority := 100) sq_hasLift_of_hasLiftingProperty {f : A ⟶ X} {g : B ⟶ Y}
-    (sq : CommSq f i p g) [hip : HasLiftingProperty i p] : sq.HasLift := by apply hip.sq_hasLift
+    (sq : CommSq f i p g) [hip : HasLiftingProperty i p] : sq.HasLift := hip.sq_hasLift _
 
 namespace HasLiftingProperty
 

Mathlib/CategoryTheory/Limits/Shapes/Images.lean

@@ -81,8 +81,6 @@ attribute [reassoc (attr := simp)] MonoFactorisation.fac
 
 attribute [instance] MonoFactorisation.m_mono
 
-attribute [instance] MonoFactorisation.m_mono
-
 namespace MonoFactorisation
 
 /-- The obvious factorisation of a monomorphism through itself. -/

Mathlib/Combinatorics/Configuration.lean

@@ -128,7 +128,7 @@ theorem Nondegenerate.exists_injective_of_card_le [Nondegenerate P L] [Fintype P
     by_cases hs₁ : s.card = 1
     -- If `s = {l}`, then pick a point `p ∉ l`
     · obtain ⟨l, rfl⟩ := Finset.card_eq_one.mp hs₁
-      obtain ⟨p, hl⟩ := exists_point l
+      obtain ⟨p, hl⟩ := exists_point (P := P) l
       rw [Finset.card_singleton, Finset.singleton_biUnion, Nat.one_le_iff_ne_zero]
       exact Finset.card_ne_zero_of_mem (Set.mem_toFinset.mpr hl)
     suffices (s.biUnion t)ᶜ.card ≤ sᶜ.card by

Mathlib/Computability/Halting.lean

@@ -281,8 +281,6 @@ namespace Nat.Partrec'
 
 open Mathlib.Vector Partrec Computable
 
-open Nat (Partrec')
-
 open Nat.Partrec'
 
 theorem to_part {n f} (pf : @Partrec' n f) : _root_.Partrec f := by

Mathlib/Data/Fin/Basic.lean

@@ -359,10 +359,6 @@ section Monoid
 protected theorem add_zero [NeZero n] (k : Fin n) : k + 0 = k := by
   simp only [add_def, val_zero', Nat.add_zero, mod_eq_of_lt (is_lt k)]
 
--- Porting note (#10618): removing `simp`, `simp` can prove it with AddCommMonoid instance
-protected theorem zero_add [NeZero n] (k : Fin n) : 0 + k = k := by
-  simp [Fin.ext_iff, add_def, mod_eq_of_lt (is_lt k)]
-
 instance inhabitedFinOneAdd (n : ℕ) : Inhabited (Fin (1 + n)) :=
   haveI : NeZero (1 + n) := by rw [Nat.add_comm]; infer_instance
   inferInstance
@@ -455,13 +451,6 @@ lemma natCast_strictMono (hbn : b ≤ n) (hab : a < b) : (a : Fin (n + 1)) < b :
 
 end OfNatCoe
 
-@[simp]
-theorem one_eq_zero_iff [NeZero n] : (1 : Fin n) = 0 ↔ n = 1 := by
-  obtain _ | _ | n := n <;> simp [Fin.ext_iff]
-
-@[simp]
-theorem zero_eq_one_iff [NeZero n] : (0 : Fin n) = 1 ↔ n = 1 := by rw [eq_comm, one_eq_zero_iff]
-
 end Add
 
 section Succ
@@ -517,10 +506,6 @@ This one instead uses a `NeZero n` typeclass hypothesis.
 theorem le_zero_iff' {n : ℕ} [NeZero n] {k : Fin n} : k ≤ 0 ↔ k = 0 :=
   ⟨fun h => Fin.ext <| by rw [Nat.eq_zero_of_le_zero h]; rfl, by rintro rfl; exact Nat.le_refl _⟩
 
--- Move to Batteries?
-@[simp] theorem cast_refl {n : Nat} (h : n = n) :
-    Fin.cast h = id := rfl
-
 -- TODO: Move to Batteries
 @[simp] lemma castLE_inj {hmn : m ≤ n} {a b : Fin m} : castLE hmn a = castLE hmn b ↔ a = b := by
   simp [Fin.ext_iff]
@@ -1430,7 +1415,7 @@ theorem eq_zero (n : Fin 1) : n = 0 := Subsingleton.elim _ _
 instance uniqueFinOne : Unique (Fin 1) where
   uniq _ := Subsingleton.elim _ _
 
-@[simp]
+@[deprecated val_eq_zero (since := "2024-09-18")]
 theorem coe_fin_one (a : Fin 1) : (a : ℕ) = 0 := by simp [Subsingleton.elim a 0]
 
 lemma eq_one_of_neq_zero (i : Fin 2) (hi : i ≠ 0) : i = 1 :=

Mathlib/Data/List/Indexes.lean

@@ -55,9 +55,9 @@ theorem mapIdxGo_append : ∀ (f : ℕ → α → β) (l₁ l₂ : List α) (arr
       cases l₂
       · rfl
       · rw [List.length_append] at h; contradiction
-    rw [l₁_nil, l₂_nil]; simp only [mapIdx.go, Array.toArray_toList]
+    rw [l₁_nil, l₂_nil]; simp only [mapIdx.go, List.toArray_toList]
   · cases' l₁ with head tail <;> simp only [mapIdx.go]
-    · simp only [nil_append, Array.toArray_toList]
+    · simp only [nil_append, List.toArray_toList]
     · simp only [List.append_eq]
       rw [ih]
       · simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h
@@ -119,7 +119,8 @@ theorem getElem?_mapIdx_go (f : ℕ → α → β) : ∀ (l : List α) (arr : Ar
     (mapIdx.go f l arr)[i]? =
       if h : i < arr.size then some arr[i] else Option.map (f i) l[i - arr.size]?
   | [], arr, i => by
-    simp [mapIdx.go, getElem?_eq, Array.getElem_eq_toList_getElem]
+    simp only [mapIdx.go, Array.toListImpl_eq, getElem?_eq, Array.toList_length,
+      Array.getElem_eq_toList_getElem, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none']
   | a :: l, arr, i => by
     rw [mapIdx.go, getElem?_mapIdx_go]
     simp only [Array.size_push]