fix proof in diffeology on Array

lecopivo · Nov 5, 2024 · 0176741 · 0176741
1 parent b952a2e
commit 0176741
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/SciLean/Analysis/Diffeology/Array.lean b/SciLean/Analysis/Diffeology/Array.lean
@@ -106,8 +106,7 @@ theorem fixSize_arrayN_data [Nonempty α] (f : α → ArrayN β n) :
     fixSize (fun x => (f x).data) = fun x => cast (by simp) (f x) := by
   simp[fixSize]
   funext a
-  sorry
-
+  rw[← cast_arrayN_mk]
 
 @[fun_prop]
 theorem cast_clm