α : Type u_1
β : Type u_3
γ : Type ?u.188767
ι : Sort u_2
ι' : Sort ?u.188773
ι₂ : Sort ?u.188776
κ : ι → Sort ?u.188781
κ₁ : ι → Sort ?u.188786
κ₂ : ι → Sort ?u.188791
κ' : ι' → Sort ?u.188796
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ (i : ι) (hi : p i), s i hi)
⊢ (f '' ⨅ (x : { i // p i }), s ↑x (_ : p ↑x)) = ⨅ (x : { i // p i }), f '' s ↑x (_ : p ↑x)
α : Type u_1
β : Type u_3
γ : Type ?u.188767
ι : Sort u_2
ι' : Sort ?u.188773
ι₂ : Sort ?u.188776
κ : ι → Sort ?u.188781
κ₁ : ι → Sort ?u.188786
κ₂ : ι → Sort ?u.188791
κ' : ι' → Sort ?u.188796
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ (i : ι) (hi : p i), s i hi)
⊢ (f '' ⋂ (i : ι) (hi : p i), s i hi) = ⋂ (i : ι) (hi : p i), f '' s i hi
simp only [iInter, iInf_subtype']
α : Type u_1
β : Type u_3
γ : Type ?u.188767
ι : Sort u_2
ι' : Sort ?u.188773
ι₂ : Sort ?u.188776
κ : ι → Sort ?u.188781
κ₁ : ι → Sort ?u.188786
κ₂ : ι → Sort ?u.188791
κ' : ι' → Sort ?u.188796
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ (i : ι) (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ (f '' ⨅ (x : { i // p i }), s ↑x (_ : p ↑x)) = ⨅ (x : { i // p i }), f '' s ↑x (_ : p ↑x)
α : Type u_1
β : Type u_3
γ : Type ?u.188767
ι : Sort u_2
ι' : Sort ?u.188773
ι₂ : Sort ?u.188776
κ : ι → Sort ?u.188781
κ₁ : ι → Sort ?u.188786
κ₂ : ι → Sort ?u.188791
κ' : ι' → Sort ?u.188796
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ (i : ι) (hi : p i), s i hi)
⊢ (f '' ⨅ (x : { i // p i }), s ↑x (_ : p ↑x)) = ⨅ (x : { i // p i }), f '' s ↑x (_ : p ↑x)
haveI : Nonempty { i // p i } := nonempty_subtype.2 hp
case h
α : Type u_1
β : Type u_3
γ : Type ?u.188767
ι : Sort u_2
ι' : Sort ?u.188773
ι₂ : Sort ?u.188776
κ : ι → Sort ?u.188781
κ₁ : ι → Sort ?u.188786
κ₂ : ι → Sort ?u.188791
κ' : ι' → Sort ?u.188796
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ (i : ι) (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ InjOn f (⋃ (i : { i // p i }), s ↑i (_ : p ↑i))
α : Type u_1
β : Type u_3
γ : Type ?u.188767
ι : Sort u_2
ι' : Sort ?u.188773
ι₂ : Sort ?u.188776
κ : ι → Sort ?u.188781
κ₁ : ι → Sort ?u.188786
κ₂ : ι → Sort ?u.188791
κ' : ι' → Sort ?u.188796
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ (i : ι) (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ (f '' ⨅ (x : { i // p i }), s ↑x (_ : p ↑x)) = ⨅ (x : { i // p i }), f '' s ↑x (_ : p ↑x)
apply InjOn.image_iInter_eq
no goals
case h
α : Type u_1
β : Type u_3
γ : Type ?u.188767
ι : Sort u_2
ι' : Sort ?u.188773
ι₂ : Sort ?u.188776
κ : ι → Sort ?u.188781
κ₁ : ι → Sort ?u.188786
κ₂ : ι → Sort ?u.188791
κ' : ι' → Sort ?u.188796
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ (i : ι) (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ InjOn f (⋃ (i : { i // p i }), s ↑i (_ : p ↑i))
simpa only [iUnion, iSup_subtype'] using h