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

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

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

State before:
case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∪ Y ↔ x ∈ Y ∪ X
Tactic:
define : x ∈ X ∪ Y
State after:
case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∪ X

State before:
case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∪ X
Tactic:
define : x ∈ Y ∪ X
State after:
case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X

State before:
case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X
Tactic:
show x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from or_comm
State after:
no goals