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

State before:
U : Type
A B C : Set U
⊢ A ∩ (B \ C) = (A ∩ B) \ C
Tactic:
apply Set.ext
State after:
case h
U : Type
A B C : Set U
⊢ ∀ (x : U), x ∈ A ∩ (B \ C) ↔ x ∈ (A ∩ B) \ C

State before:
case h
U : Type
A B C : Set U
⊢ ∀ (x : U), x ∈ A ∩ (B \ C) ↔ x ∈ (A ∩ B) \ C
Tactic:
fix x : U
State after:
case h
U : Type
A B C : Set U
x : U
⊢ x ∈ A ∩ (B \ C) ↔ x ∈ (A ∩ B) \ C

State before:
case h
U : Type
A B C : Set U
x : U
⊢ x ∈ A ∩ (B \ C) ↔ x ∈ (A ∩ B) \ C
Tactic:
show x ∈ A ∩ (B \ C) ↔ x ∈ (A ∩ B) \ C from
  calc x ∈ A ∩ (B \ C)
    _ ↔ x ∈ A ∧ (x ∈ B ∧ x ∉ C) := Iff.refl _
    _ ↔ (x ∈ A ∧ x ∈ B) ∧ x ∉ C := and_assoc.symm
    _ ↔ x ∈ (A ∩ B) \ C := Iff.refl _
State after:
no goals