case nil
α : Type u_2
β : Type u_1
r : α → α → Prop
f : β → α
s : Cycle β
⊢ Chain r (map f (Quotient.mk'' [])) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' [])

case cons
α : Type u_2
β : Type u_1
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f (Quotient.mk'' (a :: l))) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' (a :: l))
α : Type u_2
β : Type u_1
r : α → α → Prop
f : β → α
s : Cycle β
l : List β
⊢ Chain r (map f (Quotient.mk'' l)) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' l)
cases' l with a l
case cons
α : Type u_2
β : Type u_1
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f (Quotient.mk'' (a :: l))) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' (a :: l))
case nil
α : Type u_2
β : Type u_1
r : α → α → Prop
f : β → α
s : Cycle β
⊢ Chain r (map f (Quotient.mk'' [])) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' [])

case cons
α : Type u_2
β : Type u_1
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f (Quotient.mk'' (a :: l))) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' (a :: l))
rfl
case cons
α : Type u_2
β : Type u_1
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ List.Chain r (f a) (List.map f l ++ [f a]) ↔ List.Chain (fun a b => r (f a) (f b)) a (l ++ [a])
case cons
α : Type u_2
β : Type u_1
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f (Quotient.mk'' (a :: l))) ↔ Chain (fun a b => r (f a) (f b)) (Quotient.mk'' (a :: l))
dsimp only [Chain, ← mk''_eq_coe, Quotient.liftOn'_mk'', Cycle.map, Quotient.map', Quot.map,
  Quotient.mk'', Quotient.liftOn', Quotient.liftOn, Quot.liftOn_mk, List.map]
case cons
α : Type u_2
β : Type u_1
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ List.Chain (fun a b => r (f a) (f b)) a (concat l a) ↔ List.Chain (fun a b => r (f a) (f b)) a (l ++ [a])
case cons
α : Type u_2
β : Type u_1
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ List.Chain r (f a) (List.map f l ++ [f a]) ↔ List.Chain (fun a b => r (f a) (f b)) a (l ++ [a])
rw [← concat_eq_append, ← List.map_concat, List.chain_map f]
no goals
case cons
α : Type u_2
β : Type u_1
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ List.Chain (fun a b => r (f a) (f b)) a (concat l a) ↔ List.Chain (fun a b => r (f a) (f b)) a (l ++ [a])
simp