[GOAL]
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
v : TProd α (i :: is)
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ α j
[PROOFSTEP]
subst hji
[GOAL]
ι : Type u
α : ι → Type v
i j✝ : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
is : List ι
j : ι
v : TProd α (j :: is)
hj : j ∈ j :: is
⊢ α j
[PROOFSTEP]
exact v.1
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
v : TProd α (i :: l)
⊢ TProd.elim v (_ : i ∈ i :: l) = v.fst
[PROOFSTEP]
simp [TProd.elim]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hj : j ∈ i :: l
hji : j ≠ i
v : TProd α (i :: l)
⊢ TProd.elim v hj = TProd.elim v.snd (_ : j ∈ l)
[PROOFSTEP]
simp [TProd.elim, hji]
[GOAL]
ι : 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
[PROOFSTEP]
apply elim_of_ne
[GOAL]
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
[PROOFSTEP]
rintro rfl
[GOAL]
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
[PROOFSTEP]
exact hl.not_mem hj
[GOAL]
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
⊢ TProd.elim (TProd.mk (i :: is) f) hj = f j
[PROOFSTEP]
by_cases hji : j = i
[GOAL]
case pos
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ TProd.elim (TProd.mk (i :: is) f) hj = f j
[PROOFSTEP]
subst hji
[GOAL]
case pos
ι : Type u
α : ι → Type v
i j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ j :: is
⊢ TProd.elim (TProd.mk (j :: is) f) hj = f j
[PROOFSTEP]
simp
[GOAL]
case neg
ι : Type u
α : ι → Type v
i✝ j✝ : ι
l : List ι
f✝ : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ TProd.elim (TProd.mk (i :: is) f) hj = f j
[PROOFSTEP]
rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]
[GOAL]
ι : 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
[PROOFSTEP]
apply Prod.ext
[GOAL]
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
[PROOFSTEP]
rw [← elim_self v, hvw, elim_self]
[GOAL]
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
[PROOFSTEP]
refine' ext (nodup_cons.mp hl).2 fun j hj => _
[GOAL]
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
[PROOFSTEP]
rw [← elim_of_mem hl, hvw, elim_of_mem hl]
[GOAL]
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
v : TProd α l
i : ι
hi : i ∈ l
⊢ TProd.elim (TProd.mk l (TProd.elim' h v)) hi = TProd.elim v hi
[PROOFSTEP]
simp [elim_mk]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
t : (i : ι) → Set (α i)
⊢ TProd.mk [] ⁻¹' Set.tprod [] t = pi {i | i ∈ []} t
[PROOFSTEP]
simp [Set.tprod]
[GOAL]
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
⊢ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t = pi {i_1 | i_1 ∈ i :: l} t
[PROOFSTEP]
ext f
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t ↔ f ∈ pi {i_1 | i_1 ∈ i :: l} t
[PROOFSTEP]
have h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ i : ι, i ∈ l → f i ∈ t i :=
  by
  change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ {x | x ∈ l}.pi t
  rw [mk_preimage_tprod l t]
    -- `simp [Set.TProd, TProd.mk, this]` can close this goal but is slow.
[GOAL]
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
[PROOFSTEP]
change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ {x | x ∈ l}.pi t
[GOAL]
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ pi {x | x ∈ l} t
[PROOFSTEP]
rw [mk_preimage_tprod l t]
  -- `simp [Set.TProd, TProd.mk, this]` can close this goal but is slow.
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f ∈ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t ↔ f ∈ pi {i_1 | i_1 ∈ i :: l} t
[PROOFSTEP]
rw [Set.tprod, TProd.mk, mem_preimage, mem_pi, prod_mk_mem_set_prod_eq]
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 ∈ {i_2 | i_2 ∈ i :: l} → f i_1 ∈ t i_1
[PROOFSTEP]
simp_rw [mem_setOf_eq, mem_cons]
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ l → f i_1 ∈ t i_1
[PROOFSTEP]
rw [forall_eq_or_imp, and_congr_right_iff]
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f✝ : (i : ι) → α i
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i → (TProd.mk l f ∈ Set.tprod l t ↔ ∀ (a : ι), a ∈ l → f a ∈ t a)
[PROOFSTEP]
exact fun _ => h
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
⊢ TProd.elim' h ⁻¹' pi univ t = Set.tprod l t
[PROOFSTEP]
have h2 : {i | i ∈ l} = univ := by
  ext i
  simp [h]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
⊢ {i | i ∈ l} = univ
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u
α : ι → Type v
i✝ j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
i : ι
⊢ i ∈ {i | i ∈ l} ↔ i ∈ univ
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ TProd.elim' h ⁻¹' pi univ t = Set.tprod l t
[PROOFSTEP]
rw [← h2, ← mk_preimage_tprod, preimage_preimage]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x => TProd.mk l (TProd.elim' h x)) ⁻¹' Set.tprod l t = Set.tprod l t
[PROOFSTEP]
simp only [TProd.mk_elim hnd h]
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x => x) ⁻¹' Set.tprod l t = Set.tprod l t
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u
α : ι → Type v
i j : ι
l✝ : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
l : List ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ Set.tprod l t = Set.tprod l t
[PROOFSTEP]
rfl
