no goals
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b : α
R : α → α → Prop
a : α
⊢ Chain R a []
simp
no goals
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b : α
R : α → α → Prop
a : α
h : 0 < length []
⊢ R a (get [] { val := 0, isLt := h })
simp at h
no goals
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b : α
R : α → α → Prop
a : α
x✝ : ℕ
h : x✝ < length [] - 1
⊢ R (get [] { val := x✝, isLt := (_ : x✝ < length []) }) (get [] { val := x✝ + 1, isLt := (_ : succ x✝ < length []) })
simp at h
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ (R a b ∧
      (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
        ∀ (i : ℕ) (h : i < length t - 1),
          R (get t { val := i, isLt := (_ : i < length t) })
            (get t { val := i + 1, isLt := (_ : succ i < length t) })) ↔
    (∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ Chain R a (b :: t) ↔
    (∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
rw [chain_cons, @chain_iff_get _ _ t]
case mp
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ (R a b ∧
      (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
        ∀ (i : ℕ) (h : i < length t - 1),
          R (get t { val := i, isLt := (_ : i < length t) })
            (get t { val := i + 1, isLt := (_ : succ i < length t) })) →
    (∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })

case mpr
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ ((∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })) →
    R a b ∧
      (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
        ∀ (i : ℕ) (h : i < length t - 1),
          R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ (R a b ∧
      (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
        ∀ (i : ℕ) (h : i < length t - 1),
          R (get t { val := i, isLt := (_ : i < length t) })
            (get t { val := i + 1, isLt := (_ : succ i < length t) })) ↔
    (∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
constructor
case mpr.intro
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ R a b ∧
    (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length t - 1),
        R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
case mpr
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ ((∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })) →
    R a b ∧
      (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
        ∀ (i : ℕ) (h : i < length t - 1),
          R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
rintro ⟨h0, h⟩
case mpr.intro.left
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ R a b

case mpr.intro.right
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
    ∀ (i : ℕ) (h : i < length t - 1),
      R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
case mpr.intro
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ R a b ∧
    (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length t - 1),
        R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
constructor
case mpr.intro.right.left
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ ∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })

case mpr.intro.right.right
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ ∀ (i : ℕ) (h : i < length t - 1),
    R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
case mpr.intro.right
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
    ∀ (i : ℕ) (h : i < length t - 1),
      R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
constructor
case mpr.intro.right.right
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
i : ℕ
w : i < length t - 1
⊢ R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
case mpr.intro.right.right
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ ∀ (i : ℕ) (h : i < length t - 1),
    R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
intro i w
no goals
case mpr.intro.right.right
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
i : ℕ
w : i < length t - 1
⊢ R (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
exact h (i+1) (lt_pred_iff.mp w)
case mp.intro.intro
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
⊢ (∀ (h : 0 < length (b :: t)), R✝ a (get (b :: t) { val := 0, isLt := h })) ∧
    ∀ (i : ℕ) (h : i < length (b :: t) - 1),
      R✝ (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
        (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
case mp
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ (R a b ∧
      (∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })) ∧
        ∀ (i : ℕ) (h : i < length t - 1),
          R (get t { val := i, isLt := (_ : i < length t) })
            (get t { val := i + 1, isLt := (_ : succ i < length t) })) →
    (∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })) ∧
      ∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
rintro ⟨R, ⟨h0, h⟩⟩
case mp.intro.intro.left
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
⊢ ∀ (h : 0 < length (b :: t)), R✝ a (get (b :: t) { val := 0, isLt := h })

case mp.intro.intro.right
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
⊢ ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R✝ (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
case mp.intro.intro
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
⊢ (∀ (h : 0 < length (b :: t)), R✝ a (get (b :: t) { val := 0, isLt := h })) ∧
    ∀ (i : ℕ) (h : i < length (b :: t) - 1),
      R✝ (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
        (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
constructor
case mp.intro.intro.right
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
i : ℕ
w : i < length (b :: t) - 1
⊢ R✝ (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
    (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
case mp.intro.intro.right
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
⊢ ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R✝ (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
intro i w
case mp.intro.intro.right.zero
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
w : zero < length (b :: t) - 1
⊢ R✝ (get (b :: t) { val := zero, isLt := (_ : zero < length (b :: t)) })
    (get (b :: t) { val := zero + 1, isLt := (_ : succ zero < length (b :: t)) })

case mp.intro.intro.right.succ
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
i : ℕ
w : succ i < length (b :: t) - 1
⊢ R✝ (get (b :: t) { val := succ i, isLt := (_ : succ i < length (b :: t)) })
    (get (b :: t) { val := succ i + 1, isLt := (_ : succ (succ i) < length (b :: t)) })
case mp.intro.intro.right
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
i : ℕ
w : i < length (b :: t) - 1
⊢ R✝ (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
    (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
cases' i with i
no goals
case mp.intro.intro.right.succ
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
i : ℕ
w : succ i < length (b :: t) - 1
⊢ R✝ (get (b :: t) { val := succ i, isLt := (_ : succ i < length (b :: t)) })
    (get (b :: t) { val := succ i + 1, isLt := (_ : succ (succ i) < length (b :: t)) })
. exact h i (lt_pred_iff.2 <| by simpa using w)
case mp.intro.intro.left
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
h✝ : 0 < length (b :: t)
⊢ R✝ a (get (b :: t) { val := 0, isLt := h✝ })
case mp.intro.intro.left
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
⊢ ∀ (h : 0 < length (b :: t)), R✝ a (get (b :: t) { val := 0, isLt := h })
intro _
no goals
case mp.intro.intro.left
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
h✝ : 0 < length (b :: t)
⊢ R✝ a (get (b :: t) { val := 0, isLt := h✝ })
exact R
no goals
case mp.intro.intro.right.zero
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
w : zero < length (b :: t) - 1
⊢ R✝ (get (b :: t) { val := zero, isLt := (_ : zero < length (b :: t)) })
    (get (b :: t) { val := zero + 1, isLt := (_ : succ zero < length (b :: t)) })
apply h0
no goals
case mp.intro.intro.right.succ
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
i : ℕ
w : succ i < length (b :: t) - 1
⊢ R✝ (get (b :: t) { val := succ i, isLt := (_ : succ i < length (b :: t)) })
    (get (b :: t) { val := succ i + 1, isLt := (_ : succ (succ i) < length (b :: t)) })
exact h i (lt_pred_iff.2 <| by simpa using w)
no goals
α : Type u
β : Type v
R✝¹ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R✝ : α → α → Prop
a b : α
t : List α
R : R✝ a b
h0 : ∀ (h : 0 < length t), R✝ b (get t { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length t - 1),
    R✝ (get t { val := i, isLt := (_ : i < length t) }) (get t { val := i + 1, isLt := (_ : succ i < length t) })
i : ℕ
w : succ i < length (b :: t) - 1
⊢ succ i < Nat.sub (length t) 0
simpa using w
case mpr.intro.left
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ 0 < length (b :: t)
case mpr.intro.left
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ R a b
apply h0
no goals
case mpr.intro.left
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ 0 < length (b :: t)
simp
no goals
case mpr.intro.right.left
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
h0 : ∀ (h : 0 < length (b :: t)), R a (get (b :: t) { val := 0, isLt := h })
h :
  ∀ (i : ℕ) (h : i < length (b :: t) - 1),
    R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
      (get (b :: t) { val := i + 1, isLt := (_ : succ i < length (b :: t)) })
⊢ ∀ (h : 0 < length t), R b (get t { val := 0, isLt := h })
apply h 0