feat(data/list/chain): induction up the chain (#5325)

Slightly strengthen statements that were there before

src/category_theory/is_connected.lean

@@ -291,7 +291,7 @@ begin
   apply is_connected.of_induct,
   intros p d k j,
   obtain ⟨l, zags, lst⟩ := h j (classical.arbitrary J),
-  apply list.chain.induction p l zags lst _ d,
+  apply list.chain.induction_head p l zags lst _ d,
   rintros _ _ (⟨⟨xy⟩⟩ | ⟨⟨yx⟩⟩),
   { exact (k xy).2 },
   { exact (k yx).1 }

src/data/list/chain.lean

@@ -265,18 +265,32 @@ end
 
 /--
 Given a chain from `a` to `b`, and a predicate true at `b`, if `r x y → p y → p x` then
-the predicate is true at `a`.
+the predicate is true everywhere in the chain and at `a`.
 That is, we can propagate the predicate up the chain.
 -/
 lemma chain.induction {r : α → α → Prop} (p : α → Prop) {a b : α}
   (l : list α) (h : chain r a l)
   (hb : last (a :: l) (cons_ne_nil _ _) = b)
-  (carries : ∀ {x y : α}, r x y → p y → p x) (final : p b) : p a :=
+  (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) : ∀ i ∈ a :: l, p i :=
 begin
   induction l generalizing a,
-  { cases hb, exact final },
+  { cases hb,
+    simp [final] },
   { rw chain_cons at h,
-    apply carries h.1 (l_ih h.2 hb) }
+    rintro _ (rfl | _),
+    apply carries h.1 (l_ih h.2 hb _ (or.inl rfl)),
+    apply l_ih h.2 hb _ H }
 end
 
+/--
+Given a chain from `a` to `b`, and a predicate true at `b`, if `r x y → p y → p x` then
+the predicate is true at `a`.
+That is, we can propagate the predicate all the way up the chain.
+-/
+lemma chain.induction_head {r : α → α → Prop} (p : α → Prop) {a b : α}
+  (l : list α) (h : chain r a l)
+  (hb : last (a :: l) (cons_ne_nil _ _) = b)
+  (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) : p a :=
+(chain.induction p l h hb carries final) _ (mem_cons_self _ _)
+
 end list