α : Type u_2
β : Type u_1
γ : Type ?u.25203
ι : Sort ?u.25206
π : α → Type ?u.25211
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ range (MapsTo.restrict f (f ⁻¹' t) t (_ : MapsTo f (f ⁻¹' t) t)) = Subtype.val ⁻¹' range f
α : Type u_2
β : Type u_1
γ : Type ?u.25203
ι : Sort ?u.25206
π : α → Type ?u.25211
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ range (restrictPreimage t f) = Subtype.val ⁻¹' range f
delta Set.restrictPreimage
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.25203
ι : Sort ?u.25206
π : α → Type ?u.25211
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
⊢ range (MapsTo.restrict f (f ⁻¹' t) t (_ : MapsTo f (f ⁻¹' t) t)) = Subtype.val ⁻¹' range f
rw [MapsTo.range_restrict, Set.image_preimage_eq_inter_range, Set.preimage_inter,
  Subtype.coe_preimage_self, Set.univ_inter]