α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : Fin (length l)), i < j → get l i ≠ get l j) ↔ ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ Nodup l ↔ ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
rw [Nodup, pairwise_iff_get]
case mp
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : Fin (length l)), i < j → get l i ≠ get l j) → ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j

case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j) → ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : Fin (length l)), i < j → get l i ≠ get l j) ↔ ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
constructor
case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j) → ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
case mp
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : Fin (length l)), i < j → get l i ≠ get l j) → ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j

case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j) → ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
. intro h i j hij hj
  rw [get?_eq_get (lt_trans hij hj), get?_eq_get hj, Ne.def, Option.some_inj]
  exact h _ _ hij
no goals
case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j) → ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
. intro h i j hij
  rw [Ne.def, ← Option.some_inj, ← get?_eq_get, ← get?_eq_get]
  exact h i j hij j.2
case mp
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
i j : ℕ
hij : i < j
hj : j < length l
⊢ get? l i ≠ get? l j
case mp
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : Fin (length l)), i < j → get l i ≠ get l j) → ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
intro h i j hij hj
case mp
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
i j : ℕ
hij : i < j
hj : j < length l
⊢ ¬get l { val := i, isLt := (_ : i < length l) } = get l { val := j, isLt := hj }
case mp
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
i j : ℕ
hij : i < j
hj : j < length l
⊢ get? l i ≠ get? l j
rw [get?_eq_get (lt_trans hij hj), get?_eq_get hj, Ne.def, Option.some_inj]
no goals
case mp
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
i j : ℕ
hij : i < j
hj : j < length l
⊢ ¬get l { val := i, isLt := (_ : i < length l) } = get l { val := j, isLt := hj }
exact h _ _ hij
case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
i j : Fin (length l)
hij : i < j
⊢ get l i ≠ get l j
case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
⊢ (∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j) → ∀ (i j : Fin (length l)), i < j → get l i ≠ get l j
intro h i j hij
case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
i j : Fin (length l)
hij : i < j
⊢ ¬get? l ↑i = get? l ↑j
case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
i j : Fin (length l)
hij : i < j
⊢ get l i ≠ get l j
rw [Ne.def, ← Option.some_inj, ← get?_eq_get, ← get?_eq_get]
no goals
case mpr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : ∀ (i j : ℕ), i < j → j < length l → get? l i ≠ get? l j
i j : Fin (length l)
hij : i < j
⊢ ¬get? l ↑i = get? l ↑j
exact h i j hij j.2