Theorem: SizedArray.nodup_iff_get_inj (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ Nodup x ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
Tactic:
dsimp [Nodup]
State after:
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ Array.Nodup x.val ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j

State before:
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ Array.Nodup x.val ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
Tactic:
rewrite [Array.nodup_iff_getElem_inj]
State after:
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j) ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j

State before:
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j) ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
Tactic:
constructor
State after:
case mp
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j) → ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j

case mpr
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin n), x[↑i] = x[↑j] → i = j) → ∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j

State before:
case mp
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j) → ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j

case mpr
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin n), x[↑i] = x[↑j] → i = j) → ∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j
Tactic:
all_goals
  intro h i j hxij
  rcases i with ⟨i,hi⟩; rcases j with ⟨j,hj⟩
  specialize h ⟨i, x.size_eq.symm ▸ hi⟩ ⟨j, x.size_eq.symm ▸ hj⟩ hxij
  cases h; rfl
State after:
no goals

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

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

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

State before:
case mpr.mk.mk
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
h : ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
i : Nat
hi : i < Array.size x.val
j : Nat
hj : j < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := j, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
Tactic:
specialize h ⟨i, x.size_eq.symm ▸ hi⟩ ⟨j, x.size_eq.symm ▸ hj⟩ hxij
State after:
case mpr.mk.mk
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
i : Nat
hi : i < Array.size x.val
j : Nat
hj : j < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := j, isLt := hj }]
h : { val := i, isLt := (_ : i < n) } = { val := j, isLt := (_ : j < n) }
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }

State before:
case mpr.mk.mk
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
i : Nat
hi : i < Array.size x.val
j : Nat
hj : j < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := j, isLt := hj }]
h : { val := i, isLt := (_ : i < n) } = { val := j, isLt := (_ : j < n) }
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
Tactic:
cases h
State after:
case mpr.mk.mk.refl
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
i : Nat
hi hj : i < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := i, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := i, isLt := hj }

State before:
case mpr.mk.mk.refl
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
i : Nat
hi hj : i < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := i, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := i, isLt := hj }
Tactic:
rfl
State after:
no goals