no goals
ι : Type u
α : ι → Type v
i j : ι
l : List ι
f : (i : ι) → α i
t : (i : ι) → Set (α i)
⊢ TProd.mk [] ⁻¹' Set.tprod [] t = pi {i | i ∈ []} t
simp [Set.tprod]
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
ι : 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
ext f
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
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
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]
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
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
rw [Set.tprod, TProd.mk, mem_preimage, mem_pi, prod_mk_mem_set_prod_eq]
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
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
simp_rw [mem_setOf_eq, mem_cons]
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)
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
rw [forall_eq_or_imp, and_congr_right_iff]
no goals
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)
exact fun _ => 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 l ⁻¹' Set.tprod l t ↔ f ∈ pi {x | x ∈ l} t
ι : 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
change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ { x | x ∈ l }.pi t
no goals
ι : 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
rw [mk_preimage_tprod l t]