fix test

Author: Rob23oba

tests/lean/815b.lean.expected.out

@@ -24,7 +24,7 @@
         Transformer
           fun redf a => redf
     [Meta.synthInstance] new goal IsSmooth f
-      [Meta.synthInstance.instances] #[inst✝]
+      [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
   [Meta.synthInstance] ✅️ apply inst✝ to IsSmooth f
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth f ≟ IsSmooth f
     [Meta.synthInstance.answer] ✅️ IsSmooth f
@@ -44,17 +44,75 @@
         Transformer
           fun redf a => redf
     [Meta.synthInstance] new goal ∀ (b : β), IsSmooth (f b)
-      [Meta.synthInstance.instances] #[inst✝]
+      [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
   [Meta.synthInstance] ❌️ apply inst✝ to ∀ (b : β), IsSmooth (f b)
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth (f b) ≟ IsSmooth f
+  [Meta.synthInstance] ✅️ apply @diag to ∀ (b : β), IsSmooth (f b)
+    [Meta.synthInstance.tryResolve] ✅️ IsSmooth (f b) ≟ IsSmooth fun a => f b a
+    [Meta.synthInstance.unusedArgs] ∀ (b : β), IsSmooth f
+        has unused arguments, reduced type
+          IsSmooth f
+        Transformer
+          fun redf b => redf
+  [Meta.synthInstance.resume] propagating ∀ (b : β),
+        IsSmooth f to subgoal ∀ (b : β), IsSmooth f of ∀ (b : β), IsSmooth (f b)
+    [Meta.synthInstance.resume] size: 1
+    [Meta.synthInstance.unusedArgs] ∀ (b b : β), IsSmooth (f b)
+        has unused arguments, reduced type
+          ∀ (b : β), IsSmooth (f b)
+        Transformer
+          fun redf b => redf
+  [Meta.synthInstance] ✅️ apply @comp to ∀ (b : β), IsSmooth (f b)
+    [Meta.synthInstance.tryResolve] ✅️ IsSmooth (f b) ≟ IsSmooth fun a => f b a
+  [Meta.synthInstance] ❌️ apply @parm to ∀ (b : β), IsSmooth (f b)
+    [Meta.synthInstance.tryResolve] ❌️ IsSmooth (f b) ≟ IsSmooth fun a => ?m b a (?m b)
+  [Meta.synthInstance] ❌️ apply @const to ∀ (b : β), IsSmooth (f b)
+    [Meta.synthInstance.tryResolve] ❌️ IsSmooth (f b) ≟ IsSmooth fun a => ?m b
+  [Meta.synthInstance] ❌️ apply @identity to ∀ (b : β), IsSmooth (f b)
+    [Meta.synthInstance.tryResolve] ❌️ IsSmooth (f b) ≟ IsSmooth fun a => a
   [Meta.synthInstance] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a) d
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
   [Meta.synthInstance] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => f (g a) d
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
     [Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a)
-      [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
+      [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
   [Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a)
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) ≟ IsSmooth f
+  [Meta.synthInstance] ✅️ apply @swap to ∀ (a : α), IsSmooth fun g => f (g a)
+    [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) ≟ IsSmooth fun b a_1 => f (b a) a_1
+    [Meta.synthInstance] new goal ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+      [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
+  [Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth f
+  [Meta.synthInstance] ✅️ apply @diag to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
+    [Meta.synthInstance.unusedArgs] ∀ (a : α) (a : δ), IsSmooth f
+        has unused arguments, reduced type
+          IsSmooth f
+        Transformer
+          fun redf a a => redf
+  [Meta.synthInstance.resume] propagating ∀ (a : α) (a : δ),
+        IsSmooth f to subgoal ∀ (a : α) (a : δ), IsSmooth f of ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.resume] size: 1
+    [Meta.synthInstance.unusedArgs] ∀ (a : α) (a : δ) (b : β), IsSmooth (f b)
+        has unused arguments, reduced type
+          ∀ (b : β), IsSmooth (f b)
+        Transformer
+          fun redf a a => redf
+  [Meta.synthInstance] ❌️ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g =>
+          f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
+  [Meta.synthInstance] ✅️ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
+    [Meta.synthInstance.unusedArgs] ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a)
+        has unused arguments, reduced type
+          ∀ (a : α), IsSmooth fun g => f (g a)
+        Transformer
+          fun redf a a_1 => redf a
+  [Meta.synthInstance] ❌️ apply @const to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a
+  [Meta.synthInstance] ❌️ apply @identity to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a => a
   [Meta.synthInstance] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a)
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g =>
           f (g a) ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)