chore: bump toolchain to v4.3.0-rc1 (#8051)

This incorporates changes from 

* #7845
* #7847
* #7853
* #7872 (was never actually made to work, but the diffs in `nightly-testing` are unexciting: we need to fully qualify a few names)

They can all be closed when this is merged.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/Algebra/Operations.lean

@@ -463,10 +463,7 @@ protected theorem pow_induction_on_right' {C : ∀ (n : ℕ) (x), x ∈ M ^ n 
     obtain ⟨r, rfl⟩ := hx
     exact hr r
   revert hx
-  -- porting note: workaround for lean4#1926, was `simp_rw [pow_succ']`
-  suffices h_lean4_1926 : ∀ (hx' : x ∈ M ^ n * M), C (Nat.succ n) x (by rwa [pow_succ']) from
-    fun hx => h_lean4_1926 (by rwa [← pow_succ'])
-  -- porting note: end workaround
+  simp_rw [pow_succ']
   intro hx
   exact
     Submodule.mul_induction_on' (fun m hm x ih => hmul _ _ hm (n_ih _) _ ih)

Mathlib/Algebra/BigOperators/Ring.lean

@@ -147,7 +147,7 @@ theorem prod_add [DecidableEq α] (f g : α → β) (s : Finset α) :
           rw [prod_ite]
           congr 1
           exact prod_bij'
-            (fun a _ => a.1) (by simp; tauto) (by simp)
+            (fun a _ => a.1) (by simp) (by simp)
             (fun a ha => ⟨a, (mem_filter.1 ha).1⟩) (fun a ha => by simp at ha; simp; tauto)
             (by simp) (by simp)
           exact prod_bij'

Mathlib/Algebra/Homology/Homology.lean

@@ -303,35 +303,13 @@ def homology'Functor [HasCokernels V] (i : ι) : HomologicalComplex V c ⥤ V wh
   -- here, but universe implementation details get in the way...
   obj C := C.homology' i
   map {C₁ C₂} f := homology'.map _ _ (f.sqTo i) (f.sqFrom i) rfl
-  map_id _ := by
-    simp only
-    ext1
-    simp only [homology'.π_map, kernelSubobjectMap_id, Hom.sqFrom_id, Category.id_comp,
-      Category.comp_id]
-  map_comp _ _ := by
-    simp only
-    ext1
-    simp only [Hom.sqFrom_comp, kernelSubobjectMap_comp, homology'.π_map_assoc, homology'.π_map,
-      Category.assoc]
 #align homology_functor homology'Functor
 
 /-- The homology functor from `ι`-indexed complexes to `ι`-graded objects in `V`. -/
 @[simps]
 def gradedHomology'Functor [HasCokernels V] : HomologicalComplex V c ⥤ GradedObject ι V where
   obj C i := C.homology' i
   map {C C'} f i := (homology'Functor V c i).map f
-  map_id _ := by
-    ext
-    simp only [GradedObject.categoryOfGradedObjects_id]
-    ext
-    simp only [homology'.π_map, homology'Functor_map, kernelSubobjectMap_id, Hom.sqFrom_id,
-      Category.id_comp, Category.comp_id]
-  map_comp _ _ := by
-    ext
-    simp only [GradedObject.categoryOfGradedObjects_comp]
-    ext
-    simp only [Hom.sqFrom_comp, kernelSubobjectMap_comp, homology'.π_map_assoc, homology'.π_map,
-      homology'Functor_map, Category.assoc]
 #align graded_homology_functor gradedHomology'Functor
 
 end

Mathlib/Algebra/Homology/Single.lean

@@ -131,14 +131,6 @@ def single₀ : V ⥤ ChainComplex V ℕ where
         match n with
         | 0 => f
         | n + 1 => 0 }
-  map_id X := by
-    ext (_|_)
-    · rfl
-    · simp
-  map_comp f g := by
-    ext (_|_)
-    · rfl
-    · simp
 #align chain_complex.single₀ ChainComplex.single₀
 
 @[simp]
@@ -328,14 +320,6 @@ def single₀ : V ⥤ CochainComplex V ℕ where
         match n with
         | 0 => f
         | n + 1 => 0 }
-  map_id X := by
-    ext (_|_)
-    · rfl
-    · simp
-  map_comp f g := by
-    ext (_|_)
-    · rfl
-    · simp
 #align cochain_complex.single₀ CochainComplex.single₀
 
 @[simp]

Mathlib/Algebra/Jordan/Basic.lean

@@ -194,7 +194,7 @@ private theorem aux0 {a b c : A} : ⁅L (a + b + c), L ((a + b + c) * (a + b + c
   simp only [lie_add, add_lie, commute_lmul_lmul_sq, zero_add, add_zero]
   abel
 
-set_option maxHeartbeats 400000 in
+set_option maxHeartbeats 300000 in
 private theorem aux1 {a b c : A} :
     ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) +
     2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆

Mathlib/Algebra/Order/CompleteField.lean

@@ -155,7 +155,8 @@ theorem cutMap_add (a b : α) : cutMap β (a + b) = cutMap β a + cutMap β b :=
       rw [coe_mem_cutMap_iff]
       exact_mod_cast sub_lt_comm.mp hq₁q
   · rintro _ ⟨_, _, ⟨qa, ha, rfl⟩, ⟨qb, hb, rfl⟩, rfl⟩
-    refine' ⟨qa + qb, _, by norm_cast⟩
+    -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
+    refine' ⟨qa + qb, _, by beta_reduce; norm_cast⟩
     rw [mem_setOf_eq, cast_add]
     exact add_lt_add ha hb
 #align linear_ordered_field.cut_map_add LinearOrderedField.cutMap_add

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -199,7 +199,6 @@ theorem toΓSpecSheafedSpace_app_eq :
   dsimp at this
   rw [←this]
   dsimp
-  congr
 
 #align algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_SheafedSpace_app_eq AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq
 

Mathlib/Analysis/Analytic/Inverse.lean

@@ -563,7 +563,9 @@ theorem radius_rightInv_pos_of_radius_pos (p : FormalMultilinearSeries 𝕜 E F)
   -- conclude that all coefficients satisfy `aⁿ Qₙ ≤ (I + 1) a`.
   let a' : NNReal := ⟨a, apos.le⟩
   suffices H : (a' : ENNReal) ≤ (p.rightInv i).radius
-  · apply lt_of_lt_of_le _ H; exact_mod_cast apos
+  · apply lt_of_lt_of_le _ H
+    -- Prior to leanprover/lean4#2734, this was `exact_mod_cast apos`.
+    simpa only [ENNReal.coe_pos]
   apply le_radius_of_bound _ ((I + 1) * a) fun n => ?_
   by_cases hn : n = 0
   · have : ‖p.rightInv i n‖ = ‖p.rightInv i 0‖ := by congr <;> try rw [hn]

Mathlib/Analysis/MeanInequalities.lean

@@ -609,6 +609,8 @@ theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.IsConjugateExponent q) (hf :
       ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := by
   lift f to ι → ℝ≥0 using hf
   lift g to ι → ℝ≥0 using hg
+  -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
+  beta_reduce at *
   norm_cast at *
   exact NNReal.inner_le_Lp_mul_Lq_tsum hpq hf_sum hg_sum
 #align real.inner_le_Lp_mul_Lq_tsum_of_nonneg Real.inner_le_Lp_mul_Lq_tsum_of_nonneg
@@ -637,6 +639,8 @@ theorem inner_le_Lp_mul_Lq_hasSum_of_nonneg (hpq : p.IsConjugateExponent q) {A B
   lift g to ι → ℝ≥0 using hg
   lift A to ℝ≥0 using hA
   lift B to ℝ≥0 using hB
+  -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
+  beta_reduce at *
   norm_cast at hf_sum hg_sum
   obtain ⟨C, hC, H⟩ := NNReal.inner_le_Lp_mul_Lq_hasSum hpq hf_sum hg_sum
   refine' ⟨C, C.prop, hC, _⟩
@@ -674,6 +678,8 @@ theorem Lp_add_le_tsum_of_nonneg (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : 
         (∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p) := by
   lift f to ι → ℝ≥0 using hf
   lift g to ι → ℝ≥0 using hg
+  -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
+  beta_reduce at *
   norm_cast0 at *
   exact NNReal.Lp_add_le_tsum hp hf_sum hg_sum
 #align real.Lp_add_le_tsum_of_nonneg Real.Lp_add_le_tsum_of_nonneg
@@ -702,9 +708,13 @@ theorem Lp_add_le_hasSum_of_nonneg (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg :
   lift g to ι → ℝ≥0 using hg
   lift A to ℝ≥0 using hA
   lift B to ℝ≥0 using hB
+  -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
+  beta_reduce at hfA hgB
   norm_cast at hfA hgB
   obtain ⟨C, hC₁, hC₂⟩ := NNReal.Lp_add_le_hasSum hp hfA hgB
   use C
+  -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
+  beta_reduce
   norm_cast
   exact ⟨zero_le _, hC₁, hC₂⟩
 #align real.Lp_add_le_has_sum_of_nonneg Real.Lp_add_le_hasSum_of_nonneg

Mathlib/CategoryTheory/Comma.lean

@@ -167,9 +167,8 @@ theorem eqToHom_left (X Y : Comma L R) (H : X = Y) :
 #align category_theory.comma.eq_to_hom_left CategoryTheory.Comma.eqToHom_left
 
 @[simp]
-theorem eqToHom_right (X Y : Comma L R) (H : X = Y) : CommaMorphism.right (eqToHom H) = eqToHom (by
-    cases H
-    rfl) := by
+theorem eqToHom_right (X Y : Comma L R) (H : X = Y) :
+    CommaMorphism.right (eqToHom H) = eqToHom (by cases H; rfl) := by
   cases H
   rfl
 #align category_theory.comma.eq_to_hom_right CategoryTheory.Comma.eqToHom_right

Mathlib/CategoryTheory/DifferentialObject.lean

@@ -219,12 +219,10 @@ variable [(shiftFunctor C (1 : S)).PreservesZeroMorphisms]
 
 open scoped ZeroObject
 
-instance hasZeroObject : HasZeroObject (DifferentialObject S C) := by
-  -- Porting note(https://github.com/leanprover-community/mathlib4/issues/4998): added `aesop_cat`
-  -- Porting note: added `simp only [eq_iff_true_of_subsingleton]`
-  refine' ⟨⟨⟨0, 0, by aesop_cat⟩, fun X => ⟨⟨⟨⟨0, by aesop_cat⟩⟩, fun f => _⟩⟩,
-    fun X => ⟨⟨⟨⟨0, by aesop_cat⟩⟩, fun f => _⟩⟩⟩⟩ <;> ext <;>
-    simp only [eq_iff_true_of_subsingleton]
+instance hasZeroObject : HasZeroObject (DifferentialObject S C) where
+  zero := ⟨{ obj := 0, d := 0 },
+    { unique_to := fun X => ⟨⟨⟨{ f := 0 }⟩, fun f => by ext⟩⟩,
+      unique_from := fun X => ⟨⟨⟨{ f := 0 }⟩, fun f => by ext⟩⟩ }⟩
 #align category_theory.differential_object.has_zero_object CategoryTheory.DifferentialObject.hasZeroObject
 
 end DifferentialObject

Mathlib/CategoryTheory/Functor/Flat.lean

@@ -208,7 +208,7 @@ theorem uniq {K : J ⥤ C} {c : Cone K} (hc : IsLimit c) (s : Cone (K ⋙ F))
     intro j
     injection c₀.π.naturality (BiconeHom.left j) with _ e₁
     injection c₀.π.naturality (BiconeHom.right j) with _ e₂
-    simpa (config := {zeta := false}) using e₁.symm.trans e₂
+    simpa using e₁.symm.trans e₂
   have : c.extend g₁.right = c.extend g₂.right := by
     unfold Cone.extend
     congr 1

Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean

@@ -80,7 +80,6 @@ instance functor_category_isIdempotentComplete [IsIdempotentComplete C] :
   use Y, i, e
   constructor
   · ext j
-    apply equalizer.hom_ext
     dsimp
     rw [assoc, equalizer.lift_ι, ← equalizer.condition, id_comp, comp_id]
   · ext j

Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

@@ -450,7 +450,10 @@ private theorem edgeDensity_star_not_uniform [Nonempty α]
   set s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))
   set t : ℝ := ↑(G.edgeDensity U V)
   have hrs : |r - s| ≤ ε / 5 := abs_density_star_sub_density_le_eps hPε hε₁ hUVne hUV
-  have hst : ε ≤ |s - t| := by exact_mod_cast G.nonuniformWitness_spec hUVne hUV
+  have hst : ε ≤ |s - t| := by
+    -- After leanprover/lean4#2734, we need to do the zeta reduction before `norm_cast`.
+    unfold_let s t
+    exact_mod_cast G.nonuniformWitness_spec hUVne hUV
   have hpr : |p - r| ≤ ε ^ 5 / 49 :=
     average_density_near_total_density hPα hPε hε₁ star_subset_chunk star_subset_chunk
   have hqt : |q - t| ≤ ε ^ 5 / 49 := by

Mathlib/Data/Complex/Module.lean

@@ -479,7 +479,7 @@ lemma IsSelfAdjoint.coe_realPart {x : A} (hx : IsSelfAdjoint x) :
     (ℜ x : A) = x :=
   hx.coe_selfAdjointPart_apply ℝ
 
-lemma IsSelfAdjoint.imaginaryPart {x : A} (hx : IsSelfAdjoint x) :
+nonrec lemma IsSelfAdjoint.imaginaryPart {x : A} (hx : IsSelfAdjoint x) :
     ℑ x = 0 := by
   rw [imaginaryPart, LinearMap.comp_apply, hx.skewAdjointPart_apply _, map_zero]
 

Mathlib/Data/Ordmap/Ordset.lean

@@ -408,7 +408,7 @@ theorem Sized.dual_iff {t : Ordnode α} : Sized (.dual t) ↔ Sized t :=
 
 theorem Sized.rotateL {l x r} (hl : @Sized α l) (hr : Sized r) : Sized (rotateL l x r) := by
   cases r; · exact hl.node' hr
-  rw [rotateL]; split_ifs
+  rw [Ordnode.rotateL]; split_ifs
   · exact hl.node3L hr.2.1 hr.2.2
   · exact hl.node4L hr.2.1 hr.2.2
 #align ordnode.sized.rotate_l Ordnode.Sized.rotateL
@@ -1247,7 +1247,7 @@ theorem Valid'.rotateL {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : V
   have ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1 := by intros; linarith
   have hlp : size l > 0 → ¬size rl + size rr ≤ 1 := fun l0 hb =>
     absurd (le_trans (le_trans (Nat.mul_le_mul_left _ l0) H2) hb) (by decide)
-  rw [rotateL]; split_ifs with h
+  rw [Ordnode.rotateL]; split_ifs with h
   · have rr0 : size rr > 0 :=
       (mul_lt_mul_left (by decide)).1 (lt_of_le_of_lt (Nat.zero_le _) h : ratio * 0 < _)
     suffices BalancedSz (size l) (size rl) ∧ BalancedSz (size l + size rl + 1) (size rr) by

Mathlib/Data/Prod/TProd.lean

@@ -177,7 +177,7 @@ theorem elim_preimage_pi [DecidableEq ι] {l : List ι} (hnd : l.Nodup) (h : ∀
     simp [h]
   rw [← h2, ← mk_preimage_tprod, preimage_preimage]
   simp only [TProd.mk_elim hnd h]
-  dsimp; rfl
+  dsimp
 #align set.elim_preimage_pi Set.elim_preimage_pi
 
 end Set

Mathlib/Data/Set/Basic.lean

@@ -2202,19 +2202,15 @@ theorem powerset_singleton (x : α) : 𝒫({x} : Set α) = {∅, {x}} := by
 
 /-! ### Sets defined as an if-then-else -/
 
---Porting note: New theorem to prove `mem_dite` lemmas.
--- `simp [h]` where `h : p` does not simplify `∀ (h : p), x ∈ s h` any more.
--- https://github.com/leanprover/lean4/issues/1926
 theorem mem_dite (p : Prop) [Decidable p] (s : p → Set α) (t : ¬ p → Set α) (x : α) :
     (x ∈ if h : p then s h else t h) ↔ (∀ h : p, x ∈ s h) ∧ ∀ h : ¬p, x ∈ t h := by
   split_ifs with hp
   · exact ⟨fun hx => ⟨fun _ => hx, fun hnp => (hnp hp).elim⟩, fun hx => hx.1 hp⟩
   · exact ⟨fun hx => ⟨fun h => (hp h).elim, fun _ => hx⟩, fun hx => hx.2 hp⟩
 
---Porting note: Old proof was `split_ifs; simp [h]`
 theorem mem_dite_univ_right (p : Prop) [Decidable p] (t : p → Set α) (x : α) :
     (x ∈ if h : p then t h else univ) ↔ ∀ h : p, x ∈ t h := by
-  simp [mem_dite]
+  split_ifs <;> simp_all
 #align set.mem_dite_univ_right Set.mem_dite_univ_right
 
 @[simp]
@@ -2225,7 +2221,7 @@ theorem mem_ite_univ_right (p : Prop) [Decidable p] (t : Set α) (x : α) :
 
 theorem mem_dite_univ_left (p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) :
     (x ∈ if h : p then univ else t h) ↔ ∀ h : ¬p, x ∈ t h := by
-  simp [mem_dite]
+  split_ifs <;> simp_all
 #align set.mem_dite_univ_left Set.mem_dite_univ_left
 
 @[simp]

Mathlib/Data/UInt.lean

@@ -5,15 +5,20 @@ import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.Ring.Basic
 import Mathlib.Data.ZMod.Defs
 
-lemma UInt8.val_eq_of_lt {a : Nat} : a < UInt8.size -> (ofNat a).val = a := Nat.mod_eq_of_lt
+lemma UInt8.val_eq_of_lt {a : Nat} : a < UInt8.size → ((ofNat a).val : Nat) = a :=
+  Nat.mod_eq_of_lt
 
-lemma UInt16.val_eq_of_lt {a : Nat} : a < UInt16.size -> (ofNat a).val = a := Nat.mod_eq_of_lt
+lemma UInt16.val_eq_of_lt {a : Nat} : a < UInt16.size → ((ofNat a).val : Nat) = a :=
+  Nat.mod_eq_of_lt
 
-lemma UInt32.val_eq_of_lt {a : Nat} : a < UInt32.size -> (ofNat a).val = a := Nat.mod_eq_of_lt
+lemma UInt32.val_eq_of_lt {a : Nat} : a < UInt32.size → ((ofNat a).val : Nat) = a :=
+  Nat.mod_eq_of_lt
 
-lemma UInt64.val_eq_of_lt {a : Nat} : a < UInt64.size -> (ofNat a).val = a := Nat.mod_eq_of_lt
+lemma UInt64.val_eq_of_lt {a : Nat} : a < UInt64.size → ((ofNat a).val : Nat) = a :=
+  Nat.mod_eq_of_lt
 
-lemma USize.val_eq_of_lt {a : Nat} : a < USize.size -> (ofNat a).val = a := Nat.mod_eq_of_lt
+lemma USize.val_eq_of_lt {a : Nat} : a < USize.size → ((ofNat a).val : Nat) = a :=
+  Nat.mod_eq_of_lt
 
 instance UInt8.neZero : NeZero UInt8.size := ⟨by decide⟩
 

Mathlib/Lean/Meta/DiscrTree.lean

@@ -18,12 +18,12 @@ namespace Lean.Meta.DiscrTree
 Inserts a new key into a discrimination tree,
 but only if it is not of the form `#[*]` or `#[=, *, *, *]`.
 -/
-def insertIfSpecific [BEq α] (d : DiscrTree α s)
-    (keys : Array (DiscrTree.Key s)) (v : α) : DiscrTree α s :=
+def insertIfSpecific [BEq α] (d : DiscrTree α)
+    (keys : Array Key) (v : α) (config : WhnfCoreConfig) : DiscrTree α :=
   if keys == #[Key.star] || keys == #[Key.const `Eq 3, Key.star, Key.star, Key.star] then
     d
   else
-    d.insertCore keys v
+    d.insertCore keys v config
 
 /--
 Find keys which match the expression, or some subexpression.
@@ -36,31 +36,33 @@ Implementation: we reverse the results from `getMatch`,
 so that we return lemmas matching larger subexpressions first,
 and amongst those we return more specific lemmas first.
 -/
-partial def getSubexpressionMatches (d : DiscrTree α s) (e : Expr) : MetaM (Array α) := do
+partial def getSubexpressionMatches (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) :
+    MetaM (Array α) := do
   match e with
   | .bvar _ => return #[]
   | .forallE _ _ _ _ => forallTelescope e (fun args body => do
       args.foldlM (fun acc arg => do
-          pure <| acc ++ (← d.getSubexpressionMatches (← inferType arg)))
-        (← d.getSubexpressionMatches body).reverse)
+          pure <| acc ++ (← d.getSubexpressionMatches (← inferType arg) config))
+        (← d.getSubexpressionMatches body config).reverse)
   | .lam _ _ _ _
   | .letE _ _ _ _ _ => lambdaLetTelescope e (fun args body => do
       args.foldlM (fun acc arg => do
-          pure <| acc ++ (← d.getSubexpressionMatches (← inferType arg)))
-        (← d.getSubexpressionMatches body).reverse)
+          pure <| acc ++ (← d.getSubexpressionMatches (← inferType arg) config))
+        (← d.getSubexpressionMatches body config).reverse)
   | _ =>
-    e.foldlM (fun a f => do pure <| a ++ (← d.getSubexpressionMatches f)) (← d.getMatch e).reverse
+    e.foldlM (fun a f => do
+      pure <| a ++ (← d.getSubexpressionMatches f config)) (← d.getMatch e config).reverse
 
 variable {m : Type → Type} [Monad m]
 
 
 /-- The explicit stack of `Trie.mapArrays` -/
-private inductive Ctxt {α β s}
+private inductive Ctxt {α β}
   | empty : Ctxt
-  | ctxt : Array (Key s × Trie β s) → Array β → Array (Key s × Trie α s) → Key s → Ctxt → Ctxt
+  | ctxt : Array (Key × Trie β) → Array β → Array (Key × Trie α) → Key → Ctxt → Ctxt
 
 /-- Apply a function to the array of values at each node in a `DiscrTree`. -/
-partial def Trie.mapArrays (t : Trie α s) (f : Array α → Array β) : Trie β s :=
+partial def Trie.mapArrays (t : Trie α) (f : Array α → Array β) : Trie β :=
   let .node vs0 cs0 := t
   go (.mkEmpty cs0.size) (f vs0) cs0.reverse Ctxt.empty
 where
@@ -77,7 +79,7 @@ where
       go (.mkEmpty cs'.size) (f vs') cs'.reverse (.ctxt cs vs todo.pop k ps)
 
 /-- Apply a function to the array of values at each node in a `DiscrTree`. -/
-def mapArrays (d : DiscrTree α s) (f : Array α → Array β) : DiscrTree β s :=
+def mapArrays (d : DiscrTree α) (f : Array α → Array β) : DiscrTree β :=
   { root := d.root.map (fun t => t.mapArrays f) }
 
 end Lean.Meta.DiscrTree