-- Mathlib/Data/List/Chain.lean
theorem chain_iff_get {R} : ∀ {a : α} {l : List α}, Chain R a l ↔
    (∀ h : 0 < length l, R a (get l ⟨0, h⟩)) ∧
      ∀ (i : ℕ) (h : i < l.length - 1),
        R (get l ⟨i, by omega⟩) (get l ⟨i+1, by omega⟩)
  | a, [] => iff_of_true (by simp) ⟨fun h => by simp at h, fun _ h => by simp at h⟩
  | a, b :: t => by
    rw [chain_cons, @chain_iff_get _ _ t]
    constructor
    · rintro ⟨R, ⟨h0, h⟩⟩
      constructor
      · intro _
        exact R
      intro i w
      rcases i with - | i
      · apply h0
      · exact h i (by simp only [length_cons] at w; omega)
    rintro ⟨h0, h⟩; constructor
    · apply h0
      simp
    constructor
    · apply h 0
    intro i w
    exact h (i+1) (by simp only [length_cons]; omega)

Proof state:
case mpr.intro.right.right
α : Type u
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)
⊢ ∀ (i : ℕ) (h : i < t.length - 1), R (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)

Tactic:
intro i w

Result:
case mpr.intro.right.right
α : Type u
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)
i : ℕ
w : i < t.length - 1
⊢ R (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)

Proof state:
case mpr.intro.left
α : Type u
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)
⊢ R a b

Tactic:
apply h0

Result:
case mpr.intro.left
α : Type u
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)
⊢ 0 < (b :: t).length

Proof state:
case mp.intro.intro
α : Type u
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < t.length), R✝ b (t.get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < t.length - 1), R✝ (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)
⊢ (∀ (h : 0 < (b :: t).length), R✝ a ((b :: t).get ⟨0, h⟩)) ∧
    ∀ (i : ℕ) (h : i < (b :: t).length - 1), R✝ ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)

Tactic:
constructor

Result:
case mp.intro.intro.left
α : Type u
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < t.length), R✝ b (t.get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < t.length - 1), R✝ (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)
⊢ ∀ (h : 0 < (b :: t).length), R✝ a ((b :: t).get ⟨0, h⟩)

case mp.intro.intro.right
α : Type u
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < t.length), R✝ b (t.get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < t.length - 1), R✝ (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)
⊢ ∀ (i : ℕ) (h : i < (b :: t).length - 1), R✝ ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)

Proof state:
case mpr
α : Type u
R : α → α → Prop
a b : α
t : List α
⊢ ((∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)) ∧
      ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)) →
    R a b ∧
      (∀ (h : 0 < t.length), R b (t.get ⟨0, h⟩)) ∧ ∀ (i : ℕ) (h : i < t.length - 1), R (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)

Tactic:
rintro ⟨h0, h⟩

Result:
case mpr.intro
α : Type u
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)
⊢ R a b ∧
    (∀ (h : 0 < t.length), R b (t.get ⟨0, h⟩)) ∧ ∀ (i : ℕ) (h : i < t.length - 1), R (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)

Proof state:
α : Type u
β : Type v
R✝ r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b : α
R : α → α → Prop
a : α
l : List α
i : ℕ
h : i < l.length - 1
⊢ i < l.length

Tactic:
omega

Result:
no goals

Proof state:
case mp.intro.intro.left
α : Type u
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < t.length), R✝ b (t.get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < t.length - 1), R✝ (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)
⊢ ∀ (h : 0 < (b :: t).length), R✝ a ((b :: t).get ⟨0, h⟩)

Tactic:
intro _

Result:
case mp.intro.intro.left
α : Type u
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < t.length), R✝ b (t.get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < t.length - 1), R✝ (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)
h✝ : 0 < (b :: t).length
⊢ R✝ a ((b :: t).get ⟨0, h✝⟩)

Proof state:
case mp.intro.intro.right
α : Type u
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < t.length), R✝ b (t.get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < t.length - 1), R✝ (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)
⊢ ∀ (i : ℕ) (h : i < (b :: t).length - 1), R✝ ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)

Tactic:
intro i w

Result:
case mp.intro.intro.right
α : Type u
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < t.length), R✝ b (t.get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < t.length - 1), R✝ (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)
i : ℕ
w : i < (b :: t).length - 1
⊢ R✝ ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)

Proof state:
case mpr.intro
α : Type u
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)
⊢ R a b ∧
    (∀ (h : 0 < t.length), R b (t.get ⟨0, h⟩)) ∧ ∀ (i : ℕ) (h : i < t.length - 1), R (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)

Tactic:
constructor

Result:
case mpr.intro.left
α : Type u
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)
⊢ R a b

case mpr.intro.right
α : Type u
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)
⊢ (∀ (h : 0 < t.length), R b (t.get ⟨0, h⟩)) ∧ ∀ (i : ℕ) (h : i < t.length - 1), R (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)

Proof state:
α : Type u
R : α → α → Prop
a : α
x✝ : ℕ
h : x✝ < [].length - 1
⊢ R ([].get ⟨x✝, ⋯⟩) ([].get ⟨x✝ + 1, ⋯⟩)

Tactic:
simp at h

Result:
no goals

Proof state:
case mp.intro.intro.right.zero
α : Type u
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < t.length), R✝ b (t.get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < t.length - 1), R✝ (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)
w : 0 < (b :: t).length - 1
⊢ R✝ ((b :: t).get ⟨0, ⋯⟩) ((b :: t).get ⟨0 + 1, ⋯⟩)

Tactic:
apply h0

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)
i : ℕ
w : i < t.length - 1
⊢ i + 1 < (b :: t).length - 1

Tactic:
simp only [length_cons]

Result:
α : Type u
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)
i : ℕ
w : i < t.length - 1
⊢ i + 1 < t.length + 1 - 1

Proof state:
case mpr.intro.right.right
α : Type u
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < (b :: t).length), R a ((b :: t).get ⟨0, h⟩)
h : ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)
i : ℕ
w : i < t.length - 1
⊢ R (t.get ⟨i, ⋯⟩) (t.get ⟨i + 1, ⋯⟩)

Tactic:
exact h (i+1) (by simp only [length_cons]; omega)

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a : α
h : 0 < [].length
⊢ R a ([].get ⟨0, h⟩)

Tactic:
simp at h

Result:
no goals