From 7a32006485e96045488c2583d18d4fb58fba7ada Mon Sep 17 00:00:00 2001
From: Siegmentation Fault <siegmentationfault@yandex.ru>
Date: Tue, 10 Dec 2024 18:37:29 +0700
Subject: [PATCH] =?UTF-8?q?something=20is=20causing=20=E2=80=9Cunreachable?=
 =?UTF-8?q?=20code=20was=20reached=E2=80=9D=20error?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 GroundZero/Exercises/Chap4.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/GroundZero/Exercises/Chap4.lean b/GroundZero/Exercises/Chap4.lean
index d60e6ca..b919615 100644
--- a/GroundZero/Exercises/Chap4.lean
+++ b/GroundZero/Exercises/Chap4.lean
@@ -434,7 +434,7 @@ namespace «4.8»
   open GroundZero.Structures
   open GroundZero.Theorems
 
-  hott lemma injOutOfBoolChar {B : Type u} : (Σ (f : 𝟐 → B), injective f) ≃ (Σ (w : B × B), w.1 ≠ w.2) :=
+  noncomputable hott lemma injOutOfBoolChar {B : Type u} : (Σ (f : 𝟐 → B), injective f) ≃ (Σ (w : B × B), w.1 ≠ w.2) :=
   begin
     fapply Sigma.mk;
     { intro w; existsi (w.1 false, w.1 true);
@@ -453,7 +453,7 @@ namespace «4.8»
       { apply Theorems.funext; intro b; induction b using Bool.casesOn <;> reflexivity } }
   end
 
-  hott lemma embdOutOfBoolChar {B : Type u} :
+  noncomputable hott lemma embdOutOfBoolChar {B : Type u} :
     (𝟐 ↪ B) ≃ (Σ (w : B × B), w.1 ≠ w.2 × contr (w.1 = w.1) × contr (w.2 = w.2)) :=
   begin
     fapply Sigma.mk;