α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
p : Pairwise R (a :: l)
r : ∀ (a' : α✝), a' ∈ l → R a a'
p' : Pairwise R l
⊢ Chain R a l
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
p : Pairwise R (a :: l)
⊢ Chain R a l
let ⟨r, p'⟩ := pairwise_cons.1 p
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
r : ∀ (a' : α✝), a' ∈ l → R a a'
p' : Pairwise R l
⊢ Chain R a l
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
p : Pairwise R (a :: l)
r : ∀ (a' : α✝), a' ∈ l → R a a'
p' : Pairwise R l
⊢ Chain R a l
clear p
no goals
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
r : ∀ (a' : α✝), a' ∈ l → R a a'
p' : Pairwise R l
⊢ Chain R a l
induction p' generalizing a with
| nil => exact Chain.nil
| @cons b l r' _ IH =>
  simp only [chain_cons, forall_mem_cons] at r
  exact chain_cons.2 ⟨r.1, IH r'⟩
no goals
case nil
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
a : α✝
r : ∀ (a' : α✝), a' ∈ [] → R a a'
⊢ Chain R a []
exact Chain.nil
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
l✝ : List α✝
b : α✝
l : List α✝
r' : ∀ (a' : α✝), a' ∈ l → R b a'
a✝ : Pairwise R l
IH : ∀ {a : α✝}, (∀ (a' : α✝), a' ∈ l → R a a') → Chain R a l
a : α✝
r : R a b ∧ ∀ (x : α✝), x ∈ l → R a x
⊢ Chain R a (b :: l)
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
l✝ : List α✝
b : α✝
l : List α✝
r' : ∀ (a' : α✝), a' ∈ l → R b a'
a✝ : Pairwise R l
IH : ∀ {a : α✝}, (∀ (a' : α✝), a' ∈ l → R a a') → Chain R a l
a : α✝
r : ∀ (a' : α✝), a' ∈ b :: l → R a a'
⊢ Chain R a (b :: l)
simp only [chain_cons, forall_mem_cons] at r
no goals
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
l✝ : List α✝
b : α✝
l : List α✝
r' : ∀ (a' : α✝), a' ∈ l → R b a'
a✝ : Pairwise R l
IH : ∀ {a : α✝}, (∀ (a' : α✝), a' ∈ l → R a a') → Chain R a l
a : α✝
r : R a b ∧ ∀ (x : α✝), x ∈ l → R a x
⊢ Chain R a (b :: l)
exact chain_cons.2 ⟨r.1, IH r'⟩