α : Type u_1
β : Type u_2
γ : Type ?u.186792
ι : Sort ?u.186795
ι' : Sort ?u.186798
ι₂ : Sort ?u.186801
κ : ι → Sort ?u.186806
κ₁ : ι → Sort ?u.186811
κ₂ : ι → Sort ?u.186816
κ' : ι' → Sort ?u.186821
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ ((∀ (i : ι), Injective (restrictPreimage (U i) f)) ∧ ∀ (i : ι), Surjective (restrictPreimage (U i) f)) ↔
    ∀ (i : ι), Bijective (restrictPreimage (U i) f)
α : Type u_1
β : Type u_2
γ : Type ?u.186792
ι : Sort ?u.186795
ι' : Sort ?u.186798
ι₂ : Sort ?u.186801
κ : ι → Sort ?u.186806
κ₁ : ι → Sort ?u.186811
κ₂ : ι → Sort ?u.186816
κ' : ι' → Sort ?u.186821
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Bijective f ↔ ∀ (i : ι), Bijective (restrictPreimage (U i) f)
rw [Bijective, injective_iff_injective_of_iUnion_eq_univ hU,
  surjective_iff_surjective_of_iUnion_eq_univ hU]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.186792
ι : Sort ?u.186795
ι' : Sort ?u.186798
ι₂ : Sort ?u.186801
κ : ι → Sort ?u.186806
κ₁ : ι → Sort ?u.186811
κ₂ : ι → Sort ?u.186816
κ' : ι' → Sort ?u.186821
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ ((∀ (i : ι), Injective (restrictPreimage (U i) f)) ∧ ∀ (i : ι), Surjective (restrictPreimage (U i) f)) ↔
    ∀ (i : ι), Bijective (restrictPreimage (U i) f)
simp [Bijective, forall_and]