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

State before:
U : Type
B : Set U
⊢ ∅ ∪ B = B
Tactic:
apply Set.ext
State after:
case h
U : Type
B : Set U
⊢ ∀ (x : U), x ∈ ∅ ∪ B ↔ x ∈ B

State before:
case h
U : Type
B : Set U
⊢ ∀ (x : U), x ∈ ∅ ∪ B ↔ x ∈ B
Tactic:
fix x : U
State after:
case h
U : Type
B : Set U
x : U
⊢ x ∈ ∅ ∪ B ↔ x ∈ B

State before:
case h
U : Type
B : Set U
x : U
⊢ x ∈ ∅ ∪ B ↔ x ∈ B
Tactic:
apply Iff.intro
State after:
case h.mp
U : Type
B : Set U
x : U
⊢ x ∈ ∅ ∪ B → x ∈ B

case h.mpr
U : Type
B : Set U
x : U
⊢ x ∈ B → x ∈ ∅ ∪ B

State before:
case h.mp
U : Type
B : Set U
x : U
⊢ x ∈ ∅ ∪ B → x ∈ B
Tactic:
assume h1 : x ∈ ∅ ∪ B
State after:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∪ B
⊢ x ∈ B

State before:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∪ B
⊢ x ∈ B
Tactic:
define at h1
State after:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
⊢ x ∈ B

State before:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
⊢ x ∈ B
Tactic:
have h2 : x ∉ ∅ := by
  by_contra h3
  define at h3  show False from h3
  done
State after:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h2 : x ∉ ∅
⊢ x ∈ B

State before:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h2 : x ∉ ∅
⊢ x ∈ B
Tactic:
disj_syll h1 h2
State after:
case h.mp
U : Type
B : Set U
x : U
h2 : x ∉ ∅
h1 : x ∈ B
⊢ x ∈ B

State before:
case h.mp
U : Type
B : Set U
x : U
h2 : x ∉ ∅
h1 : x ∈ B
⊢ x ∈ B
Tactic:
show x ∈ B from h1
State after:
no goals

State before:
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
⊢ x ∉ ∅
Tactic:
by_contra h3
State after:
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h3 : x ∈ ∅
⊢ False

State before:
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h3 : x ∈ ∅
⊢ False
Tactic:
define at h3
State after:
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h3 : False
⊢ False

State before:
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h3 : False
⊢ False
Tactic:
show False from h3
State after:
no goals

State before:
case h.mpr
U : Type
B : Set U
x : U
⊢ x ∈ B → x ∈ ∅ ∪ B
Tactic:
assume h1 : x ∈ B
State after:
case h.mpr
U : Type
B : Set U
x : U
h1 : x ∈ B
⊢ x ∈ ∅ ∪ B

State before:
case h.mpr
U : Type
B : Set U
x : U
h1 : x ∈ B
⊢ x ∈ ∅ ∪ B
Tactic:
show x ∈ ∅ ∪ B from Or.inr h1
State after:
no goals