no goals
α : Type u_1
β : Type u_2
γ : Type ?u.38868
ι : Sort ?u.38871
π : α → Type ?u.38876
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g✝ g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
x✝ : ∃ t' g, t ⊆ t' ∧ Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)
y : β
hy : y ∈ t
t' : Set β
g : ↑s → ↑t'
htt' : t ⊆ t'
hg : Surjective g
hfg : ∀ (x : ↑s), f ↑x = ↑(g x)
x : ↑s
hx : g x = { val := y, property := (_ : y ∈ t') }
⊢ f ↑x = y
rw [hfg, hx, Subtype.coe_mk]