feat: enable backward.isDefEq.respectTransparency.types by default

src/Init/BinderNameHint.lean

@@ -43,6 +43,6 @@ It is ineffective in other positions (hypotheses of rewrite rules) or when used
 (e.g. `apply`).
 -/
 /- One might expect/hope that this was `implicit_reducible` rather than `instance_reducible`.
-Currently, there is a failure in `tests/elab/binderNameHintSimp.lean` if we make this change. -/
+Currently, the test `tests/elab/binderNameHintSimp.lean` fails (in a stage 2 build) if we make this change. -/
 @[simp ↓, expose, instance_reducible]
 def binderNameHint {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ) : γ := e

src/Init/Control/Except.lean

@@ -128,7 +128,7 @@ end Except
 /--
 Adds exceptions of type `ε` to a monad `m`.
 -/
-def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
+@[implicit_reducible] def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
   m (Except ε α)
 
 /--

src/Init/Control/ExceptCps.lean

@@ -21,7 +21,7 @@ Adds exceptions of type `ε` to a monad `m`.
 Instead of using `Except ε` to model exceptions, this implementation uses continuation passing
 style. This has different performance characteristics from `ExceptT ε`.
 -/
-@[expose] def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
+@[expose, instance_reducible] def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
 
 namespace ExceptCpsT
 

src/Init/Control/Id.lean

@@ -36,7 +36,7 @@ def containsFive (xs : List Nat) : Bool := Id.run do
 true
 ```
 -/
-@[expose] def Id (type : Type u) : Type u := type
+@[expose, implicit_reducible] def Id (type : Type u) : Type u := type
 
 namespace Id
 
@@ -60,7 +60,7 @@ This function is the identity function. Because its parameter has type `Id α`,
 `do`-notation in its arguments to use the `Monad Id` instance.
 -/
 /- One might expect/hope that this was `implicit_reducible` rather than `instance_reducible`.
-Currently, there is a failure in `Init/Data/Iterators/Lemmas/Consumers/Loop.lean` if we make this change. -/
+Currently, the stage 2 build fails in `Init/Data/Iterators/Lemmas/Consumers/Loop.lean` if we make this change. -/
 @[always_inline, inline, expose, instance_reducible]
 protected def run (x : Id α) : α := x
 

src/Init/Control/Lawful/MonadLift/Instances.lean

@@ -103,11 +103,11 @@ namespace StateRefT'
 instance {ω σ : Type} {m : Type → Type} [Monad m] : LawfulMonadLift m (StateRefT' ω σ m) where
   monadLift_pure _ := by
     simp only [MonadLift.monadLift, pure]
-    unfold StateRefT'.lift instMonad._aux_5 ReaderT.pure
+    unfold StateRefT'.lift ReaderT.pure
     simp only
   monadLift_bind _ _ := by
     simp only [MonadLift.monadLift, bind]
-    unfold StateRefT'.lift instMonad._aux_13 ReaderT.bind
+    unfold StateRefT'.lift ReaderT.bind
     simp only
 
 end StateRefT'

src/Init/Control/Option.lean

@@ -21,7 +21,7 @@ instance : ToBool (Option α) := ⟨Option.isSome⟩
 Adds the ability to fail to a monad. Unlike ordinary exceptions, there is no way to signal why a
 failure occurred.
 -/
-@[expose] def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
+@[expose, implicit_reducible] def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
   m (Option α)
 
 /--

src/Init/Control/State.lean

@@ -22,7 +22,7 @@ Adds a mutable state of type `σ` to a monad.
 Actions in the resulting monad are functions that take an initial state and return, in `m`, a tuple
 of a value and a state.
 -/
-@[expose] def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+@[expose, implicit_reducible] def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
   σ → m (α × σ)
 
 /--

src/Init/Control/StateCps.lean

@@ -21,7 +21,7 @@ The State monad transformer using CPS style.
 An alternative implementation of a state monad transformer that internally uses continuation passing
 style instead of tuples.
 -/
-@[expose] def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
+@[expose, implicit_reducible] def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
 
 namespace StateCpsT
 

src/Init/Control/StateRef.lean

@@ -20,7 +20,7 @@ A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref ω σ`
 
 The macro `StateRefT σ m α` infers `ω` from `m`. It should normally be used instead.
 -/
-@[expose] def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
+@[expose, instance_reducible] def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
 
 /-! Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/
 

src/Init/Core.lean

@@ -769,7 +769,7 @@ the `BEq` typeclass.
 Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead of
 `Prop` valued. It is mainly intended for programming applications.
 -/
-@[inline] def bne {α : Type u} [BEq α] (a b : α) : Bool :=
+@[inline, implicit_reducible] def bne {α : Type u} [BEq α] (a b : α) : Bool :=
   !(a == b)
 
 @[inherit_doc] infix:50 " != " => bne
@@ -1331,7 +1331,7 @@ def Subrelation {α : Sort u} (q r : α → α → Prop) :=
 The inverse image of `r : β → β → Prop` by a function `α → β` is the relation
 `s : α → α → Prop` defined by `s a b = r (f a) (f b)`.
 -/
-def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) : α → α → Prop :=
+@[implicit_reducible] def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) : α → α → Prop :=
   fun a₁ a₂ => r (f a₁) (f a₂)
 
 /--
