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

State before:
U : Type
A B C : Set U
⊢ A \ (B \ C) ⊆ A \ B ∪ C
Tactic:
fix x : U
State after:
U : Type
A B C : Set U
x : U
⊢ x ∈ A \ (B \ C) → x ∈ A \ B ∪ C

State before:
U : Type
A B C : Set U
x : U
⊢ x ∈ A \ (B \ C) → x ∈ A \ B ∪ C
Tactic:
assume h1 : x ∈ A \ (B \ C)
State after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A \ (B \ C)
⊢ x ∈ A \ B ∪ C

State before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A \ (B \ C)
⊢ x ∈ A \ B ∪ C
Tactic:
define
State after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A \ (B \ C)
⊢ x ∈ A \ B ∨ x ∈ C

State before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A \ (B \ C)
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
define at h1
State after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
⊢ x ∈ A \ B ∨ x ∈ C

State before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
have h2 : x ∉ B \ C := h1.right
State after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B \ C
⊢ x ∈ A \ B ∨ x ∈ C

State before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B \ C
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
define at h2
State after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : ¬(x ∈ B ∧ x ∉ C)
⊢ x ∈ A \ B ∨ x ∈ C

State before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : ¬(x ∈ B ∧ x ∉ C)
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
demorgan at h2
State after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B ∨ x ∈ C
⊢ x ∈ A \ B ∨ x ∈ C

State before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B ∨ x ∈ C
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
by_cases on h2
State after:
case Case_1
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B
⊢ x ∈ A \ B ∨ x ∈ C

case Case_2
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∈ C
⊢ x ∈ A \ B ∨ x ∈ C

State before:
case Case_1
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
apply Or.inl
State after:
case Case_1.h
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B
⊢ x ∈ A \ B

State before:
case Case_1.h
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B
⊢ x ∈ A \ B
Tactic:
show x ∈ A \ B from And.intro h1.left h2
State after:
no goals

State before:
case Case_2
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∈ C
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
apply Or.inr
State after:
case Case_2.h
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∈ C
⊢ x ∈ C

State before:
case Case_2.h
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∈ C
⊢ x ∈ C
Tactic:
show x ∈ C from h2
State after:
no goals