-- Mathlib/Data/Set/Function.lean
theorem MapsTo.restrict_surjective_iff (h : MapsTo f s t) :
    Surjective (MapsTo.restrict _ _ _ h) ↔ SurjOn f s t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : restrict f s t h ⟨a, ha⟩ = ⟨b, hb⟩
⊢ f a = b

Tactic:
simpa [Subtype.ext_iff] using ha'

Result:
no goals

Proof state:
case refine_1.intro.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : restrict f s t h ⟨a, ha⟩ = ⟨b, hb⟩
⊢ b ∈ f '' s

Tactic:
replace ha' : f a = b := by simpa [Subtype.ext_iff] using ha'

Result:
case refine_1.intro.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : f a = b
⊢ b ∈ f '' s

Proof state:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
⊢ b ∈ f '' s

Tactic:
obtain ⟨⟨a, ha⟩, ha'⟩ := h' ⟨b, hb⟩

Result:
case refine_1.intro.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : restrict f s t h ⟨a, ha⟩ = ⟨b, hb⟩
⊢ b ∈ f '' s

Proof state:
case refine_1.intro.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : f a = b
⊢ f a ∈ f '' s

Tactic:
exact mem_image_of_mem f ha

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x✝ : ↑t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ ∃ a_1, restrict f s t h a_1 = ⟨f a, hb⟩

Tactic:
exact ⟨⟨a, ha⟩, rfl⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x✝ : ↑t
b : β
hb : b ∈ t
⊢ ∃ a, restrict f s t h a = ⟨b, hb⟩

Tactic:
obtain ⟨a, ha, rfl⟩ := h' hb

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x✝ : ↑t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ ∃ a_1, restrict f s t h a_1 = ⟨f a, hb⟩

Proof state:
case refine_1.intro.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : f a = b
⊢ b ∈ f '' s

Tactic:
rw [← ha']

Result:
case refine_1.intro.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : f a = b
⊢ f a ∈ f '' s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Surjective (restrict f s t h) ↔ SurjOn f s t

Tactic:
refine ⟨fun h' b hb ↦ ?_, fun h' ⟨b, hb⟩ ↦ ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
⊢ b ∈ f '' s

case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x✝ : ↑t
b : β
hb : b ∈ t
⊢ ∃ a, restrict f s t h a = ⟨b, hb⟩