From b7dee75d5c8adb3141634205d796b997bb43fb7a Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 8 Jun 2024 03:49:34 +0200
Subject: [PATCH] Update Basic.lean

---
 HepLean/StandardModel/HiggsBoson/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean
index 840e4e7..d7167cf 100644
--- a/HepLean/StandardModel/HiggsBoson/Basic.lean
+++ b/HepLean/StandardModel/HiggsBoson/Basic.lean
@@ -81,7 +81,7 @@ lemma higgsVecToFin2ℂ_toHiggsVec (φ : higgsField) :
   higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := rfl
 
 lemma toVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, Fin 2 → ℂ) φ :=
-  smooth_higgsVecToFin2ℂ.comp  φ.toHiggsVec_smooth
+  smooth_higgsVecToFin2ℂ.comp φ.toHiggsVec_smooth
 
 lemma apply_smooth (φ : higgsField) :
     ∀ i, Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℂ) (fun (x : spaceTime) => (φ x i)) :=