α : Type u_1
β : Type u_3
γ : Type ?u.191837
ι : Sort u_2
ι' : Sort ?u.191843
ι₂ : Sort ?u.191846
κ : ι → Sort ?u.191851
κ₁ : ι → Sort ?u.191856
κ₂ : ι → Sort ?u.191861
κ' : ι' → Sort ?u.191866
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx : x ∈ ⋃ (i : ι), s i
y : α
hy : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
⊢ x = y
α : Type u_1
β : Type u_3
γ : Type ?u.191837
ι : Sort u_2
ι' : Sort ?u.191843
ι₂ : Sort ?u.191846
κ : ι → Sort ?u.191851
κ₁ : ι → Sort ?u.191856
κ₂ : ι → Sort ?u.191861
κ' : ι' → Sort ?u.191866
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
⊢ InjOn f (⋃ (i : ι), s i)
intro x hx y hy hxy
case intro
α : Type u_1
β : Type u_3
γ : Type ?u.191837
ι : Sort u_2
ι' : Sort ?u.191843
ι₂ : Sort ?u.191846
κ : ι → Sort ?u.191851
κ₁ : ι → Sort ?u.191856
κ₂ : ι → Sort ?u.191861
κ' : ι' → Sort ?u.191866
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ (i : ι), s i
y : α
hy : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
i : ι
hx : x ∈ s i
⊢ x = y
α : Type u_1
β : Type u_3
γ : Type ?u.191837
ι : Sort u_2
ι' : Sort ?u.191843
ι₂ : Sort ?u.191846
κ : ι → Sort ?u.191851
κ₁ : ι → Sort ?u.191856
κ₂ : ι → Sort ?u.191861
κ' : ι' → Sort ?u.191866
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx : x ∈ ⋃ (i : ι), s i
y : α
hy : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
⊢ x = y
rcases mem_iUnion.1 hx with ⟨i, hx⟩
case intro.intro
α : Type u_1
β : Type u_3
γ : Type ?u.191837
ι : Sort u_2
ι' : Sort ?u.191843
ι₂ : Sort ?u.191846
κ : ι → Sort ?u.191851
κ₁ : ι → Sort ?u.191856
κ₂ : ι → Sort ?u.191861
κ' : ι' → Sort ?u.191866
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ (i : ι), s i
y : α
hy✝ : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ x = y
case intro
α : Type u_1
β : Type u_3
γ : Type ?u.191837
ι : Sort u_2
ι' : Sort ?u.191843
ι₂ : Sort ?u.191846
κ : ι → Sort ?u.191851
κ₁ : ι → Sort ?u.191856
κ₂ : ι → Sort ?u.191861
κ' : ι' → Sort ?u.191866
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ (i : ι), s i
y : α
hy : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
i : ι
hx : x ∈ s i
⊢ x = y
rcases mem_iUnion.1 hy with ⟨j, hy⟩
case intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type ?u.191837
ι : Sort u_2
ι' : Sort ?u.191843
ι₂ : Sort ?u.191846
κ : ι → Sort ?u.191851
κ₁ : ι → Sort ?u.191856
κ₂ : ι → Sort ?u.191861
κ' : ι' → Sort ?u.191866
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ (i : ι), s i
y : α
hy✝ : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hi : s i ⊆ s k
hj : s j ⊆ s k
⊢ x = y
case intro.intro
α : Type u_1
β : Type u_3
γ : Type ?u.191837
ι : Sort u_2
ι' : Sort ?u.191843
ι₂ : Sort ?u.191846
κ : ι → Sort ?u.191851
κ₁ : ι → Sort ?u.191856
κ₂ : ι → Sort ?u.191861
κ' : ι' → Sort ?u.191866
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ (i : ι), s i
y : α
hy✝ : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ x = y
rcases hs i j with ⟨k, hi, hj⟩
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type ?u.191837
ι : Sort u_2
ι' : Sort ?u.191843
ι₂ : Sort ?u.191846
κ : ι → Sort ?u.191851
κ₁ : ι → Sort ?u.191856
κ₂ : ι → Sort ?u.191861
κ' : ι' → Sort ?u.191866
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ (i : ι), s i
y : α
hy✝ : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hi : s i ⊆ s k
hj : s j ⊆ s k
⊢ x = y
exact hf k (hi hx) (hj hy) hxy