Theorem: Array.nodup_iff_getElem_inj (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
inst✝ : DecidableEq α
x : Array α
⊢ Nodup x ↔ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
induction x using cons_induction with
| empty =>
  simp only [nodup_empty, true_iff]
  intro i; exact i.elim0
| cons a x IH =>
  rewrite [nodup_cons, IH]; clear IH
  constructor
  . intro h i j hxij
    rcases i with ⟨i,hi⟩; rcases j with ⟨j,hj⟩
    cases i <;> cases j <;> simp at hxij ⊢
    . exfalso; apply h.1
      rewrite [hxij]; exact getElem_mem x _
    . exfalso; apply h.1
      rewrite [← hxij]; exact getElem_mem x _
    . exact Fin.val_eq_of_eq <| h.2 ⟨_, Nat.lt_of_succ_lt_succ hi⟩ ⟨_, Nat.lt_of_succ_lt_succ hj⟩ hxij
  . intro h
    constructor
    . intro hmem
      have ⟨i,hi, hxi⟩ := mem_iff_get.mp hmem
      specialize h ⟨i+1, Nat.succ_lt_succ hi⟩ ⟨0, x.size.zero_lt_succ⟩ hxi
      cases h
    . intro i j
      specialize h i.succ j.succ
      simp only [size_cons, Fin.val_succ, getElem_cons_succ, Fin.succ_inj] at h
      exact h
State after:
no goals

State before:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ Nodup #[] ↔ ∀ (i j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j
Tactic:
simp only [nodup_empty, true_iff]
State after:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ ∀ (i j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j

State before:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ ∀ (i j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j
Tactic:
intro i
State after:
case empty
α : Type u
inst✝ : DecidableEq α
i : Fin (size #[])
⊢ ∀ (j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j

State before:
case empty
α : Type u
inst✝ : DecidableEq α
i : Fin (size #[])
⊢ ∀ (j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j
Tactic:
exact i.elim0
State after:
no goals

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
⊢ Nodup (cons a x) ↔ ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
Tactic:
rewrite [nodup_cons, IH]
State after:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) ↔
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) ↔
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
Tactic:
clear IH
State after:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) ↔
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) ↔
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
Tactic:
constructor
State after:
case cons.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) →
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j

case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j

State before:
case cons.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) →
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j

case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
. intro h i j hxij
  rcases i with ⟨i,hi⟩; rcases j with ⟨j,hj⟩
  cases i <;> cases j <;> simp at hxij ⊢
  . exfalso; apply h.1
    rewrite [hxij]; exact getElem_mem x _
  . exfalso; apply h.1
    rewrite [← hxij]; exact getElem_mem x _
  . exact Fin.val_eq_of_eq <| h.2 ⟨_, Nat.lt_of_succ_lt_succ hi⟩ ⟨_, Nat.lt_of_succ_lt_succ hj⟩ hxij
State after:
case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j

State before:
case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
. intro h
  constructor
  . intro hmem
    have ⟨i,hi, hxi⟩ := mem_iff_get.mp hmem
    specialize h ⟨i+1, Nat.succ_lt_succ hi⟩ ⟨0, x.size.zero_lt_succ⟩ hxi
    cases h
  . intro i j
    specialize h i.succ j.succ
    simp only [size_cons, Fin.val_succ, getElem_cons_succ, Fin.succ_inj] at h
    exact h
State after:
no goals

State before:
case cons.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j) →
    ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
Tactic:
intro h i j hxij
State after:
case cons.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
i j : Fin (size (cons a x))
hxij : (cons a x)[↑i] = (cons a x)[↑j]
⊢ i = j

State before:
case cons.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
i j : Fin (size (cons a x))
hxij : (cons a x)[↑i] = (cons a x)[↑j]
⊢ i = j
Tactic:
rcases i with ⟨i,hi⟩
State after:
case cons.mp.mk
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
j : Fin (size (cons a x))
i : Nat
hi : i < size (cons a x)
hxij : (cons a x)[↑{ val := i, isLt := hi }] = (cons a x)[↑j]
⊢ { val := i, isLt := hi } = j

