case mk
α : 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
j : Fin (length l)
i : ℕ
hi : i < length l
hg : get l { val := i, isLt := hi } = get l j
⊢ { val := i, isLt := hi } = j
α : 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 : Fin (length l)
hg : get l i = get l j
⊢ i = j
cases' i with i hi
case mk.mk
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
case mk
α : 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
j : Fin (length l)
i : ℕ
hi : i < length l
hg : get l { val := i, isLt := hi } = get l j
⊢ { val := i, isLt := hi } = j
cases' j with j hj
case mk.mk.inl
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hij : i < j
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }

case mk.mk.inr.inl
α : 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 : ℕ
hi hj : i < length l
hg : get l { val := i, isLt := hi } = get l { val := i, isLt := hj }
⊢ { val := i, isLt := hi } = { val := i, isLt := hj }

case mk.mk.inr.inr
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hji : j < i
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
case mk.mk
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
rcases lt_trichotomy i j with (hij | rfl | hji)
case mk.mk.inr.inl
α : 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 : ℕ
hi hj : i < length l
hg : get l { val := i, isLt := hi } = get l { val := i, isLt := hj }
⊢ { val := i, isLt := hi } = { val := i, isLt := hj }

case mk.mk.inr.inr
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hji : j < i
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
case mk.mk.inl
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hij : i < j
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }

case mk.mk.inr.inl
α : 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 : ℕ
hi hj : i < length l
hg : get l { val := i, isLt := hi } = get l { val := i, isLt := hj }
⊢ { val := i, isLt := hi } = { val := i, isLt := hj }

case mk.mk.inr.inr
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hji : j < i
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
. exact (h ⟨i, hi⟩ ⟨j, hj⟩ hij hg).elim
case mk.mk.inr.inr
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hji : j < i
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
case mk.mk.inr.inl
α : 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 : ℕ
hi hj : i < length l
hg : get l { val := i, isLt := hi } = get l { val := i, isLt := hj }
⊢ { val := i, isLt := hi } = { val := i, isLt := hj }

case mk.mk.inr.inr
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hji : j < i
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
. rfl
no goals
case mk.mk.inr.inr
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hji : j < i
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
. exact (h ⟨j, hj⟩ ⟨i, hi⟩ hji hg.symm).elim
no goals
case mk.mk.inl
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hij : i < j
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
exact (h ⟨i, hi⟩ ⟨j, hj⟩ hij hg).elim
no goals
case mk.mk.inr.inl
α : 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 : ℕ
hi hj : i < length l
hg : get l { val := i, isLt := hi } = get l { val := i, isLt := hj }
⊢ { val := i, isLt := hi } = { val := i, isLt := hj }
rfl
no goals
case mk.mk.inr.inr
α : 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 : ℕ
hi : i < length l
j : ℕ
hj : j < length l
hg : get l { val := i, isLt := hi } = get l { val := j, isLt := hj }
hji : j < i
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
exact (h ⟨j, hj⟩ ⟨i, hi⟩ hji hg.symm).elim