Theorem: Set.map_subset_map (GMLInit/Data/Set/Subset.lean)

State before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
⊢ s.Subset t → (f <$> s).Subset (f <$> t)
Tactic:
intro hst y ⟨x,hx,h⟩
State after:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ f <$> t

State before:
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ f <$> t
Tactic:
cases h
State after:
case refl
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ f x ∈ f <$> t

State before:
case refl
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ f x ∈ f <$> t
Tactic:
exists x
State after:
case refl
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ x ∈ t ∧ f x = f x

State before:
case refl
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ x ∈ t ∧ f x = f x
Tactic:
constructor
State after:
case refl.left
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ x ∈ t

case refl.right
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ f x = f x

State before:
case refl.left
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ x ∈ t
Tactic:
exact hst x hx
State after:
no goals

State before:
case refl.right
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ f x = f x
Tactic:
rfl
State after:
no goals