update (because something changed in Lean again)

forked-from-1kasper · May 29, 2024 · 04dc591 · 04dc591
1 parent 86adb04
commit 04dc591
Show file tree

Hide file tree

Showing 11 changed files with 74 additions and 65 deletions.
diff --git a/GroundZero/Algebra/EilenbergMacLane.lean b/GroundZero/Algebra/EilenbergMacLane.lean
@@ -122,8 +122,8 @@ namespace K1
   hott definition decode (z : K1 G) : code z → base = z :=
   begin
     induction z; exact loop;
-    case loopπ x =>
-    { change _ = _; transitivity; apply Equiv.transportCharacterization;
+    { case loopπ x =>
+      change _ = _; transitivity; apply Equiv.transportCharacterization;
       apply Theorems.funext; intro y; transitivity;
       apply ap (λ p, Equiv.transport (λ x, base = x) (loop x) (loop p));
       transitivity; apply Equiv.transportToTransportconst;

diff --git a/GroundZero/Algebra/Group/Absolutizer.lean b/GroundZero/Algebra/Group/Absolutizer.lean
@@ -68,10 +68,10 @@ namespace Group
       { intros a b; apply Relquot.elem; exact G.φ (φ.ap a) (φ.ap b) };
       { apply Relquot.set };
       { intro a₁ a₂ b₁ b₂ (p : ∥_∥); induction p;
-        case elemπ p =>
-        { intro (q : ∥_∥); induction q;
-          case elemπ q =>
-          { apply Id.ap Relquot.elem; apply Equiv.bimap;
+        { case elemπ p =>
+          intro (q : ∥_∥); induction q;
+          { case elemπ q =>
+            apply Id.ap Relquot.elem; apply Equiv.bimap;
             { induction p using Sum.casesOn;
               { apply Id.ap; assumption };
               { transitivity; apply Id.ap; assumption;

diff --git a/GroundZero/Algebra/Group/Presentation.lean b/GroundZero/Algebra/Group/Presentation.lean
@@ -84,9 +84,11 @@ namespace Group
   noncomputable hott theorem abelComm : (Abelianization G).isCommutative :=
   begin
     intro (a : Relquot _) (b : Relquot _);
-    apply @commutes (Abelianization G); induction a; case elemπ a =>
-    { induction b; case elemπ b =>
-      { apply Factor.sound; intros y H; apply H.2.2; apply Merely.elem;
+    apply @commutes (Abelianization G); induction a;
+    { case elemπ a =>
+      induction b;
+      { case elemπ b =>
+        apply Factor.sound; intros y H; apply H.2.2; apply Merely.elem;
         existsi (a, b); reflexivity };
       apply Relquot.set; apply propIsSet; apply Relquot.set };
       apply Relquot.set; apply propIsSet; apply Relquot.set

diff --git a/GroundZero/Algebra/Group/Subgroup.lean b/GroundZero/Algebra/Group/Subgroup.lean
@@ -188,17 +188,20 @@ namespace Group
     Group.subgroup.mk (Algebra.im φ.1)
       (HITs.Merely.elem ⟨e, homoUnit φ⟩)
       (begin
-        intro a b (p : ∥_∥); induction p; case elemπ p =>
-        { intro (q : ∥_∥); induction q; case elemπ q =>
-          { apply HITs.Merely.elem; existsi p.1 * q.1;
+        intro a b (p : ∥_∥); induction p;
+        { case elemπ p =>
+          intro (q : ∥_∥); induction q;
+          { case elemπ q =>
+            apply HITs.Merely.elem; existsi p.1 * q.1;
             transitivity; apply homoMul; apply Equiv.bimap H.φ;
             apply p.2; apply q.2 };
           apply HITs.Merely.uniq };
         apply piProp; intro; apply HITs.Merely.uniq
       end)
       (begin
-        intro a (p : ∥_∥); induction p; case elemπ p =>
-        { apply HITs.Merely.elem; existsi p.1⁻¹;
+        intro a (p : ∥_∥); induction p;
+        { case elemπ p =>
+          apply HITs.Merely.elem; existsi p.1⁻¹;
           transitivity; apply homoInv; apply ap _ p.2 };
         apply HITs.Merely.uniq
       end)

diff --git a/GroundZero/Algebra/Reals.lean b/GroundZero/Algebra/Reals.lean
@@ -306,9 +306,9 @@ namespace GroundZero.Algebra
   noncomputable hott def doubleGeZeroImplGeZero {x : ℝ} : R.ρ 0 (x + x) → R.ρ 0 x :=
   begin
     intro p; induction R.total 0 x;
-    case inl q₁ => { apply q₁ };
-    case inr q₂ =>
-    { apply explode; apply (strictIneqAdd R q₂ q₂).1;
+    { case inl q₁ => apply q₁ };
+    { case inr q₂ =>
+      apply explode; apply (strictIneqAdd R q₂ q₂).1;
       apply @antisymmetric.asymm R.κ; apply ineqAdd <;> exact q₂.2;
       apply Equiv.transport (R.ρ · (x + x)); symmetry; apply R.τ⁺.mulOne; exact p }
   end

diff --git a/GroundZero/Exercises/Chap3.lean b/GroundZero/Exercises/Chap3.lean
@@ -386,8 +386,8 @@ namespace «3.18»
   begin
     apply Prod.mk; intro lem P H nnp;
     induction lem P H using Sum.casesOn;
-    case inl p  => { exact p };
-    case inr np => { apply explode (nnp np) };
+    { case inl p  => exact p };
+    { case inr np => apply explode (nnp np) };
 
     intro dneg P H; apply dneg; apply propEM H; intro npnp;
     apply npnp; right; intro p; apply npnp; left; exact p
@@ -417,20 +417,20 @@ namespace «3.19»
   hott lemma BSP (n m : ℕ) : P (n + m) → P (BSA G n m) :=
   begin
     intro h; induction m using Nat.casesOn;
-    case zero   => { exact h };
-    case succ m => { show P (Coproduct.elim _ _ _); induction G n using Sum.casesOn;
-                     case inl p  => { exact p };
-                     case inr np => { apply BSP (Nat.succ n) m;
+    { case zero   => exact h };
+    { case succ m => show P (Coproduct.elim _ _ _); induction G n using Sum.casesOn;
+                     { case inl p  => exact p };
+                     { case inr np => apply BSP (Nat.succ n) m;
                                       exact transport P (Nat.succPlus n m)⁻¹ h }; };
   end
 
   hott lemma minimality (n m k : ℕ) : P k → n ≤ k → BSA G n m ≤ k :=
   begin
     intro pk h; induction m using Nat.casesOn;
-    case zero   => { exact h };
-    case succ m => { show Coproduct.elim _ _ _ ≤ _; induction G n using Sum.casesOn;
-                     case inl p  => { exact h };
-                     case inr np => { apply minimality (Nat.succ n) m k pk;
+    { case zero   => exact h };
+    { case succ m => show Coproduct.elim _ _ _ ≤ _; induction G n using Sum.casesOn;
+                     { case inl p  => exact h };
+                     { case inr np => apply minimality (Nat.succ n) m k pk;
                                       apply Nat.le.neqSucc;
                                       { intro ω; apply np; apply transport P;
                                         symmetry; apply ap Nat.pred ω; exact pk };
@@ -457,20 +457,20 @@ namespace «3.19»
   hott lemma upperEstimate (n m : ℕ) : BSA G n m ≤ n + m :=
   begin
     induction m using Nat.casesOn;
-    case zero   => { apply Nat.max.refl };
-    case succ m => { show Coproduct.elim _ _ _ ≤ _; induction G n using Sum.casesOn;
-                     case inl p  => { apply Nat.le.addl Nat.zero; apply Nat.max.zeroLeft };
-                     case inr np => { apply transport (_ ≤ ·); apply Nat.succPlus;
+    { case zero   => apply Nat.max.refl };
+    { case succ m => show Coproduct.elim _ _ _ ≤ _; induction G n using Sum.casesOn;
+                     { case inl p  => apply Nat.le.addl Nat.zero; apply Nat.max.zeroLeft };
+                     { case inr np => apply transport (_ ≤ ·); apply Nat.succPlus;
                                       apply upperEstimate (Nat.succ n) m } }
   end
 
   hott lemma lowerEstimate (n m : ℕ) : n ≤ BSA G n m :=
   begin
     induction m using Nat.casesOn;
-    case zero   => { apply Nat.max.refl };
-    case succ m => { show _ ≤ Coproduct.elim _ _ _; induction G n using Sum.casesOn;
-                     case inl p  => { apply Nat.max.refl };
-                     case inr np => { apply Nat.le.trans; apply Nat.le.succ;
+    { case zero   => apply Nat.max.refl };
+    { case succ m => show _ ≤ Coproduct.elim _ _ _; induction G n using Sum.casesOn;
+                     { case inl p  => apply Nat.max.refl };
+                     { case inr np => apply Nat.le.trans; apply Nat.le.succ;
                                       apply lowerEstimate (Nat.succ n) m } }
   end
 end «3.19»
@@ -521,26 +521,26 @@ namespace «3.23»
   hott definition decMerely.elem {A : Type u} (G : dec A) : A → decMerely G :=
   begin
     intro x; induction G using Sum.casesOn;
-    case inl y => { existsi y; apply idp };
-    case inr φ => { apply explode (φ x) }
+    { case inl y => existsi y; apply idp };
+    { case inr φ => apply explode (φ x) }
   end
 
   hott definition decMerely.uniq {A : Type u} (G : dec A) : prop (decMerely G) :=
   begin
     induction G using Sum.casesOn;
-    case inl _ => { intro w₁ w₂; fapply Sigma.prod;
+    { case inl _ => intro w₁ w₂; fapply Sigma.prod;
                     { transitivity; apply w₁.2; symmetry; apply w₂.2 };
                     { transitivity; apply transportCompositionRev;
                       apply Equiv.rewriteComp; symmetry;
                       apply Id.cancelInvComp } };
-    case inr φ => { intro w₁ w₂; apply explode (φ w₁.1) }
+    { case inr φ => intro w₁ w₂; apply explode (φ w₁.1) }
   end
 
   hott definition decMerely.dec {A : Type u} (G : dec A) : dec (@decMerely A G) :=
   begin
     induction G using Sum.casesOn;
-    case inl x => { left; existsi x; apply idp };
-    case inr φ => { right; intro w; apply φ w.1 }
+    { case inl x => left; existsi x; apply idp };
+    { case inr φ => right; intro w; apply φ w.1 }
   end
 
   -- so for decidable type propositional truncation can be constructed explicitly (i.e. without HITs)

diff --git a/GroundZero/HITs/Reals.lean b/GroundZero/HITs/Reals.lean
@@ -136,8 +136,8 @@ namespace Reals
   noncomputable hott lemma helixOverCis (x : R) : helix (cis x) = ℤ :=
   begin
     induction x;
-    case cz x => { apply (Integer.shift x)⁻¹ };
-    case sz z => {
+    { case cz x => apply (Integer.shift x)⁻¹ };
+    { case sz z =>
       change _ = _; let p := Integer.shift z; apply calc
             Equiv.transport (λ x, helix (cis x) = ℤ) (glue z) (Integer.shift z)⁻¹
           = @ap R Type _ _ (helix ∘ cis) (glue z)⁻¹ ⬝ (Integer.shift z)⁻¹ :

diff --git a/GroundZero/Structures.lean b/GroundZero/Structures.lean
@@ -165,10 +165,9 @@ noncomputable hott corollary hlevel.strongCumulative (n m : hlevel) (ρ : n ≤
   Π {A : Type u}, (is-n-type A) → (is-m-type A) :=
 begin
   induction ρ; intros; assumption;
-  case step m ρ ih => {
+  { case step m ρ ih =>
     intros A G; apply @hlevel.cumulative;
-    apply ih; assumption
-  }
+    apply ih; assumption }
 end
 
 hott definition isTruncated {A : Type u} {B : Type v} (n : ℕ₋₂) (f : A → B) :=

diff --git a/GroundZero/Theorems/Classical.lean b/GroundZero/Theorems/Classical.lean
@@ -54,26 +54,29 @@ section
   noncomputable hott theorem lem {A : Type u} (H : prop A) : A + ¬A :=
   begin
     have f := @choiceOfRel inh 𝟐 (λ φ x, φ.fst x) inh.hset boolIsSet (λ x, HITs.Merely.lift id x.2);
-    induction f; case elemπ w =>
-    { let ⟨φ, p⟩ := w;
+    induction f;
+    { case elemπ w =>
+      let ⟨φ, p⟩ := w;
       let U : 𝟐 → Prop := λ x, ⟨∥(x = true) + A∥,  HITs.Merely.uniq⟩;
       let V : 𝟐 → Prop := λ x, ⟨∥(x = false) + A∥, HITs.Merely.uniq⟩;
       have r : ∥_∥ := p ⟨U, HITs.Merely.elem ⟨true,  HITs.Merely.elem (Sum.inl (idp _))⟩⟩;
       have s : ∥_∥ := p ⟨V, HITs.Merely.elem ⟨false, HITs.Merely.elem (Sum.inl (idp _))⟩⟩;
-      induction r; case elemπ r' =>
-      { induction s; case elemπ s' =>
-        { induction r' using Sum.casesOn;
-          case inl r' =>
-          { induction s' using Sum.casesOn;
-            case inl s' =>
-            { right; intro z; apply ffNeqTt;
+      induction r;
+      { case elemπ r' =>
+        induction s;
+        { case elemπ s' =>
+          induction r' using Sum.casesOn;
+          { case inl r' =>
+            induction s' using Sum.casesOn;
+            { case inl s' =>
+              right; intro z; apply ffNeqTt;
               transitivity; exact s'⁻¹; symmetry; transitivity; exact r'⁻¹;
               apply ap; fapply Types.Sigma.prod; apply Theorems.funext;
               intro x; apply Theorems.Equiv.propset.Id; apply propext;
               apply HITs.Merely.uniq; apply HITs.Merely.uniq; apply Prod.mk <;>
               intro <;> apply HITs.Merely.elem <;> right <;> exact z; apply HITs.Merely.uniq };
-            case inr => { left; assumption } };
-          case inr => { left; assumption } };
+            { case inr => left; assumption } };
+          { case inr => left; assumption } };
         apply propEM H };
       apply propEM H };
     apply propEM H

diff --git a/GroundZero/Theorems/Connectedness.lean b/GroundZero/Theorems/Connectedness.lean
@@ -35,8 +35,9 @@ namespace Connectedness
     apply Prod.mk;
     { fapply Trunc.ind;
       { intro y; transitivity; apply ap (Trunc.ap _);
-        apply Trunc.recβrule; induction (c y).1; case elemπ w =>
-        { transitivity; apply ap (Trunc.ap f); apply Trunc.recβrule;
+        apply Trunc.recβrule; induction (c y).1;
+        { case elemπ w =>
+          transitivity; apply ap (Trunc.ap f); apply Trunc.recβrule;
           transitivity; apply Trunc.recβrule; apply ap Trunc.elem; exact w.2 };
         { apply hlevel.cumulative; apply Trunc.uniq } };
       { intro; apply hlevel.cumulative; apply Trunc.uniq } };
@@ -63,8 +64,9 @@ namespace Connectedness
     { intro s; apply Theorems.funext; intro a; transitivity;
       apply ap (Trunc.rec _ _); apply (c (f a)).2; apply Trunc.elem;
       exact ⟨a, idp (f a)⟩; apply Trunc.recβrule };
-    { intro s; apply Theorems.funext; intro b; induction (c b).1; case elemπ w =>
-      { transitivity; apply ap (Trunc.rec _ _); apply (c b).2 (Trunc.elem w);
+    { intro s; apply Theorems.funext; intro b; induction (c b).1;
+      { case elemπ w =>
+        transitivity; apply ap (Trunc.rec _ _); apply (c b).2 (Trunc.elem w);
         transitivity; apply Trunc.recβrule; apply apd s w.2 };
       { apply hlevel.cumulative; apply (P b).2 } }
   end

diff --git a/GroundZero/Theorems/Functions.lean b/GroundZero/Theorems/Functions.lean
@@ -31,8 +31,8 @@ hott definition cut {A : Type u} {B : Type v} (f : A → B) : A → Ran f :=
 hott lemma cutIsSurj {A : Type u} {B : Type v} (f : A → B) : surjective (cut f) :=
 begin
   intro ⟨x, (H : ∥_∥)⟩; induction H;
-  case elemπ G =>
-  { apply Merely.elem; existsi G.1; fapply Sigma.prod;
+  { case elemπ G =>
+    apply Merely.elem; existsi G.1; fapply Sigma.prod;
     exact G.2; apply Merely.uniq };
   apply Merely.uniq
 end
@@ -58,8 +58,8 @@ hott lemma ranConstEqv {A : Type u} (a : A) {B : Type v}
 begin
   existsi (λ _, ★); fapply Prod.mk <;> existsi (λ _, ranConst a b);
   { intro ⟨b', (G : ∥_∥)⟩; fapply Sigma.prod; change b = b';
-    induction G; case elemπ w => { exact w.2 }; apply H;
-    apply Merely.uniq };
+    induction G; { case elemπ w => exact w.2 };
+    apply H; apply Merely.uniq };
   { intro ★; reflexivity }
 end