Theorem: List.Nodup.map (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ Nodup (List.map f l)
Tactic:
apply nodup_of_get_inj
State after:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ ∀ (i j : Nat) (x : i < length (List.map f l)) (x_1 : j < length (List.map f l)),
    (List.map f l)[i] = (List.map f l)[j] → i = j

State before:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ ∀ (i j : Nat) (x : i < length (List.map f l)) (x_1 : j < length (List.map f l)),
    (List.map f l)[i] = (List.map f l)[j] → i = j
Tactic:
intro i j hi hj
State after:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
⊢ (List.map f l)[i] = (List.map f l)[j] → i = j

State before:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
⊢ (List.map f l)[i] = (List.map f l)[j] → i = j
Tactic:
simp only [getElem_eq_get, get_map]
State after:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
⊢ f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
      f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) }) →
    i = j

State before:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
⊢ f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
      f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) }) →
    i = j
Tactic:
intro hfij
State after:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
hfij :
  f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
    f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) })
⊢ i = j

State before:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
hfij :
  f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
    f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) })
⊢ i = j
Tactic:
specialize hf _ _ hfij
State after:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
hfij :
  f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
    f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) })
hf :
  get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) } =
    get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) }
⊢ i = j

State before:
case h
α : Type u
β : Type v
l : List α
nodup : Nodup l
f : α → β
i j : Nat
hi : i < length (List.map f l)
hj : j < length (List.map f l)
hfij :
  f (get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) }) =
    f (get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) })
hf :
  get l { val := i, isLt := (_ : { val := i, isLt := hi }.val < length l) } =
    get l { val := j, isLt := (_ : { val := j, isLt := hj }.val < length l) }
⊢ i = j
Tactic:
exact nodup.get_inj i j hf
State after:
no goals