@@ -1478,7 +1478,7 @@ Examples:
  * `(1, 2).map (· + 1) (· * 3) = (2, 6)`
  * `(1, 2).map toString (· * 3) = ("1", 6)`
 -/
-def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
+@[implicit_reducible] def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
     (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
   | (a, b) => (f a, g b)
 
@@ -1983,6 +1983,7 @@ must respect `s.r`. `Quotient.lift` allows values in a quotient to be mapped to
 as the mapping respects `s.r`.
 
 -/
+@[implicit_reducible]
 protected def mk' {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
   Quotient.mk s a
 

src/Init/Data/Array/Attach.lean

@@ -162,6 +162,10 @@ theorem pmap_eq_map_attach {p : α → Prop} {f : ∀ a, p a → β} {xs : Array
   cases xs
   simp [List.pmap_eq_map_attach]
 
+theorem attachWith_eq_map_attach {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a} :
+    xs.attachWith P H = xs.attach.map fun ⟨x, h⟩ => ⟨x, H _ h⟩ := by
+  cases xs <;> simp_all [List.attachWith_eq_map_attach]
+
 @[simp]
 theorem pmap_eq_attachWith {p q : α → Prop} {f : ∀ a, p a → q a} {xs : Array α} (H) :
     pmap (fun a h => ⟨a, f a h⟩) xs H = xs.attachWith q (fun x h => f x (H x h)) := by

src/Init/Data/Array/Basic.lean

@@ -90,7 +90,10 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by
 
 @[simp, grind =] theorem toArray_toList {xs : Array α} : xs.toList.toArray = xs := rfl
 
-@[simp, grind =] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs.toList[i] = xs[i] := rfl
+-- TODO: Ideally we'd use `xs[i]'(id h)` to avoid defeq abuse, but then
+-- `simp only [← getElem_toList]` won't work. For now, the solution is to make `Array.size`
+-- implicit-reducible.
+@[simp, grind =] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.toList.length) : xs.toList[i] = xs[i] := rfl
 
 @[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
   simp only [getElem?_def, getElem_toList]
@@ -170,7 +173,7 @@ Low-level indexing operator which is as fast as a C array read.
 
 This avoids overhead due to unboxing a `Nat` used as an index.
 -/
-@[extern "lean_array_uget", simp, expose]
+@[extern "lean_array_uget", simp, expose, implicit_reducible]
 def uget (xs : @& Array α) (i : USize) (h : i.toNat < xs.size) : α :=
   xs[i.toNat]
 
@@ -189,7 +192,7 @@ in-place when the reference to the array is unique.
 
 This avoids overhead due to unboxing a `Nat` used as an index.
 -/
-@[extern "lean_array_uset", expose]
+@[extern "lean_array_uset", expose, implicit_reducible]
 def uset (xs : Array α) (i : USize) (v : α) (h : i.toNat < xs.size) : Array α :=
   xs.set i.toNat v h
 

src/Init/Data/Array/DecidableEq.lean

@@ -76,6 +76,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) :
     simpa [isEqv_iff_rel] using h'
 
 @[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
+  -- rfl is necessary because `Array.getInternal isn't instance-reducible
   simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]; rfl
 
 theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by
@@ -154,6 +155,7 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) :
   simp [BEq.beq, isEqv_eq_decide]
 
 @[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
+  -- rfl is necessary because `Array.getInternal isn't instance-reducible
   simp [beq_eq_decide, List.beq_eq_decide, Array.size]; rfl
 
 end Array

src/Init/Data/Array/FinRange.lean

@@ -26,7 +26,7 @@ Examples:
  * `Array.finRange 0 = (#[] : Array (Fin 0))`
  * `Array.finRange 2 = (#[0, 1] : Array (Fin 2))`
 -/
-protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i
+@[expose, instance_reducible] protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i
 
 @[simp, grind =] theorem size_finRange {n} : (Array.finRange n).size = n := by
   simp [Array.finRange]

src/Init/Data/Array/Lemmas.lean

@@ -1872,7 +1872,7 @@ theorem getElem_of_append {xs ys zs : Array α} (eq : xs = ys.push a ++ zs) (h :
   rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h]
   simp
 
-@[simp] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := rfl
+@[simp] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := (rfl)
 
 @[simp] theorem append_singleton_assoc {a : α} {xs ys : Array α} : xs ++ (#[a] ++ ys) = xs.push a ++ ys := by
   rw [← append_assoc, append_singleton]
@@ -2833,9 +2833,8 @@ theorem getElem_extract_aux {xs : Array α} {start stop : Nat} (h : i < (xs.extr
 
 @[simp, grind =] theorem getElem_extract {xs : Array α} {start stop : Nat}
     (h : i < (xs.extract start stop).size) :
-    (xs.extract start stop)[i] = xs[start + i]'(getElem_extract_aux h) :=
-  show (extract.loop xs (min stop xs.size - start) start #[])[i]
-    = xs[start + i]'(getElem_extract_aux h) by rw [getElem_extract_loop_ge]; rfl; exact Nat.zero_le _
+    (xs.extract start stop)[i] = xs[start + i]'(getElem_extract_aux h) := by
+  simp [extract, getElem_extract_loop_ge]
 
 theorem getElem?_extract {xs : Array α} {start stop : Nat} :
     (xs.extract start stop)[i]? = if i < min stop xs.size - start then xs[start + i]? else none := by