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

State before:
α : 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 : (map f as)[i] = (map f as)[j]
⊢ i = j
Tactic:
conv at h =>
  simp only [Array.getElem_map]
State after:
α : 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 = j

State before:
α : 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 = j
Tactic:
apply has.get_inj
State after:
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

State before:
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
Tactic:
apply hf _ _ h
State after:
no goals