-- Mathlib/Data/List/Cycle.lean
theorem chain_iff_pairwise [IsTrans α r] : Chain r s ↔ ∀ a ∈ s, ∀ b ∈ s, r a b :=
  ⟨by
    induction' s with a l _
    · exact fun _ b hb => (not_mem_nil _ hb).elim
    intro hs b hb c hc
    rw [Cycle.chain_coe_cons, List.chain_iff_pairwise] at hs
    simp only [pairwise_append, pairwise_cons, mem_append, mem_singleton, List.not_mem_nil,
      IsEmpty.forall_iff, imp_true_iff, Pairwise.nil, forall_eq, true_and] at hs
    simp only [mem_coe_iff, mem_cons] at hb hc
    rcases hb with (rfl | hb) <;> rcases hc with (rfl | hc)
    · exact hs.1 c (Or.inr rfl)
    · exact hs.1 c (Or.inl hc)
    · exact hs.2.2 b hb
    · exact _root_.trans (hs.2.2 b hb) (hs.1 c (Or.inl hc)), Cycle.chain_of_pairwise⟩

Proof state:
case HI.inl.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r c c

Tactic:
exact hs.1 c (Or.inr rfl)

Result:
no goals

Proof state:
case HI.inr.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c

Tactic:
exact _root_.trans (hs.2.2 b hb) (hs.1 c (Or.inl hc))

Result:
no goals

Proof state:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : List.Pairwise r (a :: (l ++ [a]))
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c

Tactic:
simp only [pairwise_append, pairwise_cons, mem_append, mem_singleton, List.not_mem_nil,
  IsEmpty.forall_iff, imp_true_iff, Pairwise.nil, forall_eq, true_and] at hs

Result:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
⊢ r b c

Proof state:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
⊢ Chain r ↑(a :: l) → ∀ a_2 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_2 b

Tactic:
intro hs b hb c hc

Result:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c

Proof state:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b = a ∨ b ∈ l
hc : c = a ∨ c ∈ l
⊢ r b c

Tactic:
rcases hb with (rfl | hb) <;> rcases hc with (rfl | hc)

Result:
case HI.inl.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r c c

case HI.inl.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b
hc : c ∈ l
⊢ r b c

case HI.inr.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hb : b ∈ l
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r b c

case HI.inr.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c

Proof state:
case HI.inl.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b
hc : c ∈ l
⊢ r b c

Tactic:
exact hs.1 c (Or.inl hc)

Result:
no goals

Proof state:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c

Tactic:
rw [Cycle.chain_coe_cons, List.chain_iff_pairwise] at hs

Result:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : List.Pairwise r (a :: (l ++ [a]))
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c

Proof state:
case HI.inr.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hb : b ∈ l
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r b c

Tactic:
exact hs.2.2 b hb

Result:
no goals

Proof state:
case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
⊢ Chain r nil → ∀ a ∈ nil, ∀ b ∈ nil, r a b

Tactic:
exact fun _ b hb => (not_mem_nil _ hb).elim

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
⊢ Chain r s → ∀ a ∈ s, ∀ b ∈ s, r a b

Tactic:
induction' s with a l _

Result:
case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
⊢ Chain r nil → ∀ a ∈ nil, ∀ b ∈ nil, r a b

case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
⊢ Chain r ↑(a :: l) → ∀ a_2 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_2 b

Proof state:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
⊢ r b c

Tactic:
simp only [mem_coe_iff, mem_cons] at hb hc

Result:
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b = a ∨ b ∈ l
hc : c = a ∨ c ∈ l
⊢ r b c