Restructure proofs for readability

Author: alvinylt

IrisMath/IrisMath/StepIndex.lean

@@ -22,19 +22,22 @@ instance ordinalSIdx : SIdx Ordinal where
   lt_trans := lt_trans
   lt_wf := Ordinal.lt_wf
   lt_trichotomyT n m :=
-    if h : n < m then .inl h
-    else if h' : m < n then .inr <| .inr h'
-    else .inr <| .inl <| le_antisymm (not_lt.mp h') (not_lt.mp h)
+    if h : n < m then by left; exact h
+    else if h' : m < n then by right; right; exact h'
+    else by right; left; exact le_antisymm (not_lt.mp h') (not_lt.mp h)
   le_lteq := le_iff_lt_or_eq
   not_lt_zero _ := by simp
   lt_succ_self := Order.lt_succ
   succ_le_of_lt := Order.succ_le_of_lt
   weak_case n :=
     letI : Decidable (∃ m, n = Order.succ m) := Classical.propDecidable _
-    if h : ∃ m, n = Order.succ m then
-      .inl ⟨h.choose, h.choose_spec⟩
-    else
-      .inr fun m hm => lt_of_le_of_ne (Order.succ_le_of_lt hm) fun he => h ⟨m, he.symm⟩
+    if h : ∃ m, n = Order.succ m then by left; exact ⟨h.choose, h.choose_spec⟩
+    else by
+      right; intro m hm
+      apply lt_of_le_of_ne
+      · exact Order.succ_le_of_lt hm
+      · intro he
+        exact h ⟨m, he.symm⟩
 
 @[reducible]
 def ordinalSubtypeSIdx (κ : Ordinal) (hκ : Order.IsSuccLimit κ) :
@@ -46,9 +49,9 @@ def ordinalSubtypeSIdx (κ : Ordinal) (hκ : Order.IsSuccLimit κ) :
   lt_trans := lt_trans
   lt_wf := InvImage.wf Subtype.val Ordinal.lt_wf
   lt_trichotomyT n m :=
-    if h : n < m then .inl h
-    else if h' : m < n then .inr <| .inr h'
-    else .inr <| .inl <| le_antisymm (not_lt.mp h') (not_lt.mp h)
+    if h : n < m then by left; exact h
+    else if h' : m < n then by right; right; exact h'
+    else by right; left; exact le_antisymm (not_lt.mp h') (not_lt.mp h)
   le_lteq := le_iff_lt_or_eq
   not_lt_zero n :=
     show ¬n.val < 0
@@ -58,15 +61,17 @@ def ordinalSubtypeSIdx (κ : Ordinal) (hκ : Order.IsSuccLimit κ) :
     change Order.succ n.val ≤ m.val
     simpa
   weak_case n :=
-    letI : Decidable (∃ m, n = (fun o : { o // o < κ } =>
-        ⟨Order.succ o.val, hκ.succ_lt o.property⟩) m) :=
-      Classical.propDecidable _
-    if h : ∃ m, n = (fun o => ⟨Order.succ o.val, hκ.succ_lt o.property⟩) m then
-      .inl ⟨h.choose, h.choose_spec⟩
-    else
-      .inr fun m hm =>
-        lt_of_le_of_ne (Order.succ_le_of_lt hm : Order.succ m.val ≤ n.val)
-          fun he => h ⟨m, he.symm⟩
+    let succFn : {o : Ordinal // o < κ} → {o : Ordinal // o < κ} :=
+      fun o => ⟨Order.succ o.val, hκ.succ_lt o.property⟩
+    letI : Decidable (∃ m, n = succFn m) := Classical.propDecidable _
+    if h : ∃ m, n = succFn m then by
+      left; exact ⟨h.choose, h.choose_spec⟩
+    else by
+      right; intro m hm
+      apply lt_of_le_of_ne
+      · exact (Order.succ_le_of_lt hm : Order.succ m.val ≤ n.val)
+      · intro he
+        exact h ⟨m, he.symm⟩
 
 @[reducible]
 def ordinalToTypeSIdx (κ : Ordinal) (hκ : Order.IsSuccLimit κ) : SIdx κ.ToType :=
@@ -83,20 +88,23 @@ def ordinalToTypeSIdx (κ : Ordinal) (hκ : Order.IsSuccLimit κ) : SIdx κ.ToTy
     lt_trans := lt_trans
     lt_wf := wellFounded_lt
     lt_trichotomyT n m :=
-      if h : n < m then .inl h
-      else if h' : m < n then .inr <| .inr h'
-      else .inr <| .inl <| le_antisymm (not_lt.mp h') (not_lt.mp h)
+      if h : n < m then by left; exact h
+      else if h' : m < n then by right; right; exact h'
+      else by right; left; exact le_antisymm (not_lt.mp h') (not_lt.mp h)
     le_lteq := le_iff_lt_or_eq
     not_lt_zero _ := not_lt_bot
     lt_succ_self := Order.lt_succ
     succ_le_of_lt := Order.succ_le_of_lt
     weak_case n :=
       letI : Decidable (∃ m, n = Order.succ m) := Classical.propDecidable _
-      if h : ∃ m, n = Order.succ m then
-        .inl ⟨h.choose, h.choose_spec⟩
-      else
-        .inr fun m hm =>
-          lt_of_le_of_ne (Order.succ_le_of_lt hm) fun he => h ⟨m, he.symm⟩
+      if h : ∃ m, n = Order.succ m then by
+        left; exact ⟨h.choose, h.choose_spec⟩
+      else by
+        right; intro m hm
+        apply lt_of_le_of_ne
+        · exact Order.succ_le_of_lt hm
+        · intro he
+          exact h ⟨m, he.symm⟩
   }
 
 theorem limit_iff_isSuccLimit {o : Ordinal} : SIdx.Limit o ↔ Order.IsSuccLimit o := by