case inl
α : Type u_1
β : Type u_2
γ : Type ?u.190319
ι : Sort u_3
ι' : Sort ?u.190325
ι₂ : Sort ?u.190328
κ : ι → Sort ?u.190333
κ₁ : ι → Sort ?u.190338
κ₂ : ι → Sort ?u.190343
κ' : ι' → Sort ?u.190348
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : IsEmpty ι
⊢ (f '' ⋂ (i : ι), s i) = ⋂ (i : ι), f '' s i

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.190319
ι : Sort u_3
ι' : Sort ?u.190325
ι₂ : Sort ?u.190328
κ : ι → Sort ?u.190333
κ₁ : ι → Sort ?u.190338
κ₂ : ι → Sort ?u.190343
κ' : ι' → Sort ?u.190348
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : Nonempty ι
⊢ (f '' ⋂ (i : ι), s i) = ⋂ (i : ι), f '' s i
α : Type u_1
β : Type u_2
γ : Type ?u.190319
ι : Sort u_3
ι' : Sort ?u.190325
ι₂ : Sort ?u.190328
κ : ι → Sort ?u.190333
κ₁ : ι → Sort ?u.190338
κ₂ : ι → Sort ?u.190343
κ' : ι' → Sort ?u.190348
f : α → β
hf : Bijective f
s : ι → Set α
⊢ (f '' ⋂ (i : ι), s i) = ⋂ (i : ι), f '' s i
cases isEmpty_or_nonempty ι
no goals
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.190319
ι : Sort u_3
ι' : Sort ?u.190325
ι₂ : Sort ?u.190328
κ : ι → Sort ?u.190333
κ₁ : ι → Sort ?u.190338
κ₂ : ι → Sort ?u.190343
κ' : ι' → Sort ?u.190348
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : IsEmpty ι
⊢ (f '' ⋂ (i : ι), s i) = ⋂ (i : ι), f '' s i
simp_rw [iInter_of_empty, image_univ_of_surjective hf.surjective]
no goals
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.190319
ι : Sort u_3
ι' : Sort ?u.190325
ι₂ : Sort ?u.190328
κ : ι → Sort ?u.190333
κ₁ : ι → Sort ?u.190338
κ₂ : ι → Sort ?u.190343
κ' : ι' → Sort ?u.190348
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : Nonempty ι
⊢ (f '' ⋂ (i : ι), s i) = ⋂ (i : ι), f '' s i
exact (hf.injective.injOn _).image_iInter_eq