case hji
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hl : Nodup (i :: l)
hj : j ∈ l
v : TProd α (i :: l)
⊢ j ≠ i
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hl : Nodup (i :: l)
hj : j ∈ l
v : TProd α (i :: l)
⊢ TProd.elim v (_ : j ∈ i :: l) = TProd.elim v.snd hj
apply elim_of_ne
case hji
ι : Type u
α : ι → Type v
j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hj : j ∈ l
hl : Nodup (j :: l)
v : TProd α (j :: l)
⊢ False
case hji
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hl : Nodup (i :: l)
hj : j ∈ l
v : TProd α (i :: l)
⊢ j ≠ i
rintro rfl
no goals
case hji
ι : Type u
α : ι → Type v
j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hj : j ∈ l
hl : Nodup (j :: l)
v : TProd α (j :: l)
⊢ False
exact hl.not_mem hj