Theorem: HTPI.Example_3_6_4 (HTPILib/Chap3.lean)

State before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
⊢ ∃ x, x ∈ B ∩ C
Tactic:
obtain (b : U) (h4 : b ∈ A ∩ B) from h1
State after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
⊢ ∃ x, x ∈ B ∩ C

State before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
⊢ ∃ x, x ∈ B ∩ C
Tactic:
obtain (c : U) (h5 : c ∈ A ∩ C) from h2
State after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
c : U
h5 : c ∈ A ∩ C
⊢ ∃ x, x ∈ B ∩ C

State before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
c : U
h5 : c ∈ A ∩ C
⊢ ∃ x, x ∈ B ∩ C
Tactic:
obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),
  y ∈ A → z ∈ A → y = z)  from h3
State after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
c : U
h5 : c ∈ A ∩ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C

State before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
c : U
h5 : c ∈ A ∩ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C
Tactic:
define at h4
State after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∩ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C

State before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∩ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C
Tactic:
define at h5
State after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C

State before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C
Tactic:
have h8 : b = c := h7 b c h4.left h5.left
State after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
h8 : b = c
⊢ ∃ x, x ∈ B ∩ C

State before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
h8 : b = c
⊢ ∃ x, x ∈ B ∩ C
Tactic:
rewrite [h8] at h4
State after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b c : U
h4 : c ∈ A ∧ c ∈ B
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
h8 : b = c
⊢ ∃ x, x ∈ B ∩ C

State before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b c : U
h4 : c ∈ A ∧ c ∈ B
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
h8 : b = c
⊢ ∃ x, x ∈ B ∩ C
Tactic:
show ∃ (x : U), x ∈ B ∩ C from
  Exists.intro c (And.intro h4.right h5.right)
State after:
no goals