α : Type u_1
β : Type u_2
γ : Type ?u.186386
ι : Sort ?u.186389
ι' : Sort ?u.186392
ι₂ : Sort ?u.186395
κ : ι → Sort ?u.186400
κ₁ : ι → Sort ?u.186405
κ₂ : ι → Sort ?u.186410
κ' : ι' → Sort ?u.186415
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective (restrictPreimage (U i) f)
x : β
⊢ ∃ a, f a = x
α : Type u_1
β : Type u_2
γ : Type ?u.186386
ι : Sort ?u.186389
ι' : Sort ?u.186392
ι₂ : Sort ?u.186395
κ : ι → Sort ?u.186400
κ₁ : ι → Sort ?u.186405
κ₂ : ι → Sort ?u.186410
κ' : ι' → Sort ?u.186415
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Surjective f ↔ ∀ (i : ι), Surjective (restrictPreimage (U i) f)
refine' ⟨fun H i => (U i).restrictPreimage_surjective H, fun H x => _⟩
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.186386
ι : Sort ?u.186389
ι' : Sort ?u.186392
ι₂ : Sort ?u.186395
κ : ι → Sort ?u.186400
κ₁ : ι → Sort ?u.186405
κ₂ : ι → Sort ?u.186410
κ' : ι' → Sort ?u.186415
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective (restrictPreimage (U i) f)
x : β
i : ι
hi : x ∈ U i
⊢ ∃ a, f a = x
α : Type u_1
β : Type u_2
γ : Type ?u.186386
ι : Sort ?u.186389
ι' : Sort ?u.186392
ι₂ : Sort ?u.186395
κ : ι → Sort ?u.186400
κ₁ : ι → Sort ?u.186405
κ₂ : ι → Sort ?u.186410
κ' : ι' → Sort ?u.186415
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective (restrictPreimage (U i) f)
x : β
⊢ ∃ a, f a = x
obtain ⟨i, hi⟩ :=
  Set.mem_iUnion.mp
    (show x ∈ Set.iUnion U by rw [hU]; triv)
no goals
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.186386
ι : Sort ?u.186389
ι' : Sort ?u.186392
ι₂ : Sort ?u.186395
κ : ι → Sort ?u.186400
κ₁ : ι → Sort ?u.186405
κ₂ : ι → Sort ?u.186410
κ' : ι' → Sort ?u.186415
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective (restrictPreimage (U i) f)
x : β
i : ι
hi : x ∈ U i
⊢ ∃ a, f a = x
exact ⟨_, congr_arg Subtype.val (H i ⟨x, hi⟩).choose_spec⟩
α : Type u_1
β : Type u_2
γ : Type ?u.186386
ι : Sort ?u.186389
ι' : Sort ?u.186392
ι₂ : Sort ?u.186395
κ : ι → Sort ?u.186400
κ₁ : ι → Sort ?u.186405
κ₂ : ι → Sort ?u.186410
κ' : ι' → Sort ?u.186415
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective (restrictPreimage (U i) f)
x : β
⊢ x ∈ univ
α : Type u_1
β : Type u_2
γ : Type ?u.186386
ι : Sort ?u.186389
ι' : Sort ?u.186392
ι₂ : Sort ?u.186395
κ : ι → Sort ?u.186400
κ₁ : ι → Sort ?u.186405
κ₂ : ι → Sort ?u.186410
κ' : ι' → Sort ?u.186415
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective (restrictPreimage (U i) f)
x : β
⊢ x ∈ iUnion U
rw [hU]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.186386
ι : Sort ?u.186389
ι' : Sort ?u.186392
ι₂ : Sort ?u.186395
κ : ι → Sort ?u.186400
κ₁ : ι → Sort ?u.186405
κ₂ : ι → Sort ?u.186410
κ' : ι' → Sort ?u.186415
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective (restrictPreimage (U i) f)
x : β
⊢ x ∈ univ
triv