Theorem: Array.nodup_ofFn (Fifteen/Data/Array/Basic.lean)

State before:
α : Type u
n : Nat
f : Fin n → α
hf : ∀ (i j : Fin n), f i = f j → i = j
i j : Nat
hi : i < size (ofFn f)
hj : j < size (ofFn f)
h : (ofFn f)[i] = (ofFn f)[j]
⊢ i = j
Tactic:
simp only [Array.getElem_ofFn] at h
State after:
α : Type u
n : Nat
f : Fin n → α
hf : ∀ (i j : Fin n), f i = f j → i = j
i j : Nat
hi : i < size (ofFn f)
hj : j < size (ofFn f)
h : f { val := i, isLt := (_ : i < n) } = f { val := j, isLt := (_ : j < n) }
⊢ i = j

State before:
α : Type u
n : Nat
f : Fin n → α
hf : ∀ (i j : Fin n), f i = f j → i = j
i j : Nat
hi : i < size (ofFn f)
hj : j < size (ofFn f)
h : f { val := i, isLt := (_ : i < n) } = f { val := j, isLt := (_ : j < n) }
⊢ i = j
Tactic:
cases hf _ _ h
State after:
case refl
α : Type u
n : Nat
f : Fin n → α
hf : ∀ (i j : Fin n), f i = f j → i = j
i : Nat
hi hj : i < size (ofFn f)
h : f { val := i, isLt := (_ : i < n) } = f { val := i, isLt := (_ : i < n) }
⊢ i = i

State before:
case refl
α : Type u
n : Nat
f : Fin n → α
hf : ∀ (i j : Fin n), f i = f j → i = j
i : Nat
hi hj : i < size (ofFn f)
h : f { val := i, isLt := (_ : i < n) } = f { val := i, isLt := (_ : i < n) }
⊢ i = i
Tactic:
rfl
State after:
no goals