State before:
case cons.mp.mk
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
j : Fin (size (cons a x))
i : Nat
hi : i < size (cons a x)
hxij : (cons a x)[↑{ val := i, isLt := hi }] = (cons a x)[↑j]
⊢ { val := i, isLt := hi } = j
Tactic:
rcases j with ⟨j,hj⟩
State after:
case cons.mp.mk.mk
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
i : Nat
hi : i < size (cons a x)
j : Nat
hj : j < size (cons a x)
hxij : (cons a x)[↑{ val := i, isLt := hi }] = (cons a x)[↑{ val := j, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }

State before:
case cons.mp.mk.mk
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
i : Nat
hi : i < size (cons a x)
j : Nat
hj : j < size (cons a x)
hxij : (cons a x)[↑{ val := i, isLt := hi }] = (cons a x)[↑{ val := j, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
Tactic:
cases i <;> cases j <;> simp at hxij ⊢
State after:
case cons.mp.mk.mk.zero.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ 0 = { val := Nat.succ n✝, isLt := hj }

case cons.mp.mk.mk.succ.zero
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ { val := Nat.succ n✝, isLt := hi } = 0

case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝

State before:
case cons.mp.mk.mk.zero.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ 0 = { val := Nat.succ n✝, isLt := hj }

case cons.mp.mk.mk.succ.zero
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ { val := Nat.succ n✝, isLt := hi } = 0

case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
Tactic:
. exfalso; apply h.1
  rewrite [hxij]; exact getElem_mem x _
State after:
case cons.mp.mk.mk.succ.zero
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ { val := Nat.succ n✝, isLt := hi } = 0

case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝

State before:
case cons.mp.mk.mk.succ.zero
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ { val := Nat.succ n✝, isLt := hi } = 0

case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
Tactic:
. exfalso; apply h.1
  rewrite [← hxij]; exact getElem_mem x _
State after:
case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝

State before:
case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
Tactic:
. exact Fin.val_eq_of_eq <| h.2 ⟨_, Nat.lt_of_succ_lt_succ hi⟩ ⟨_, Nat.lt_of_succ_lt_succ hj⟩ hxij
State after:
no goals

State before:
case cons.mp.mk.mk.zero.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ 0 = { val := Nat.succ n✝, isLt := hj }
Tactic:
exfalso
State after:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ False

State before:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ False
Tactic:
apply h.1
State after:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ a ∈ x

State before:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ a ∈ x
Tactic:
rewrite [hxij]
State after:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ x[n✝] ∈ x

State before:
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ x[n✝] ∈ x
Tactic:
exact getElem_mem x _
State after:
no goals

State before:
case cons.mp.mk.mk.succ.zero
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ { val := Nat.succ n✝, isLt := hi } = 0
Tactic:
exfalso
State after:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ False

State before:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ False
Tactic:
apply h.1
State after:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ a ∈ x

State before:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ a ∈ x
Tactic:
rewrite [← hxij]
State after:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ x[n✝] ∈ x

State before:
case cons.mp.mk.mk.succ.zero.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝ : Nat
hi : Nat.succ n✝ < size (cons a x)
hj : Nat.zero < size (cons a x)
hxij : x[n✝] = a
⊢ x[n✝] ∈ x
Tactic:
exact getElem_mem x _
State after:
no goals

State before:
case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
Tactic:
exact Fin.val_eq_of_eq <| h.2 ⟨_, Nat.lt_of_succ_lt_succ hi⟩ ⟨_, Nat.lt_of_succ_lt_succ hj⟩ hxij
State after:
no goals

State before:
case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j) →
    ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
intro h
State after:
case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j

State before:
case cons.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
constructor
State after:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ¬a ∈ x

case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j

State before:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ¬a ∈ x

case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
. intro hmem
  have ⟨i,hi, hxi⟩ := mem_iff_get.mp hmem
  specialize h ⟨i+1, Nat.succ_lt_succ hi⟩ ⟨0, x.size.zero_lt_succ⟩ hxi
  cases h
State after:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j

State before:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
. intro i j
  specialize h i.succ j.succ
  simp only [size_cons, Fin.val_succ, getElem_cons_succ, Fin.succ_inj] at h
  exact h
State after:
no goals

State before:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ¬a ∈ x
Tactic:
intro hmem
State after:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
hmem : a ∈ x
⊢ False

State before:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
hmem : a ∈ x
⊢ False
Tactic:
have ⟨i,hi, hxi⟩ := mem_iff_get.mp hmem
State after:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
hmem : a ∈ x
i : Nat
hi : i < size x
hxi : x[i] = a
⊢ False

State before:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
hmem : a ∈ x
i : Nat
hi : i < size x
hxi : x[i] = a
⊢ False
Tactic:
specialize h ⟨i+1, Nat.succ_lt_succ hi⟩ ⟨0, x.size.zero_lt_succ⟩ hxi
State after:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
hmem : a ∈ x
i : Nat
hi : i < size x
hxi : x[i] = a
h :
  { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (List.length x.data)) } =
    { val := 0, isLt := (_ : 0 < Nat.succ (size x)) }
⊢ False

State before:
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
hmem : a ∈ x
i : Nat
hi : i < size x
hxi : x[i] = a
h :
  { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (List.length x.data)) } =
    { val := 0, isLt := (_ : 0 < Nat.succ (size x)) }
⊢ False
Tactic:
cases h
State after:
no goals

State before:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
⊢ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
Tactic:
intro i j
State after:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
i j : Fin (size x)
⊢ x[↑i] = x[↑j] → i = j

State before:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
i j : Fin (size x)
⊢ x[↑i] = x[↑j] → i = j
Tactic:
specialize h i.succ j.succ
State after:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
i j : Fin (size x)
h : (cons a x)[↑(Fin.succ i)] = (cons a x)[↑(Fin.succ j)] → Fin.succ i = Fin.succ j
⊢ x[↑i] = x[↑j] → i = j

State before:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
i j : Fin (size x)
h : (cons a x)[↑(Fin.succ i)] = (cons a x)[↑(Fin.succ j)] → Fin.succ i = Fin.succ j
⊢ x[↑i] = x[↑j] → i = j
Tactic:
simp only [size_cons, Fin.val_succ, getElem_cons_succ, Fin.succ_inj] at h
State after:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
i j : Fin (size x)
h : x[↑i] = x[↑j] → i = j
⊢ x[↑i] = x[↑j] → i = j

State before:
case cons.mpr.right
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
i j : Fin (size x)
h : x[↑i] = x[↑j] → i = j
⊢ x[↑i] = x[↑j] → i = j
Tactic:
exact h
State after:
no goals