From 776bce19fe9b6b6a803502fbc4a41453fee12262 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 8 Jun 2024 03:53:42 +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 d7167cf..39e2c73 100644
--- a/HepLean/StandardModel/HiggsBoson/Basic.lean
+++ b/HepLean/StandardModel/HiggsBoson/Basic.lean
@@ -75,7 +75,7 @@ lemma toHiggsVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ
   exact h1
 
 lemma toField_toHiggsVec_apply (φ : higgsField) (x : spaceTime) :
-    (φ.toHiggsVec x).toField x = φ x := rfl
+  (φ.toHiggsVec x).toField x = φ x := rfl
 
 lemma higgsVecToFin2ℂ_toHiggsVec (φ : higgsField) :
   higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := rfl