case h₁
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
⊢ v.fst = w.fst

case h₂
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
⊢ v.snd = w.snd
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
⊢ v = w
apply Prod.ext
case h₂
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
⊢ v.snd = w.snd
case h₁
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
⊢ v.fst = w.fst

case h₂
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
⊢ v.snd = w.snd
rw [← elim_self v, hvw, elim_self]
case h₂
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
j : ι
hj : j ∈ is
⊢ TProd.elim v.snd hj = TProd.elim w.snd hj
case h₂
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
⊢ v.snd = w.snd
refine' ext (nodup_cons.mp hl).2 fun j hj => _
no goals
case h₂
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : Nodup (i :: is)
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), TProd.elim v hi = TProd.elim w hi
j : ι
hj : j ∈ is
⊢ TProd.elim v.snd hj = TProd.elim w.snd hj
rw [← elim_of_mem hl, hvw, elim_of_mem hl]