perf (CategoryTheory.ComposableArrows): swap out linarith for omega (#9594)

This file now has the lead in the number of CPU instructions amongst all of mathlib. The majority come from `linarith` being an `autoparam` for many definitions, often in multiple arguments. This uses `omega` in place of `linarith` to improve performance. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: mattrobball

Mathlib/Algebra/Homology/ExactSequence.lean

@@ -44,16 +44,16 @@ variable {n : ℕ} (S : ComposableArrows C n)
 two consecutive arrows are zero. -/
 structure IsComplex : Prop where
   /-- the composition of two consecutive arrows is zero -/
-  zero (i : ℕ) (hi : i + 2 ≤ n := by linarith) :
+  zero (i : ℕ) (hi : i + 2 ≤ n := by omega) :
     S.map' i (i + 1) ≫ S.map' (i + 1) (i + 2) = 0
 
 attribute [reassoc] IsComplex.zero
 
 variable {S}
 
 @[reassoc]
-lemma IsComplex.zero' (hS : S.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by linarith)
-    (hjk : j + 1 = k := by linarith) (hk : k ≤ n := by linarith) :
+lemma IsComplex.zero' (hS : S.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega)
+    (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) :
     S.map' i j ≫ S.map' j k = 0 := by
   subst hij hjk
   exact hS.zero i hk
@@ -75,42 +75,42 @@ lemma isComplex₀ (S : ComposableArrows C 0) : S.IsComplex where
   zero i hi := by simp (config := {decide := true}) at hi
 
 lemma isComplex₁ (S : ComposableArrows C 1) : S.IsComplex where
-  zero i hi := by exfalso; linarith
+  zero i hi := by exfalso; omega
 
 variable (S)
 
 /-- The short complex consisting of maps `S.map' i j` and `S.map' j k` when we know
 that `S : ComposableArrows C n` satisfies `S.IsComplex`. -/
 @[reducible]
-def sc' (hS : S.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by linarith)
-    (hjk : j + 1 = k := by linarith) (hk : k ≤ n := by linarith) :
+def sc' (hS : S.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega)
+    (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) :
     ShortComplex C :=
   ShortComplex.mk (S.map' i j) (S.map' j k) (hS.zero' i j k)
 
 /-- The short complex consisting of maps `S.map' i (i + 1)` and `S.map' (i + 1) (i + 2)`
 when we know that `S : ComposableArrows C n` satisfies `S.IsComplex`. -/
-abbrev sc (hS : S.IsComplex) (i : ℕ) (hi : i + 2 ≤ n := by linarith) :
+abbrev sc (hS : S.IsComplex) (i : ℕ) (hi : i + 2 ≤ n := by omega) :
     ShortComplex C :=
   S.sc' hS i (i + 1) (i + 2)
 
 /-- `F : ComposableArrows C n` is exact if it is a complex and that all short
 complexes consisting of two consecutive arrows are exact. -/
 structure Exact extends S.IsComplex : Prop where
-  exact (i : ℕ) (hi : i + 2 ≤ n := by linarith) : (S.sc toIsComplex i).Exact
+  exact (i : ℕ) (hi : i + 2 ≤ n := by omega) : (S.sc toIsComplex i).Exact
 
 variable {S}
 
-lemma Exact.exact' (hS : S.Exact) (i j k : ℕ) (hij : i + 1 = j := by linarith)
-    (hjk : j + 1 = k := by linarith) (hk : k ≤ n := by linarith) :
+lemma Exact.exact' (hS : S.Exact) (i j k : ℕ) (hij : i + 1 = j := by omega)
+    (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) :
     (S.sc' hS.toIsComplex i j k).Exact := by
   subst hij hjk
   exact hS.exact i hk
 
 /-- Functoriality maps for `ComposableArrows.sc'`. -/
 @[simps]
 def sc'Map {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex)
-    (i j k : ℕ) (hij : i + 1 = j := by linarith)
-    (hjk : j + 1 = k := by linarith) (hk : k ≤ n := by linarith) :
+    (i j k : ℕ) (hij : i + 1 = j := by omega)
+    (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) :
     S₁.sc' h₁ i j k ⟶ S₂.sc' h₂ i j k where
   τ₁ := φ.app _
   τ₂ := φ.app _
@@ -119,16 +119,16 @@ def sc'Map {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.
 /-- Functoriality maps for `ComposableArrows.sc`. -/
 @[simps!]
 def scMap {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex)
-    (i : ℕ) (hi : i + 2 ≤ n := by linarith) :
+    (i : ℕ) (hi : i + 2 ≤ n := by omega) :
     S₁.sc h₁ i ⟶ S₂.sc h₂ i :=
   sc'Map φ h₁ h₂ i (i + 1) (i + 2)
 
 /-- The isomorphism `S₁.sc' _ i j k ≅ S₂.sc' _ i j k` induced by an isomorphism `S₁ ≅ S₂`
 in `ComposableArrows C n`. -/
 @[simps]
 def sc'MapIso {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂)
-    (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by linarith)
-    (hjk : j + 1 = k := by linarith) (hk : k ≤ n := by linarith) :
+    (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega)
+    (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) :
     S₁.sc' h₁ i j k ≅ S₂.sc' h₂ i j k where
   hom := sc'Map e.hom h₁ h₂ i j k
   inv := sc'Map e.inv h₂ h₁ i j k
@@ -140,7 +140,7 @@ in `ComposableArrows C n`. -/
 @[simps]
 def scMapIso {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂)
     (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex)
-    (i : ℕ) (hi : i + 2 ≤ n := by linarith) :
+    (i : ℕ) (hi : i + 2 ≤ n := by omega) :
     S₁.sc h₁ i ≅ S₂.sc h₂ i where
   hom := scMap e.hom h₁ h₂ i
   inv := scMap e.inv h₂ h₁ i
@@ -164,16 +164,16 @@ lemma exact₀ (S : ComposableArrows C 0) : S.Exact where
 
 lemma exact₁ (S : ComposableArrows C 1) : S.Exact where
   toIsComplex := S.isComplex₁
-  exact i hi := by exfalso; linarith
+  exact i hi := by exfalso; omega
 
 lemma isComplex₂_iff (S : ComposableArrows C 2) :
     S.IsComplex ↔ S.map' 0 1 ≫ S.map' 1 2 = 0 := by
   constructor
   · intro h
-    exact h.zero 0 (by linarith)
+    exact h.zero 0 (by omega)
   · intro h
     refine' IsComplex.mk (fun i hi => _)
-    obtain rfl : i = 0 := by linarith
+    obtain rfl : i = 0 := by omega
     exact h
 
 lemma isComplex₂_mk (S : ComposableArrows C 2) (w : S.map' 0 1 ≫ S.map' 1 2 = 0) :
@@ -188,10 +188,10 @@ lemma exact₂_iff (S : ComposableArrows C 2) (hS : S.IsComplex) :
     S.Exact ↔ (S.sc' hS 0 1 2).Exact := by
   constructor
   · intro h
-    exact h.exact 0 (by linarith)
+    exact h.exact 0 (by omega)
   · intro h
     refine' Exact.mk hS (fun i hi => _)
-    obtain rfl : i = 0 := by linarith
+    obtain rfl : i = 0 := by omega
     exact h
 
 lemma exact₂_mk (S : ComposableArrows C 2) (w : S.map' 0 1 ≫ S.map' 1 2 = 0)
@@ -216,7 +216,7 @@ lemma exact_iff_δ₀ (S : ComposableArrows C (n + 2)) :
     · rw [exact₂_iff]; swap
       · rw [isComplex₂_iff]
         exact h.toIsComplex.zero 0
-      exact h.exact 0 (by linarith)
+      exact h.exact 0 (by omega)
     · exact Exact.mk (IsComplex.mk (fun i hi => h.toIsComplex.zero (i + 1)))
         (fun i hi => h.exact (i + 1))
   · rintro ⟨h, h₀⟩
@@ -247,13 +247,13 @@ lemma exact_iff_δlast {n : ℕ} (S : ComposableArrows C (n + 2)) :
     · rw [exact₂_iff]; swap
       · rw [isComplex₂_iff]
         exact h.toIsComplex.zero n
-      exact h.exact n (by linarith)
+      exact h.exact n (by omega)
   · rintro ⟨h, h'⟩
     refine' Exact.mk (IsComplex.mk (fun i hi => _)) (fun i hi => _)
-    · obtain hi | rfl := LE.le.lt_or_eq (show i ≤ n by linarith)
+    · obtain hi | rfl := LE.le.lt_or_eq (show i ≤ n by omega)
       · exact h.toIsComplex.zero i
       · exact h'.toIsComplex.zero 0
-    · obtain hi | rfl := LE.le.lt_or_eq (show i ≤ n by linarith)
+    · obtain hi | rfl := LE.le.lt_or_eq (show i ≤ n by omega)
       · exact h.exact i
       · exact h'.exact 0
 

Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean

@@ -106,7 +106,7 @@ theorem epi_of_epi_of_epi_of_mono'
       ← R₂.map'_comp 1 2 3, hR₂', comp_zero, comp_zero]
   obtain ⟨A₂, π₂, _, f₁, h₃⟩ := (hR₁.exact 0).exact_up_to_refinements _ h₂
   dsimp at f₁ h₃
-  have h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1) ≫ R₂.map' 1 2 = 0 := by
+  have h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 _) ≫ R₂.map' 1 2 = 0 := by
     rw [sub_comp, assoc, assoc, assoc, ← NatTrans.naturality, ← reassoc_of% h₃, h₁, sub_self]
   obtain ⟨A₃, π₃, _, g₀, h₅⟩ := (hR₂.exact 0).exact_up_to_refinements _ h₄
   dsimp at g₀ h₅