Theorem: HTPI.Theorem_5_5_2_1 (HTPILib/Chap5.lean)

State before:
A B : Type
f : A → B
W X : Set A
⊢ image f (W ∩ X) ⊆ image f W ∩ image f X
Tactic:
fix y : B
State after:
A B : Type
f : A → B
W X : Set A
y : B
⊢ y ∈ image f (W ∩ X) → y ∈ image f W ∩ image f X

State before:
A B : Type
f : A → B
W X : Set A
y : B
⊢ y ∈ image f (W ∩ X) → y ∈ image f W ∩ image f X
Tactic:
assume h1 : y ∈ image f (W ∩ X)
State after:
A B : Type
f : A → B
W X : Set A
y : B
h1 : y ∈ image f (W ∩ X)
⊢ y ∈ image f W ∩ image f X

State before:
A B : Type
f : A → B
W X : Set A
y : B
h1 : y ∈ image f (W ∩ X)
⊢ y ∈ image f W ∩ image f X
Tactic:
define at h1
State after:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
⊢ y ∈ image f W ∩ image f X

State before:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
⊢ y ∈ image f W ∩ image f X
Tactic:
obtain (x : A) (h2 : x ∈ W ∩ X ∧ f x = y) from h1
State after:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : x ∈ W ∩ X ∧ f x = y
⊢ y ∈ image f W ∩ image f X

State before:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : x ∈ W ∩ X ∧ f x = y
⊢ y ∈ image f W ∩ image f X
Tactic:
define : x ∈ W ∩ X at h2
State after:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f W ∩ image f X

State before:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f W ∩ image f X
Tactic:
apply And.intro
State after:
case left
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f W

case right
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f X

State before:
case left
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f W
Tactic:
define
State after:
case left
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ ∃ x ∈ W, f x = y

State before:
case left
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ ∃ x ∈ W, f x = y
Tactic:
show ∃ (x : A), x ∈ W ∧ f x = y from
  Exists.intro x (And.intro h2.left.left h2.right)
State after:
no goals

State before:
case right
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f X
Tactic:
show y ∈ image f X from
  Exists.intro x (And.intro h2.left.right h2.right)
State after:
no goals