refactor(data/list/chain): transitive → is_trans on `chain.pairwi…

…se` (#15571)

Apart from being more widely used throughout `mathlib`, `is_trans` can be inferred when used with common relations such as `≤`, `<`, `∣`, and others.

src/data/list/chain.lean

@@ -123,23 +123,23 @@ begin
   exact chain_cons.2 ⟨r.1, IH r'⟩
 end
 
-protected lemma chain.pairwise (tr : transitive R) :
+protected lemma chain.pairwise [is_trans α R] :
   ∀ {a : α} {l : list α}, chain R a l → pairwise R (a :: l)
 | a [] chain.nil := pairwise_singleton _ _
 | a _ (@chain.cons _ _ _ b l h hb) := hb.pairwise.cons begin
     simp only [mem_cons_iff, forall_eq_or_imp, h, true_and],
-    exact λ c hc, tr h (rel_of_pairwise_cons hb.pairwise hc),
+    exact λ c hc, trans h (rel_of_pairwise_cons hb.pairwise hc),
   end
 
-theorem chain_iff_pairwise (tr : transitive R) {a : α} {l : list α} :
+theorem chain_iff_pairwise [is_trans α R] {a : α} {l : list α} :
   chain R a l ↔ pairwise R (a :: l) :=
-⟨chain.pairwise tr, pairwise.chain⟩
+⟨chain.pairwise, pairwise.chain⟩
 
 protected lemma chain.sublist [is_trans α R] (hl : l₂.chain R a) (h : l₁ <+ l₂) : l₁.chain R a :=
-by { rw chain_iff_pairwise (transitive_of_trans R) at ⊢ hl, exact hl.sublist (h.cons_cons a) }
+by { rw chain_iff_pairwise at ⊢ hl, exact hl.sublist (h.cons_cons a) }
 
 protected lemma chain.rel [is_trans α R] (hl : l.chain R a) (hb : b ∈ l) : R a b :=
-by { rw chain_iff_pairwise (transitive_of_trans R) at hl, exact rel_of_pairwise_cons hl hb }
+by { rw chain_iff_pairwise at hl, exact rel_of_pairwise_cons hl hb }
 
 theorem chain_iff_nth_le {R} : ∀ {a : α} {l : list α},
   chain R a l ↔ (∀ h : 0 < length l, R a (nth_le l 0 h)) ∧ (∀ i (h : i < length l - 1),
@@ -214,13 +214,13 @@ theorem pairwise.chain' : ∀ {l : list α}, pairwise R l → chain' R l
 | []       _ := trivial
 | (a :: l) h := pairwise.chain h
 
-theorem chain'_iff_pairwise (tr : transitive R) : ∀ {l : list α},
+theorem chain'_iff_pairwise [is_trans α R] : ∀ {l : list α},
   chain' R l ↔ pairwise R l
 | []       := (iff_true_intro pairwise.nil).symm
-| (a :: l) := chain_iff_pairwise tr
+| (a :: l) := chain_iff_pairwise
 
 protected lemma chain'.sublist [is_trans α R] (hl : l₂.chain' R) (h : l₁ <+ l₂) : l₁.chain' R :=
-by { rw chain'_iff_pairwise (transitive_of_trans R) at ⊢ hl, exact hl.sublist h }
+by { rw chain'_iff_pairwise at ⊢ hl, exact hl.sublist h }
 
 theorem chain'.cons {x y l} (h₁ : R x y) (h₂ : chain' R (y :: l)) :
   chain' R (x :: y :: l) :=

src/data/list/cycle.lean

@@ -821,12 +821,12 @@ begin
     exact hs b (Hl hb) a Ha }
 end
 
-theorem chain_iff_pairwise (hr : transitive r) : chain r s ↔ ∀ (a ∈ s) (b ∈ s), r a b :=
+theorem chain_iff_pairwise [is_trans α r] : chain r s ↔ ∀ (a ∈ s) (b ∈ s), r a b :=
 ⟨begin
   induction s using cycle.induction_on with a l _,
   exact λ _ b hb, hb.elim,
   intros hs b hb c hc,
-  rw [cycle.chain_coe_cons, chain_iff_pairwise hr] at hs,
+  rw [cycle.chain_coe_cons, chain_iff_pairwise] at hs,
   simp only [pairwise_append, pairwise_cons, mem_append, mem_singleton, list.not_mem_nil,
     is_empty.forall_iff, implies_true_iff, pairwise.nil, forall_eq, true_and] at hs,
   simp only [mem_coe_iff, mem_cons_iff] at hb hc,
@@ -835,11 +835,11 @@ theorem chain_iff_pairwise (hr : transitive r) : chain r s ↔ ∀ (a ∈ s) (b
   { exact hs.1 c (or.inr rfl) },
   { exact hs.1 c (or.inl hc) },
   { exact hs.2.2 b hb },
-  { exact hr (hs.2.2 b hb) (hs.1 c (or.inl hc)) }
+  { exact trans (hs.2.2 b hb) (hs.1 c (or.inl hc)) }
 end, cycle.chain_of_pairwise⟩
 
-theorem forall_eq_of_chain (hr : transitive r) (hr' : anti_symmetric r)
+theorem forall_eq_of_chain [is_trans α r] [is_antisymm α r]
   (hs : chain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : a = b :=
-by { rw chain_iff_pairwise hr at hs, exact hr' (hs a ha b hb) (hs b hb a ha) }
+by { rw chain_iff_pairwise at hs, exact antisymm (hs a ha b hb) (hs b hb a ha) }
 
 end cycle

src/data/list/range.lean

@@ -66,7 +66,7 @@ theorem chain_lt_range' (s n : ℕ) : chain (<) s (range' (s+1) n) :=
 
 theorem pairwise_lt_range' : ∀ s n : ℕ, pairwise (<) (range' s n)
 | s 0     := pairwise.nil
-| s (n+1) := (chain_iff_pairwise (by exact λ a b c, lt_trans)).1 (chain_lt_range' s n)
+| s (n+1) := chain_iff_pairwise.1 (chain_lt_range' s n)
 
 theorem nodup_range' (s n : ℕ) : nodup (range' s n) :=
 (pairwise_lt_range' s n).imp (λ a b, ne_of_lt)

src/data/nat/prime.lean

@@ -513,7 +513,7 @@ lemma factors_chain' (n) : list.chain' (≤) (factors n) :=
 @list.chain'.tail _ _ (_::_) (factors_chain_2 _)
 
 lemma factors_sorted (n : ℕ) : list.sorted (≤) (factors n) :=
-(list.chain'_iff_pairwise (@le_trans _ _)).1 (factors_chain' _)
+list.chain'_iff_pairwise.1 (factors_chain' _)
 
 /-- `factors` can be constructed inductively by extracting `min_fac`, for sufficiently large `n`. -/
 lemma factors_add_two (n : ℕ) :
@@ -1030,7 +1030,7 @@ factors_helper_same _ _ _ _ (mul_one _) (factors_helper_nil _)
 
 lemma factors_helper_end (n : ℕ) (l : list ℕ) (H : factors_helper n 2 l) : nat.factors n = l :=
 let ⟨h₁, h₂, h₃⟩ := H nat.prime_two in
-have _, from (list.chain'_iff_pairwise (@le_trans _ _)).1 (@list.chain'.tail _ _ (_::_) h₁),
+have _, from list.chain'_iff_pairwise.1 (@list.chain'.tail _ _ (_::_) h₁),
 (list.eq_of_perm_of_sorted (nat.factors_unique h₃ h₂) this (nat.factors_sorted _)).symm
 
 /-- Given `n` and `a` natural numerals, returns `(l, ⊢ factors_helper n a l)`. -/

src/logic/equiv/list.lean

@@ -251,7 +251,7 @@ lemma raise_chain : ∀ l n, list.chain (≤) n (raise l n)
 /-- `raise l n` is an non-decreasing sequence. -/
 lemma raise_sorted : ∀ l n, list.sorted (≤) (raise l n)
 | []       n := list.sorted_nil
-| (m :: l) n := (list.chain_iff_pairwise (@le_trans _ _)).1 (raise_chain _ _)
+| (m :: l) n := list.chain_iff_pairwise.1 (raise_chain _ _)
 
 /-- If `α` is denumerable, then so is `multiset α`. Warning: this is *not* the same encoding as used
 in `multiset.encodable`. -/
@@ -299,8 +299,7 @@ lemma raise'_chain : ∀ l {m n}, m < n → list.chain (<) m (raise' l n)
 /-- `raise' l n` is a strictly increasing sequence. -/
 lemma raise'_sorted : ∀ l n, list.sorted (<) (raise' l n)
 | []       n := list.sorted_nil
-| (m :: l) n := (list.chain_iff_pairwise (@lt_trans _ _)).1
-  (raise'_chain _ (lt_succ_self _))
+| (m :: l) n := list.chain_iff_pairwise.1 (raise'_chain _ (lt_succ_self _))
 
 /-- Makes `raise' l n` into a finset. Elements are distinct thanks to `raise'_sorted`. -/
 def raise'_finset (l : list ℕ) (n : ℕ) : finset ℕ :=