apply hf _ _ h
case a
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : f as[i] = f as[j]
⊢ as[i] = as[j]

case hi
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : f as[i] = f as[j]
⊢ i < size as

case hj
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : f as[i] = f as[j]
⊢ j < size as
no goals