α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a : α
l : List α
⊢ ∀ (i j : Fin (length [])), i < j → R (get [] i) (get [] j)
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a : α
l : List α
⊢ Pairwise R [] ↔ ∀ (i j : Fin (length [])), i < j → R (get [] i) (get [] j)
simp only [Pairwise.nil, true_iff_iff]
no goals
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a : α
l : List α
⊢ ∀ (i j : Fin (length [])), i < j → R (get [] i) (get [] j)
exact fun i j _h => (Nat.not_lt_zero j).elim j.2
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
⊢ ((∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)) ↔
    ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
⊢ Pairwise R (a :: l) ↔ ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
rw [pairwise_cons, pairwise_iff_get]
case refine'_1
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i j : Fin (length (a :: l))
hij : i < j
⊢ R (get (a :: l) i) (get (a :: l) j)

case refine'_2
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
a' : α
m : a' ∈ l
⊢ R a a'

case refine'_3
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
i j : Fin (length l)
hij : i < j
⊢ R (get l i) (get l j)
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
⊢ ((∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)) ↔
    ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
refine'
  ⟨fun H i j hij => _, fun H =>
    ⟨fun a' m => _, fun i j hij => _⟩⟩
no goals
case refine'_3
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
i j : Fin (length l)
hij : i < j
⊢ R (get l i) (get l j)
. simpa using H i.succ j.succ (show i.1.succ < j.1.succ from Nat.succ_lt_succ hij)
case refine'_1.mk
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i : Fin (length (a :: l))
j : ℕ
hj : j < length (a :: l)
hij : i < { val := j, isLt := hj }
⊢ R (get (a :: l) i) (get (a :: l) { val := j, isLt := hj })
case refine'_1
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i j : Fin (length (a :: l))
hij : i < j
⊢ R (get (a :: l) i) (get (a :: l) j)
cases' j with j hj
case refine'_1.mk.zero
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i : Fin (length (a :: l))
hj : zero < length (a :: l)
hij : i < { val := zero, isLt := hj }
⊢ R (get (a :: l) i) (get (a :: l) { val := zero, isLt := hj })

case refine'_1.mk.succ
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i : Fin (length (a :: l))
j : ℕ
hj : succ j < length (a :: l)
hij : i < { val := succ j, isLt := hj }
⊢ R (get (a :: l) i) (get (a :: l) { val := succ j, isLt := hj })
case refine'_1.mk
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i : Fin (length (a :: l))
j : ℕ
hj : j < length (a :: l)
hij : i < { val := j, isLt := hj }
⊢ R (get (a :: l) i) (get (a :: l) { val := j, isLt := hj })
cases' j with j
case refine'_1.mk.succ.mk
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
j : ℕ
hj : succ j < length (a :: l)
i : ℕ
hi : i < length (a :: l)
hij : { val := i, isLt := hi } < { val := succ j, isLt := hj }
⊢ R (get (a :: l) { val := i, isLt := hi }) (get (a :: l) { val := succ j, isLt := hj })
case refine'_1.mk.succ
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i : Fin (length (a :: l))
j : ℕ
hj : succ j < length (a :: l)
hij : i < { val := succ j, isLt := hj }
⊢ R (get (a :: l) i) (get (a :: l) { val := succ j, isLt := hj })
cases' i with i hi
case refine'_1.mk.succ.mk.zero
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
j : ℕ
hj : succ j < length (a :: l)
hi : zero < length (a :: l)
hij : { val := zero, isLt := hi } < { val := succ j, isLt := hj }
⊢ R (get (a :: l) { val := zero, isLt := hi }) (get (a :: l) { val := succ j, isLt := hj })

case refine'_1.mk.succ.mk.succ
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
j : ℕ
hj : succ j < length (a :: l)
i : ℕ
hi : succ i < length (a :: l)
hij : { val := succ i, isLt := hi } < { val := succ j, isLt := hj }
⊢ R (get (a :: l) { val := succ i, isLt := hi }) (get (a :: l) { val := succ j, isLt := hj })
case refine'_1.mk.succ.mk
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
j : ℕ
hj : succ j < length (a :: l)
i : ℕ
hi : i < length (a :: l)
hij : { val := i, isLt := hi } < { val := succ j, isLt := hj }
⊢ R (get (a :: l) { val := i, isLt := hi }) (get (a :: l) { val := succ j, isLt := hj })
cases' i with i
no goals
case refine'_1.mk.zero
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i : Fin (length (a :: l))
hj : zero < length (a :: l)
hij : i < { val := zero, isLt := hj }
⊢ R (get (a :: l) i) (get (a :: l) { val := zero, isLt := hj })
exact (Nat.not_lt_zero _).elim hij
no goals
case refine'_1.mk.succ.mk.zero
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
j : ℕ
hj : succ j < length (a :: l)
hi : zero < length (a :: l)
hij : { val := zero, isLt := hi } < { val := succ j, isLt := hj }
⊢ R (get (a :: l) { val := zero, isLt := hi }) (get (a :: l) { val := succ j, isLt := hj })
exact H.1 _ (get_mem l _ _)
no goals
case refine'_1.mk.succ.mk.succ
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
j : ℕ
hj : succ j < length (a :: l)
i : ℕ
hi : succ i < length (a :: l)
hij : { val := succ i, isLt := hi } < { val := succ j, isLt := hj }
⊢ R (get (a :: l) { val := succ i, isLt := hi }) (get (a :: l) { val := succ j, isLt := hj })
exact H.2 _ _ (Nat.lt_of_succ_lt_succ hij)
case refine'_2.intro.refl
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
n : Fin (length l)
m : get l n ∈ l
⊢ R a (get l n)
case refine'_2
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
a' : α
m : a' ∈ l
⊢ R a a'
rcases get_of_mem m with ⟨n, h, rfl⟩
case refine'_2.intro.refl
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
n : Fin (length l)
m : get l n ∈ l
this :
  R (get (a :: l) { val := 0, isLt := (_ : 0 < length (a :: l)) })
    (get (a :: l) { val := ↑(Fin.succ n), isLt := (_ : succ ↑n < succ (length l)) })
⊢ R a (get l n)
case refine'_2.intro.refl
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
n : Fin (length l)
m : get l n ∈ l
⊢ R a (get l n)
have := H ⟨0, show 0 < (a::l).length from Nat.succ_pos _⟩ ⟨n.succ, Nat.succ_lt_succ n.2⟩
  (Nat.succ_pos n)
no goals
case refine'_2.intro.refl
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
n : Fin (length l)
m : get l n ∈ l
this :
  R (get (a :: l) { val := 0, isLt := (_ : 0 < length (a :: l)) })
    (get (a :: l) { val := ↑(Fin.succ n), isLt := (_ : succ ↑n < succ (length l)) })
⊢ R a (get l n)
simpa
no goals
case refine'_3
α : Type u_1
β : Type ?u.44959
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
i j : Fin (length l)
hij : i < j
⊢ R (get l i) (get l j)
simpa using H i.succ j.succ (show i.1.succ < j.1.succ from Nat.succ_lt_succ hij)