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

State before:
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
⊢ image f (W ∩ X) = image f W ∩ image f X
Tactic:
apply Set.ext
State after:
case h
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
⊢ ∀ (x : B), x ∈ image f (W ∩ X) ↔ x ∈ image f W ∩ image f X

State before:
case h
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
⊢ ∀ (x : B), x ∈ image f (W ∩ X) ↔ x ∈ image f W ∩ image f X
Tactic:
fix y : B
State after:
case h
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f (W ∩ X) ↔ y ∈ image f W ∩ image f X

State before:
case h
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f (W ∩ X) ↔ y ∈ image f W ∩ image f X
Tactic:
apply Iff.intro
State after:
case h.mp
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f (W ∩ X) → y ∈ image f W ∩ image f X

case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f W ∩ image f X → y ∈ image f (W ∩ X)

State before:
case h.mp
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f (W ∩ X) → y ∈ image f W ∩ image f X
Tactic:
assume h2 : y ∈ image f (W ∩ X)
State after:
case h.mp
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f (W ∩ X)
⊢ y ∈ image f W ∩ image f X

State before:
case h.mp
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f (W ∩ X)
⊢ y ∈ image f W ∩ image f X
Tactic:
show y ∈ image f W ∩ image f X from Theorem_5_5_2_1 f W X h2
State after:
no goals

State before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f W ∩ image f X → y ∈ image f (W ∩ X)
Tactic:
assume h2 : y ∈ image f W ∩ image f X
State after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f W ∩ image f X
⊢ y ∈ image f (W ∩ X)

State before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f W ∩ image f X
⊢ y ∈ image f (W ∩ X)
Tactic:
define at h2
State after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f W ∧ y ∈ image f X
⊢ y ∈ image f (W ∩ X)

State before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f W ∧ y ∈ image f X
⊢ y ∈ image f (W ∩ X)
Tactic:
rewrite [image_def, image_def] at h2
State after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
⊢ y ∈ image f (W ∩ X)

State before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
⊢ y ∈ image f (W ∩ X)
Tactic:
obtain (x1 : A) (h3 : x1 ∈ W ∧ f x1 = y) from h2.left
State after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
⊢ y ∈ image f (W ∩ X)

State before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
⊢ y ∈ image f (W ∩ X)
Tactic:
obtain (x2 : A) (h4 : x2 ∈ X ∧ f x2 = y) from h2.right
State after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
⊢ y ∈ image f (W ∩ X)

State before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
⊢ y ∈ image f (W ∩ X)
Tactic:
have h5 : f x2 = y := h4.right
State after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = y
⊢ y ∈ image f (W ∩ X)

State before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = y
⊢ y ∈ image f (W ∩ X)
Tactic:
rewrite [←h3.right] at h5
State after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
⊢ y ∈ image f (W ∩ X)

State before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
⊢ y ∈ image f (W ∩ X)
Tactic:
define at h1
State after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
⊢ y ∈ image f (W ∩ X)

State before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
⊢ y ∈ image f (W ∩ X)
Tactic:
have h6 : x2 = x1 := h1 x2 x1 h5
State after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
h6 : x2 = x1
⊢ y ∈ image f (W ∩ X)

State before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
h6 : x2 = x1
⊢ y ∈ image f (W ∩ X)
Tactic:
rewrite [h6] at h4
State after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x1 ∈ X ∧ f x1 = y
h5 : f x2 = f x1
h6 : x2 = x1
⊢ y ∈ image f (W ∩ X)

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