α : Type u_1
β : Type u_2
γ : Type ?u.185953
ι : Sort ?u.185956
ι' : Sort ?u.185959
ι₂ : Sort ?u.185962
κ : ι → Sort ?u.185967
κ₁ : ι → Sort ?u.185972
κ₂ : ι → Sort ?u.185977
κ' : ι' → Sort ?u.185982
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective (restrictPreimage (U i) f)
x y : α
e : f x = f y
⊢ x = y
α : Type u_1
β : Type u_2
γ : Type ?u.185953
ι : Sort ?u.185956
ι' : Sort ?u.185959
ι₂ : Sort ?u.185962
κ : ι → Sort ?u.185967
κ₁ : ι → Sort ?u.185972
κ₂ : ι → Sort ?u.185977
κ' : ι' → Sort ?u.185982
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Injective f ↔ ∀ (i : ι), Injective (restrictPreimage (U i) f)
refine' ⟨fun H i => (U i).restrictPreimage_injective H, fun H x y e => _⟩
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.185953
ι : Sort ?u.185956
ι' : Sort ?u.185959
ι₂ : Sort ?u.185962
κ : ι → Sort ?u.185967
κ₁ : ι → Sort ?u.185972
κ₂ : ι → Sort ?u.185977
κ' : ι' → Sort ?u.185982
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective (restrictPreimage (U i) f)
x y : α
e : f x = f y
i : ι
hi : f x ∈ U i
⊢ x = y
α : Type u_1
β : Type u_2
γ : Type ?u.185953
ι : Sort ?u.185956
ι' : Sort ?u.185959
ι₂ : Sort ?u.185962
κ : ι → Sort ?u.185967
κ₁ : ι → Sort ?u.185972
κ₂ : ι → Sort ?u.185977
κ' : ι' → Sort ?u.185982
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective (restrictPreimage (U i) f)
x y : α
e : f x = f y
⊢ x = y
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp
    (show f x ∈ Set.iUnion U by rw [hU]; triv)
no goals
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.185953
ι : Sort ?u.185956
ι' : Sort ?u.185959
ι₂ : Sort ?u.185962
κ : ι → Sort ?u.185967
κ₁ : ι → Sort ?u.185972
κ₂ : ι → Sort ?u.185977
κ' : ι' → Sort ?u.185982
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective (restrictPreimage (U i) f)
x y : α
e : f x = f y
i : ι
hi : f x ∈ U i
⊢ x = y
injection @H i ⟨x, hi⟩ ⟨y, show f y ∈ U i from e ▸ hi⟩ (Subtype.ext e)
α : Type u_1
β : Type u_2
γ : Type ?u.185953
ι : Sort ?u.185956
ι' : Sort ?u.185959
ι₂ : Sort ?u.185962
κ : ι → Sort ?u.185967
κ₁ : ι → Sort ?u.185972
κ₂ : ι → Sort ?u.185977
κ' : ι' → Sort ?u.185982
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective (restrictPreimage (U i) f)
x y : α
e : f x = f y
⊢ f x ∈ univ
α : Type u_1
β : Type u_2
γ : Type ?u.185953
ι : Sort ?u.185956
ι' : Sort ?u.185959
ι₂ : Sort ?u.185962
κ : ι → Sort ?u.185967
κ₁ : ι → Sort ?u.185972
κ₂ : ι → Sort ?u.185977
κ' : ι' → Sort ?u.185982
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective (restrictPreimage (U i) f)
x y : α
e : f x = f y
⊢ f x ∈ iUnion U
rw [hU]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.185953
ι : Sort ?u.185956
ι' : Sort ?u.185959
ι₂ : Sort ?u.185962
κ : ι → Sort ?u.185967
κ₁ : ι → Sort ?u.185972
κ₂ : ι → Sort ?u.185977
κ' : ι' → Sort ?u.185982
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective (restrictPreimage (U i) f)
x y : α
e : f x = f y
⊢ f x ∈ univ
triv