feat: reduce s.1 =?= v to s =?= ⟨v⟩ if structure has a single field

This feature was suggested by @dselsam at PR #521.
It closes #509

src/Lean/Meta/ExprDefEq.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.ProjFns
+import Lean.Structure
 import Lean.Meta.WHNF
 import Lean.Meta.InferType
 import Lean.Meta.FunInfo
@@ -1355,7 +1356,21 @@ private def isDefEqOnFailure (t s : Expr) : MetaM Bool :=
 
 private def isDefEqProj : Expr → Expr → MetaM Bool
   | Expr.proj _ i t _, Expr.proj _ j s _ => pure (i == j) <&&> Meta.isExprDefEqAux t s
+  | Expr.proj structName 0 s _, v => isDefEqSingleton structName s v
+  | v, Expr.proj structName 0 s _ => isDefEqSingleton structName s v
   | _, _ => pure false
+where
+  /- If `structName` is a structure with a single field, then reduce `s.1 =?= v` to `s =?= ⟨v⟩` -/
+  isDefEqSingleton (structName : Name) (s : Expr) (v : Expr) : MetaM Bool := do
+    let ctorVal := getStructureCtor (← getEnv) structName
+    if ctorVal.numFields != 1 then
+      return false -- It is not a structure with a single field.
+    let sType ← whnf (← inferType s)
+    let sTypeFn := sType.getAppFn
+    if !sTypeFn.isConstOf structName then
+      return false
+    let ctorApp := mkApp (mkAppN (mkConst ctorVal.name sTypeFn.constLevels!) sType.getAppArgs) v
+    Meta.isExprDefEqAux s ctorApp
 
 /-
   Given applications `t` and `s` that are in WHNF (modulo the current transparency setting),

tests/lean/run/509.lean

@@ -0,0 +1,34 @@
+class has_note (M : Type) where
+  note : M
+
+notation "♩" => has_note.note
+
+class has_note2 (M : Type) extends has_note M
+
+variable {ι : Type} (β : ι → Type)
+
+structure foo [∀ i, has_note (β i)] : Type where
+  to_fun : ∀ i, β i
+
+instance foo.has_note [∀ i, has_note (β i)] : has_note (foo (λ i => β i)) where
+  note := { to_fun := λ _ => ♩ }
+
+instance foo.has_note2 [∀ i, has_note2 (β i)] : has_note2 (foo (λ i => β i)) where
+  note := ♩
+
+variable (α : Type) (M : Type)
+
+structure bar [has_note M] where
+  to_fun : α → M
+
+instance bar.has_note [has_note M] : has_note (bar α M) where
+  note := { to_fun := λ _ => ♩ }
+
+instance bar.has_note2 [has_note2 M] : has_note2 (bar α M) where
+  note := ♩
+
+example [has_note2 M] : has_note2 (foo (λ (i : ι) => bar (β i) M)) :=
+inferInstance
+
+example [has_note2 M] : has_note2 (foo (λ (i : ι) => bar (β i) M)) :=
+foo.has_note2 _