-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Pairwise.lean
theorem pairwise_iff_getElem : Pairwise R l ↔
    ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j]

Proof state:
case mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
a b : α✝
h'✝ : [a, b] <+ l
is : List (Fin l.length)
h' : [a, b] = map (fun x => l[x]) is
hij : Pairwise (fun x1 x2 => x1 < x2) is
⊢ R a b

Tactic:
rcases is with ⟨⟩ | ⟨a', ⟨⟩ | ⟨b', ⟨⟩⟩⟩ <;> simp at h'

Result:
case mpr.cons.cons.nil
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
a b : α✝
h'✝ : [a, b] <+ l
a' b' : Fin l.length
hij : Pairwise (fun x1 x2 => x1 < x2) [a', b']
h' : a = l[↑a'] ∧ b = l[↑b']
⊢ R a b

Proof state:
case mp
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ {a b : α✝}, [a, b] <+ l → R a b
i j : Nat
hi : i < l.length
hj : j < l.length
h' : i < j
⊢ R l[i] l[j]

Tactic:
apply h

Result:
case mp.a
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ {a b : α✝}, [a, b] <+ l → R a b
i j : Nat
hi : i < l.length
hj : j < l.length
h' : i < j
⊢ [l[i], l[j]] <+ l

Proof state:
case mp.a
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ {a b : α✝}, [a, b] <+ l → R a b
i j : Nat
hi : i < l.length
hj : j < l.length
h' : i < j
⊢ [l[i], l[j]] <+ l

Tactic:
simpa [h'] using map_getElem_sublist (is := [⟨i, hi⟩, ⟨j, hj⟩])

Result:
no goals

Proof state:
case mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
a b : α✝
h' : [a, b] <+ l
⊢ R a b

Tactic:
have ⟨is, h', hij⟩ := sublist_eq_map_getElem h'

Result:
case mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
a b : α✝
h'✝ : [a, b] <+ l
is : List (Fin l.length)
h' : [a, b] = map (fun x => l[x]) is
hij : Pairwise (fun x1 x2 => x1 < x2) is
⊢ R a b

Proof state:
case mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
⊢ ∀ {a b : α✝}, [a, b] <+ l → R a b

Tactic:
intros a b h'

Result:
case mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
a b : α✝
h' : [a, b] <+ l
⊢ R a b

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
⊢ (∀ {a b : α✝}, [a, b] <+ l → R a b) ↔ ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]

Tactic:
constructor <;> intro h

Result:
case mp
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ {a b : α✝}, [a, b] <+ l → R a b
⊢ ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]

case mpr
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
⊢ ∀ {a b : α✝}, [a, b] <+ l → R a b

Proof state:
case mp
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ {a b : α✝}, [a, b] <+ l → R a b
⊢ ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]

Tactic:
intros i j hi hj h'

Result:
case mp
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ {a b : α✝}, [a, b] <+ l → R a b
i j : Nat
hi : i < l.length
hj : j < l.length
h' : i < j
⊢ R l[i] l[j]

Proof state:
case mpr.cons.cons.nil.intro
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
a' b' : Fin l.length
hij : Pairwise (fun x1 x2 => x1 < x2) [a', b']
h' : [l[↑a'], l[↑b']] <+ l
⊢ R l[↑a'] l[↑b']

Tactic:
apply h

Result:
case mpr.cons.cons.nil.intro._hij
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
a' b' : Fin l.length
hij : Pairwise (fun x1 x2 => x1 < x2) [a', b']
h' : [l[↑a'], l[↑b']] <+ l
⊢ ↑a' < ↑b'

Proof state:
case mpr.cons.cons.nil.intro._hij
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
a' b' : Fin l.length
hij : Pairwise (fun x1 x2 => x1 < x2) [a', b']
h' : [l[↑a'], l[↑b']] <+ l
⊢ ↑a' < ↑b'

Tactic:
simpa using hij

Result:
no goals

Proof state:
case mpr.cons.cons.nil
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
a b : α✝
h'✝ : [a, b] <+ l
a' b' : Fin l.length
hij : Pairwise (fun x1 x2 => x1 < x2) [a', b']
h' : a = l[↑a'] ∧ b = l[↑b']
⊢ R a b

Tactic:
rcases h' with ⟨rfl, rfl⟩

Result:
case mpr.cons.cons.nil.intro
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
h : ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
a' b' : Fin l.length
hij : Pairwise (fun x1 x2 => x1 < x2) [a', b']
h' : [l[↑a'], l[↑b']] <+ l
⊢ R l[↑a'] l[↑b']

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
⊢ Pairwise R l ↔ ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]

Tactic:
rw [pairwise_iff_forall_sublist]

Result:
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
⊢ (∀ {a b : α✝}, [a, b] <+ l → R a b) ↔ ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]