feat: support for lambda expressions in discr trees

src/Init/Control/Lawful/Basic.lean

@@ -49,7 +49,7 @@ attribute [simp] id_map
   (comp_map _ _ _).symm
 
 theorem Functor.map_unit [Functor f] [LawfulFunctor f] {a : f PUnit} : (fun _ => PUnit.unit) <$> a = a := by
-  simp [map]
+  rw [id_map]
 
 /--
 An applicative functor satisfies the laws of an applicative functor.

src/Init/Core.lean

@@ -1481,7 +1481,13 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
 theorem Exists.of_psigma_prop {α : Sort u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
   | ⟨x, hx⟩ => ⟨x, hx⟩
 
-protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂}
+@[simp]
+protected theorem Sigma.eta {α : Type u} {β : α → Type v} (x : Sigma β) : Sigma.mk x.1 x.2 = x := rfl
+
+@[simp]
+protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} (x : PSigma β) : PSigma.mk x.1 x.2 = x := rfl
+
+protected theorem PSigma.mk_congr {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂}
     (h₁ : a₁ = a₂) (h₂ : Eq.ndrec b₁ h₁ = b₂) : PSigma.mk a₁ b₁ = PSigma.mk a₂ b₂ := by
   subst h₁
   subst h₂
@@ -1820,8 +1826,8 @@ protected def indep (f : (a : α) → motive (Quot.mk r a)) (a : α) : PSigma mo
 protected theorem indepCoherent
     (f : (a : α) → motive (Quot.mk r a))
     (h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
-    : (a b : α) → r a b → Quot.indep f a = Quot.indep f b  :=
-  fun a b e => PSigma.eta (sound e) (h a b e)
+    : (a b : α) → r a b → Quot.indep f a = Quot.indep f b :=
+  fun a b e => PSigma.mk_congr (sound e) (h a b e)
 
 protected theorem liftIndepPr1
     (f : (a : α) → motive (Quot.mk r a))

src/Init/Data/Array/Attach.lean

@@ -135,7 +135,7 @@ theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {xs :
 theorem attach_congr {xs ys : Array α} (h : xs = ys) :
     xs.attach = ys.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
   subst h
-  simp
+  rw [map_id']
 
 theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H : ∀ x ∈ xs, P x} :
     xs.attachWith P H = ys.attachWith P fun _ h => H _ (w ▸ h) := by
@@ -340,7 +340,8 @@ theorem foldl_attach {xs : Array α} {f : β → α → β} {b : β} :
     List.length_pmap, List.foldl_toArray', mem_toArray, List.foldl_subtype]
   congr
   ext
-  simpa using fun a => List.mem_of_getElem? a
+  simp only [List.getElem?_unattach, List.getElem?_map, List.getElem?_attach, Option.map_pmap,
+    Option.pmap_eq_map, Option.map_id_fun', id_eq]
 
 /--
 If we fold over `l.attach` with a function that ignores the membership predicate,
@@ -359,7 +360,8 @@ theorem foldr_attach {xs : Array α} {f : α → β → β} {b : β} :
     List.length_pmap, List.foldr_toArray', mem_toArray, List.foldr_subtype]
   congr
   ext
-  simpa using fun a => List.mem_of_getElem? a
+  simp only [List.getElem?_unattach, List.getElem?_map, List.getElem?_attach, Option.map_pmap,
+    Option.pmap_eq_map, Option.map_id_fun', id_eq]
 
 theorem attach_map {xs : Array α} {f : α → β} :
     (xs.map f).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by

src/Init/Data/Array/MapIdx.lean

@@ -372,12 +372,12 @@ theorem mapIdx_eq_push_iff {xs : Array α} {b : β} :
     mapIdx f xs = ys.push b ↔
       ∃ (a : α) (zs : Array α), xs = zs.push a ∧ mapIdx f zs = ys ∧ f zs.size a = b := by
   rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_push_iff]
-  simp only [mapFinIdx_eq_mapIdx, exists_and_left, exists_prop]
+  simp only [mapFinIdx_eq_mapIdx, exists_prop]
   constructor
-  · rintro ⟨zs, rfl, a, rfl, rfl⟩
+  · rintro ⟨zs, a, rfl, rfl, rfl⟩
     exact ⟨a, zs, by simp⟩
   · rintro ⟨a, zs, rfl, rfl, rfl⟩
-    exact ⟨zs, rfl, a, by simp⟩
+    exact ⟨zs, a, by simp⟩
 
 @[simp] theorem mapIdx_eq_singleton_iff {xs : Array α} {f : Nat → α → β} {b : β} :
     mapIdx f xs = #[b] ↔ ∃ (a : α), xs = #[a] ∧ f 0 a = b := by

src/Init/Data/List/Attach.lean

@@ -106,7 +106,7 @@ theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {l :
 theorem attach_congr {l₁ l₂ : List α} (h : l₁ = l₂) :
     l₁.attach = l₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
   subst h
-  simp
+  rw [map_id']
 
 theorem attachWith_congr {l₁ l₂ : List α} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x} :
     l₁.attachWith P H = l₂.attachWith P fun _ h => H _ (w ▸ h) := by

src/Init/Data/List/MapIdx.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Mario Carneiro
 -/
-
 module
 
 prelude
@@ -452,12 +451,7 @@ theorem mapIdx_eq_append_iff {l : List α} :
         mapIdx f l₁' = l₁ ∧
         mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂ := by
   rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_append_iff]
-  simp only [mapFinIdx_eq_mapIdx, exists_and_left, exists_prop]
-  constructor
-  · rintro ⟨l₁, rfl, l₂, rfl, h⟩
-    refine ⟨l₁, l₂, by simp_all⟩
-  · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
-    refine ⟨l₁, rfl, l₂, by simp_all⟩
+  simp
 
 theorem mapIdx_eq_mapIdx_iff {l : List α} :
     mapIdx f l = mapIdx g l ↔ ∀ i : Nat, (h : i < l.length) → f i l[i] = g i l[i] := by

src/Init/Data/Option/Attach.lean

@@ -57,7 +57,7 @@ terminates.
 theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
     o₁.attach = o₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
   subst h
-  simp
+  rw [map_id']
 
 theorem attachWith_congr {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ x, o₁ = some x → P x} :
     o₁.attachWith P H = o₂.attachWith P fun _ h => H _ (w ▸ h) := by
@@ -177,7 +177,7 @@ theorem map_attach_eq_attachWith {o : Option α} {p : α → Prop} (f : ∀ a, o
 theorem attach_bind {o : Option α} {f : α → Option β} :
     (o.bind f).attach =
       o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, bind_eq_some_iff.2 ⟨_, h, h'⟩⟩ := by
-  cases o <;> simp
+  cases o <;> simp [Subtype.eta]
 
 theorem bind_attach {o : Option α} {f : {x // o = some x} → Option β} :
     o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩ := by

src/Init/Data/Vector/Attach.lean

@@ -129,12 +129,12 @@ theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {xs :
 theorem attach_congr {xs ys : Vector α n} (h : xs = ys) :
     xs.attach = ys.attach.map (fun x => ⟨x.1, h ▸ x.2⟩) := by
   subst h
-  simp
+  rw [map_id']
 
 theorem attachWith_congr {xs ys : Vector α n} (w : xs = ys) {P : α → Prop} {H : ∀ x ∈ xs, P x} :
     xs.attachWith P H = ys.attachWith P fun _ h => H _ (w ▸ h) := by
   subst w
-  simp
+  rfl
 
 @[simp] theorem attach_push {a : α} {xs : Vector α n} :
     (xs.push a).attach =

src/Init/Prelude.lean

@@ -16,7 +16,6 @@ This is the first file in the Lean import hierarchy. It is responsible for setti
 up basic definitions, most of which Lean already has "built in knowledge" about,
 so it is important that they be set up in exactly this way. (For example, Lean will
 use `PUnit` in the desugaring of `do` notation, or in the pattern match compiler.)
-
 -/
 
 universe u v w