-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_iff_forall_sublist : l.Pairwise R ↔ (∀ {a b}, [a,b] <+ l → R a b)

Proof state:
case cons.mpr.right
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
⊢ Pairwise R tl

Tactic:
apply IH.mpr

Result:
case cons.mpr.right
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
⊢ ∀ {a b : α✝}, [a, b] <+ tl → R a b

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : (∀ (a' : α✝), a' ∈ tl → R hd a') ∧ Pairwise R tl
x✝² x✝¹ : α✝
x✝ : [x✝², x✝¹] <+ hd :: tl
b : α✝
hab : [b] <+ tl
⊢ R hd b

Tactic:
refine h.1 _ (hab.subset ?_)

Result:
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : (∀ (a' : α✝), a' ∈ tl → R hd a') ∧ Pairwise R tl
x✝² x✝¹ : α✝
x✝ : [x✝², x✝¹] <+ hd :: tl
b : α✝
hab : [b] <+ tl
⊢ b ∈ [b]

Proof state:
case nil
α✝ : Type u_1
R : α✝ → α✝ → Prop
⊢ Pairwise R [] ↔ ∀ {a b : α✝}, [a, b] <+ [] → R a b

Tactic:
simp

Result:
no goals

Proof state:
case cons.mpr.right
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
⊢ ∀ {a b : α✝}, [a, b] <+ tl → R a b

Tactic:
intro a b hab

Result:
case cons.mpr.right
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
a b : α✝
hab : [a, b] <+ tl
⊢ R a b

Proof state:
case cons.mpr.right
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
a b : α✝
hab : [a, b] <+ tl
⊢ R a b

Tactic:
apply h

Result:
case cons.mpr.right.a
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
a b : α✝
hab : [a, b] <+ tl
⊢ [a, b] <+ hd :: tl

Proof state:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
⊢ Pairwise R (hd :: tl) ↔ ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b

Tactic:
rw [List.pairwise_cons]

Result:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
⊢ (∀ (a' : α✝), a' ∈ tl → R hd a') ∧ Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b

Proof state:
case cons.mpr.left
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
x : α✝
hx : x ∈ tl
⊢ R hd x

Tactic:
apply h

Result:
case cons.mpr.left.a
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
x : α✝
hx : x ∈ tl
⊢ [hd, x] <+ hd :: tl

Proof state:
case cons.mpr.left
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
⊢ ∀ (a' : α✝), a' ∈ tl → R hd a'

Tactic:
intro x hx

Result:
case cons.mpr.left
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
x : α✝
hx : x ∈ tl
⊢ R hd x

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : (∀ (a' : α✝), a' ∈ tl → R hd a') ∧ Pairwise R tl
x✝² x✝¹ : α✝
x✝ : [x✝², x✝¹] <+ hd :: tl
b : α✝
hab : [b] <+ tl
⊢ b ∈ [b]

Tactic:
simp

Result:
no goals

Proof state:
case cons.mpr.left.a
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
x : α✝
hx : x ∈ tl
⊢ x ∈ tl

Tactic:
exact hx

Result:
no goals

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : (∀ (a' : α✝), a' ∈ tl → R hd a') ∧ Pairwise R tl
x✝² x✝¹ : α✝
x✝ : [x✝², x✝¹] <+ hd :: tl
a b : α✝
hab : [a, b] <+ tl
⊢ R a b

Tactic:
exact IH.mp h.2 hab

Result:
no goals

Proof state:
case cons.mp
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : (∀ (a' : α✝), a' ∈ tl → R hd a') ∧ Pairwise R tl
⊢ ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b

Tactic:
intro
| a, b, .cons _ hab => exact IH.mp h.2 hab
| _, b, .cons₂ _ hab => refine h.1 _ (hab.subset ?_); simp

Result:
no goals

Proof state:
case cons.mpr.right.a
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
a b : α✝
hab : [a, b] <+ tl
⊢ [a, b] <+ hd :: tl

Tactic:
exact hab.cons _

Result:
no goals

Proof state:
case cons.mpr.left.a
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
x : α✝
hx : x ∈ tl
⊢ [hd, x] <+ hd :: tl

Tactic:
rw [List.cons_sublist_cons, List.singleton_sublist]

Result:
case cons.mpr.left.a
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
x : α✝
hx : x ∈ tl
⊢ x ∈ tl

Proof state:
case cons.mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
⊢ (∀ (a' : α✝), a' ∈ tl → R hd a') ∧ Pairwise R tl

Tactic:
constructor

Result:
case cons.mpr.left
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
⊢ ∀ (a' : α✝), a' ∈ tl → R hd a'

case cons.mpr.right
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
⊢ Pairwise R tl

Proof state:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
⊢ (∀ (a' : α✝), a' ∈ tl → R hd a') ∧ Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b

Tactic:
constructor <;> intro h

Result:
case cons.mp
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : (∀ (a' : α✝), a' ∈ tl → R hd a') ∧ Pairwise R tl
⊢ ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b

case cons.mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
hd : α✝
tl : List α✝
IH : Pairwise R tl ↔ ∀ {a b : α✝}, [a, b] <+ tl → R a b
h : ∀ {a b : α✝}, [a, b] <+ hd :: tl → R a b
⊢ (∀ (a' : α✝), a' ∈ tl → R hd a') ∧ Pairwise R tl