case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ (a : α), a ∈ nil → ∀ (b : α), b ∈ nil → r a b) → Chain r nil

case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
⊢ (∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b) → Chain r ↑(a :: l)
α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → r a b) → Chain r s
induction' s using Cycle.induction_on with a l _
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
⊢ (∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b) → Chain r ↑(a :: l)
case H0
α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ (a : α), a ∈ nil → ∀ (b : α), b ∈ nil → r a b) → Chain r nil

case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
⊢ (∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b) → Chain r ↑(a :: l)
exact fun _ => Cycle.Chain.nil r
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
⊢ Chain r ↑(a :: l)
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
⊢ (∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b) → Chain r ↑(a :: l)
intro hs
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
⊢ Chain r ↑(a :: l)
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
⊢ Chain r ↑(a :: l)
have Ha : a ∈ (a :: l : Cycle α) := by simp
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ Chain r ↑(a :: l)
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
⊢ Chain r ↑(a :: l)
have Hl : ∀ {b} (_hb : b ∈ l), b ∈ (a :: l : Cycle α) := @fun b hb => by simp [hb]
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ List.Chain r a (l ++ [a])
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ Chain r ↑(a :: l)
rw [Cycle.chain_coe_cons]
case HI.p
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ List.Pairwise r (a :: (l ++ [a]))
case HI
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ List.Chain r a (l ++ [a])
apply Pairwise.chain
case HI.p
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ (∀ (a' : α), a' ∈ l ++ [a] → r a a') ∧ List.Pairwise r (l ++ [a])
case HI.p
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ List.Pairwise r (a :: (l ++ [a]))
rw [pairwise_cons]
case HI.p.refine'_1
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l ++ [a]
⊢ r a b

case HI.p.refine'_2
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c ∈ [a]
⊢ r b c
case HI.p
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ (∀ (a' : α), a' ∈ l ++ [a] → r a a') ∧ List.Pairwise r (l ++ [a])
refine'
  ⟨fun b hb => _,
    pairwise_append.2
      ⟨pairwise_of_forall_mem_list fun b hb c hc => hs b (Hl hb) c (Hl hc),
        pairwise_singleton r a, fun b hb c hc => _⟩⟩
no goals
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
⊢ a ∈ ↑(a :: l)
simp
no goals
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
b : α
hb : b ∈ l
⊢ b ∈ ↑(a :: l)
simp [hb]
case HI.p.refine'_1
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l ∨ b ∈ [a]
⊢ r a b
case HI.p.refine'_1
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l ++ [a]
⊢ r a b
rw [mem_append] at hb
case HI.p.refine'_1.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
⊢ r a b

case HI.p.refine'_1.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ [a]
⊢ r a b
case HI.p.refine'_1
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l ∨ b ∈ [a]
⊢ r a b
cases' hb with hb hb
no goals
case HI.p.refine'_1.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
⊢ r a b
exact hs a Ha b (Hl hb)
case HI.p.refine'_1.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b = a
⊢ r a b
case HI.p.refine'_1.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ [a]
⊢ r a b
rw [mem_singleton] at hb
case HI.p.refine'_1.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b = a
⊢ r a a
case HI.p.refine'_1.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b = a
⊢ r a b
rw [hb]
no goals
case HI.p.refine'_1.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b = a
⊢ r a a
exact hs a Ha a Ha
case HI.p.refine'_2
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c = a
⊢ r b c
case HI.p.refine'_2
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c ∈ [a]
⊢ r b c
rw [mem_singleton] at hc
case HI.p.refine'_2
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c = a
⊢ r b a
case HI.p.refine'_2
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c = a
⊢ r b c
rw [hc]
no goals
case HI.p.refine'_2
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ (a : α), a ∈ ↑l → ∀ (b : α), b ∈ ↑l → r a b) → Chain r ↑l
hs : ∀ (a_1 : α), a_1 ∈ ↑(a :: l) → ∀ (b : α), b ∈ ↑(a :: l) → r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c = a
⊢ r b a
exact hs b (Hl hb) a Ha