...

lecopivo · Nov 4, 2024 · e46e652 · e46e652
1 parent 02807fc
commit e46e652
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/SciLean/Analysis/Diffeology/Connection.lean b/SciLean/Analysis/Diffeology/Connection.lean
@@ -57,10 +57,11 @@ instance {X : Type*} (E : X → Type*) [Diffeology X] [∀ x, Diffeology (E x)]
       · apply hp₂
 
   const_plot := by
-    intros
+    intros n xdx
     constructor
     · apply Diffeology.const_plot
-    · intros
+    · intros x₀ ht
+      simp at ht
       simp
       unfold PlotPointHomotopy.transportSection
       unfold PlotPointHomotopy.transportSection'