no goals
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a b : α
R : α → α → Prop
⊢ Chain' R []
simp
no goals
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a b : α
R : α → α → Prop
x✝ : ℕ
h : x✝ < length [] - 1
⊢ R (get [] { val := x✝, isLt := (_ : x✝ < length []) }) (get [] { val := x✝ + 1, isLt := (_ : succ x✝ < length []) })
simp at h
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 : α
x✝ : ℕ
h : x✝ < length [a] - 1
⊢ R (get [a] { val := x✝, isLt := (_ : x✝ < length [a]) })
    (get [a] { val := x✝ + 1, isLt := (_ : succ x✝ < length [a]) })
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 ∧
      ∀ (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 (a :: b :: t) - 1),
        R (get (a :: b :: t) { val := 0, isLt := (_ : 0 < length (a :: b :: t)) })
          (get (a :: b :: t) { val := 0 + 1, isLt := (_ : succ 0 < length (a :: b :: t)) })) ∧
      ∀ (n : ℕ) (h : n + 1 < length (a :: b :: t) - 1),
        R (get (a :: b :: t) { val := n + 1, isLt := (_ : n + 1 < length (a :: b :: t)) })
          (get (a :: b :: t) { val := n + 1 + 1, isLt := (_ : succ (n + 1) < length (a :: 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) ↔
    ∀ (i : ℕ) (h : i < length (a :: b :: t) - 1),
      R (get (a :: b :: t) { val := i, isLt := (_ : i < length (a :: b :: t)) })
        (get (a :: b :: t) { val := i + 1, isLt := (_ : succ i < length (a :: b :: t)) })
rw [← and_forall_succ, chain'_cons, chain'_iff_get]
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ R a b →
    ((∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get t { val := i, isLt := (_ : i < length t) })) ↔
      ∀ (n : ℕ) (h : n + 1 < length (a :: b :: t) - 1),
        R (get (b :: t) { val := n, isLt := (_ : n < length (b :: t)) })
          (get t { val := n, isLt := (_ : n < length t) }))
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ (R a b ∧
      ∀ (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 (a :: b :: t) - 1),
        R (get (a :: b :: t) { val := 0, isLt := (_ : 0 < length (a :: b :: t)) })
          (get (a :: b :: t) { val := 0 + 1, isLt := (_ : succ 0 < length (a :: b :: t)) })) ∧
      ∀ (n : ℕ) (h : n + 1 < length (a :: b :: t) - 1),
        R (get (a :: b :: t) { val := n + 1, isLt := (_ : n + 1 < length (a :: b :: t)) })
          (get (a :: b :: t) { val := n + 1 + 1, isLt := (_ : succ (n + 1) < length (a :: b :: t)) })
simp
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ R a b →
    ((∀ (i : ℕ) (h : i < length t),
        R (get (b :: t) { val := i, isLt := (_ : i < succ (length t)) })
          (get t { val := i, isLt := (_ : succ (i + 0) ≤ length t) })) ↔
      ∀ (n : ℕ) (h : n + 1 < length t + 1),
        R (get (b :: t) { val := n, isLt := (_ : succ (n + 0) ≤ length (b :: t)) })
          (get t { val := n, isLt := (_ : succ (n + 0) ≤ length t) }))
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ R a b →
    ((∀ (i : ℕ) (h : i < length (b :: t) - 1),
        R (get (b :: t) { val := i, isLt := (_ : i < length (b :: t)) })
          (get t { val := i, isLt := (_ : i < length t) })) ↔
      ∀ (n : ℕ) (h : n + 1 < length (a :: b :: t) - 1),
        R (get (b :: t) { val := n, isLt := (_ : n < length (b :: t)) })
          (get t { val := n, isLt := (_ : n < length t) }))
dsimp [succ_sub_one]
no goals
α : Type u
β : Type v
R✝ r : α → α → Prop
l l₁ l₂ : List α
a✝ b✝ : α
R : α → α → Prop
a b : α
t : List α
⊢ R a b →
    ((∀ (i : ℕ) (h : i < length t),
        R (get (b :: t) { val := i, isLt := (_ : i < succ (length t)) })
          (get t { val := i, isLt := (_ : succ (i + 0) ≤ length t) })) ↔
      ∀ (n : ℕ) (h : n + 1 < length t + 1),
        R (get (b :: t) { val := n, isLt := (_ : succ (n + 0) ≤ length (b :: t)) })
          (get t { val := n, isLt := (_ : succ (n + 0) ≤ length t) }))
exact fun _ => ⟨fun h i hi => h i (Nat.lt_of_succ_lt_succ hi),
                fun h i hi => h i (Nat.succ_lt_succ hi)⟩