Theorem: exercise3_8 (LeanCourse/Assignments/Solutions/Solutions3.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' s ∩ t = f '' (s ∩ f ⁻¹' t)
Tactic:
ext y
State after:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)

State before:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)
Tactic:
constructor
State after:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t)

case h.mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t

State before:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t)
Tactic:
rintro ⟨⟨x, xs, rfl⟩, fxv⟩
State after:
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
xs : x ∈ s
fxv : f x ∈ t
⊢ f x ∈ f '' (s ∩ f ⁻¹' t)

State before:
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
xs : x ∈ s
fxv : f x ∈ t
⊢ f x ∈ f '' (s ∩ f ⁻¹' t)
Tactic:
use x, ⟨xs, fxv⟩
State after:
no goals

State before:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t
Tactic:
rintro ⟨x, ⟨⟨xs, fxv⟩, rfl⟩⟩
State after:
case h.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
xs : x ∈ s
fxv : x ∈ f ⁻¹' t
⊢ f x ∈ f '' s ∩ t

State before:
case h.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
xs : x ∈ s
fxv : x ∈ f ⁻¹' t
⊢ f x ∈ f '' s ∩ t
Tactic:
exact ⟨⟨x, xs, rfl⟩, fxv⟩
State after:
no goals