Theorem: inter_image_fun_inter_subset (meetings/ex4.lean)

State before:
α β : Type
X Y : Set α
f : α → β
⊢ f '' (X ∩ Y) ⊆ f '' X ∩ f '' Y
Tactic:
simp only [Set.subset_inter_iff, Set.image_subset_iff, Set.subset_def]
State after:
α β : Type
X Y : Set α
f : α → β
⊢ ∀ x ∈ f '' (X ∩ Y), x ∈ f '' X ∩ f '' Y

State before:
α β : Type
X Y : Set α
f : α → β
⊢ ∀ x ∈ f '' (X ∩ Y), x ∈ f '' X ∩ f '' Y
Tactic:
simp [Set.subset_def]
State after:
α β : Type
X Y : Set α
f : α → β
⊢ ∀ (x : β), ∀ x_1 ∈ X, x_1 ∈ Y → f x_1 = x → (∃ x_2 ∈ X, f x_2 = x) ∧ ∃ x_2 ∈ Y, f x_2 = x

State before:
α β : Type
X Y : Set α
f : α → β
⊢ ∀ (x : β), ∀ x_1 ∈ X, x_1 ∈ Y → f x_1 = x → (∃ x_2 ∈ X, f x_2 = x) ∧ ∃ x_2 ∈ Y, f x_2 = x
Tactic:
intros a b bmemX bmemY img
State after:
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ (∃ x ∈ X, f x = a) ∧ ∃ x ∈ Y, f x = a

State before:
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ (∃ x ∈ X, f x = a) ∧ ∃ x ∈ Y, f x = a
Tactic:
constructor
State after:
case left
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ ∃ x ∈ X, f x = a

case right
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ ∃ x ∈ Y, f x = a

State before:
case left
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ ∃ x ∈ X, f x = a
Tactic:
use b
State after:
no goals

State before:
case right
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ ∃ x ∈ Y, f x = a
Tactic:
use b
State after:
no goals