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

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

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

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

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

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

State before:
case h
α : Type u
β : Type v
p : α → Prop
l : List α
nodup : Nodup l
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ l → p a
i j : Nat
hi : i < length (List.pmap f l h)
hj : j < length (List.pmap f l h)
hfij :
  f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))
      (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }))) =
    f (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj }))
      (_ : p (get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj })))
f_inj :
  get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := i, isLt := hi }) =
    get l (Fin.cast (_ : length (List.pmap f l h) = length l) { val := j, isLt := hj })
⊢ i = j
Tactic:
exact nodup.get_inj i j f_inj
State after:
no goals