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

State before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
⊢ A ∩ C ⊆ B \ D
Tactic:
define
State after:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
⊢ ∀ ⦃a : U⦄, a ∈ A ∩ C → a ∈ B \ D

State before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
⊢ ∀ ⦃a : U⦄, a ∈ A ∩ C → a ∈ B \ D
Tactic:
fix x : U
State after:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
⊢ x ∈ A ∩ C → x ∈ B \ D

State before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
⊢ x ∈ A ∩ C → x ∈ B \ D
Tactic:
assume h3 : x ∈ A ∩ C
State after:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∩ C
⊢ x ∈ B \ D

State before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∩ C
⊢ x ∈ B \ D
Tactic:
define at h3
State after:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B \ D

State before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B \ D
Tactic:
define
State after:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B ∧ x ∉ D

State before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B ∧ x ∉ D
Tactic:
apply And.intro
State after:
case left
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B

case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∉ D

State before:
case left
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B
Tactic:
show x ∈ B from h1 h3.left
State after:
no goals

State before:
case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∉ D
Tactic:
contradict h2 with h4
State after:
case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
h4 : x ∈ D
⊢ ∃ c, c ∈ C ∩ D

State before:
case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
h4 : x ∈ D
⊢ ∃ c, c ∈ C ∩ D
Tactic:
apply Exists.intro x
State after:
case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
h4 : x ∈ D
⊢ x ∈ C ∩ D

State before:
case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
h4 : x ∈ D
⊢ x ∈ C ∩ D
Tactic:
show x ∈ C ∩ D from And.intro h3.right h4
State after:
no goals