chore: remove superfluous uses of triv (#11679)

Std defines `triv`, a slight variation on `trivial`. It appears that Mathlib doesn't care about the distinction (any more?) and so we can consolidate on a single tactic. leanprover-community/batteries#712 separately replaces `triv` in Std with an error explaining to use `trivial`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Apr 15, 2024 · ef90877 · ef90877
1 parent 193d1f4
commit ef90877
Show file tree

Hide file tree

Showing 6 changed files with 7 additions and 19 deletions.
diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
@@ -818,11 +818,11 @@ def Scheme.openCoverOfSuprEqTop {s : Type*} (X : Scheme) (U : s → Opens X)
   obj i := X.restrict (U i).openEmbedding
   map i := X.ofRestrict (U i).openEmbedding
   f x :=
-    haveI : x ∈ ⨆ i, U i := hU.symm ▸ show x ∈ (⊤ : Opens X) by triv
+    haveI : x ∈ ⨆ i, U i := hU.symm ▸ show x ∈ (⊤ : Opens X) by trivial
     (Opens.mem_iSup.mp this).choose
   Covers x := by
     erw [Subtype.range_coe]
-    have : x ∈ ⨆ i, U i := hU.symm ▸ show x ∈ (⊤ : Opens X) by triv
+    have : x ∈ ⨆ i, U i := hU.symm ▸ show x ∈ (⊤ : Opens X) by trivial
     exact (Opens.mem_iSup.mp this).choose_spec
 #align algebraic_geometry.Scheme.open_cover_of_supr_eq_top AlgebraicGeometry.Scheme.openCoverOfSuprEqTop
 

diff --git a/Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean b/Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean
@@ -138,7 +138,7 @@ theorem LinearMap.continuousAt_zero_of_locally_bounded (f : E →ₛₗ[σ] F)
     intro n
     by_cases h : n = 0
     · rw [h, Nat.cast_zero, zero_smul]
-      exact mem_of_mem_nhds (bE.1.mem_of_mem <| by triv)
+      exact mem_of_mem_nhds (bE.1.mem_of_mem <| by trivial)
     rcases hu n h with ⟨y, hy, hu1⟩
     convert hy
     rw [← hu1, ← mul_smul]

diff --git a/Mathlib/Data/List/Cycle.lean b/Mathlib/Data/List/Cycle.lean
@@ -972,7 +972,7 @@ variable {r : α → α → Prop} {s : Cycle α}
 theorem Chain.imp {r₁ r₂ : α → α → Prop} (H : ∀ a b, r₁ a b → r₂ a b) (p : Chain r₁ s) :
     Chain r₂ s := by
   induction s using Cycle.induction_on
-  · triv
+  · trivial
   · rw [chain_coe_cons] at p ⊢
     exact p.imp H
 #align cycle.chain.imp Cycle.Chain.imp

diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean
@@ -1513,7 +1513,7 @@ theorem injective_iff_injective_of_iUnion_eq_univ :
     Injective f ↔ ∀ i, Injective ((U i).restrictPreimage f) := by
   refine' ⟨fun H i => (U i).restrictPreimage_injective H, fun H x y e => _⟩
   obtain ⟨i, hi⟩ := Set.mem_iUnion.mp
-      (show f x ∈ Set.iUnion U by rw [hU]; triv)
+      (show f x ∈ Set.iUnion U by rw [hU]; trivial)
   injection @H i ⟨x, hi⟩ ⟨y, show f y ∈ U i from e ▸ hi⟩ (Subtype.ext e)
 #align set.injective_iff_injective_of_Union_eq_univ Set.injective_iff_injective_of_iUnion_eq_univ
 
@@ -1522,7 +1522,7 @@ theorem surjective_iff_surjective_of_iUnion_eq_univ :
   refine' ⟨fun H i => (U i).restrictPreimage_surjective H, fun H x => _⟩
   obtain ⟨i, hi⟩ :=
     Set.mem_iUnion.mp
-      (show x ∈ Set.iUnion U by rw [hU]; triv)
+      (show x ∈ Set.iUnion U by rw [hU]; trivial)
   exact ⟨_, congr_arg Subtype.val (H i ⟨x, hi⟩).choose_spec⟩
 #align set.surjective_iff_surjective_of_Union_eq_univ Set.surjective_iff_surjective_of_iUnion_eq_univ
 

diff --git a/Mathlib/Topology/LocalAtTarget.lean b/Mathlib/Topology/LocalAtTarget.lean
@@ -126,7 +126,7 @@ theorem inducing_iff_inducing_of_iSup_eq_top (h : Continuous f) :
       Opens.mem_iSup.mp
         (show f x ∈ iSup U by
           rw [hU]
-          triv)
+          trivial)
     erw [← OpenEmbedding.map_nhds_eq (h.1 _ (U i).2).openEmbedding_subtype_val ⟨x, hi⟩]
     rw [(H i) ⟨x, hi⟩, Filter.subtype_coe_map_comap, Function.comp_apply, Subtype.coe_mk,
       inf_eq_left, Filter.le_principal_iff]

diff --git a/test/triv.lean b/test/triv.lean