α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
⊢ (f '' ⋂ (i : ι), s i) = ⋂ (i : ι), f '' s i
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
⊢ (f '' ⋂ (i : ι), s i) = ⋂ (i : ι), f '' s i
inhabit ι
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
hy : y ∈ ⋂ (i : ι), f '' s i
⊢ y ∈ f '' ⋂ (i : ι), s i
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
⊢ (f '' ⋂ (i : ι), s i) = ⋂ (i : ι), f '' s i
refine' Subset.antisymm (image_iInter_subset s f) fun y hy => _
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
hy : ∀ (i : ι), ∃ x x_1, f x = y
⊢ y ∈ f '' ⋂ (i : ι), s i
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
hy : y ∈ ⋂ (i : ι), f '' s i
⊢ y ∈ f '' ⋂ (i : ι), s i
simp only [mem_iInter, mem_image_iff_bex] at hy
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
⊢ y ∈ f '' ⋂ (i : ι), s i
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
hy : ∀ (i : ι), ∃ x x_1, f x = y
⊢ y ∈ f '' ⋂ (i : ι), s i
choose x hx hy using hy
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
⊢ x default ∈ s i
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
⊢ y ∈ f '' ⋂ (i : ι), s i
refine' ⟨x default, mem_iInter.2 fun i => _, hy _⟩
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
⊢ x default = x i
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
⊢ x default ∈ s i
suffices x default = x i by
  rw [this]
  apply hx
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hy : ∀ (i : ι), f (x i) = y
i : ι
hx : ∀ (i : ι), x i ∈ ⋃ (j : ι), s j
⊢ x default = x i
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
⊢ x default = x i
replace hx : ∀ i, x i ∈ ⋃ j, s j := fun i => (subset_iUnion _ _) (hx i)
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hy : ∀ (i : ι), f (x i) = y
i : ι
hx : ∀ (i : ι), x i ∈ ⋃ (j : ι), s j
⊢ f (x default) = f (x i)
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hy : ∀ (i : ι), f (x i) = y
i : ι
hx : ∀ (i : ι), x i ∈ ⋃ (j : ι), s j
⊢ x default = x i
apply h (hx _) (hx _)
no goals
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hy : ∀ (i : ι), f (x i) = y
i : ι
hx : ∀ (i : ι), x i ∈ ⋃ (j : ι), s j
⊢ f (x default) = f (x i)
simp only [hy]
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x i ∈ s i
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x default ∈ s i
rw [this]
no goals
α : Type u_2
β : Type u_3
γ : Type ?u.187674
ι : Sort u_1
ι' : Sort ?u.187680
ι₂ : Sort ?u.187683
κ : ι → Sort ?u.187688
κ₁ : ι → Sort ?u.187693
κ₂ : ι → Sort ?u.187698
κ' : ι' → Sort ?u.187703
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x i ∈ s i
apply hx