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

State before:
U : Type
⊢ ∃! A, ∀ (B : Set U), A ∪ B = B
Tactic:
exists_unique
State after:
case Existence
U : Type
⊢ ∃ A, ∀ (B : Set U), A ∪ B = B

case Uniqueness
U : Type
⊢ ∀ (A_1 A_2 : Set U), (∀ (B : Set U), A_1 ∪ B = B) → (∀ (B : Set U), A_2 ∪ B = B) → A_1 = A_2

State before:
case Existence
U : Type
⊢ ∃ A, ∀ (B : Set U), A ∪ B = B
Tactic:
apply Exists.intro ∅
State after:
case Existence
U : Type
⊢ ∀ (B : Set U), ∅ ∪ B = B

State before:
case Existence
U : Type
⊢ ∀ (B : Set U), ∅ ∪ B = B
Tactic:
show ∀ (B : Set U), ∅ ∪ B = B from empty_union
State after:
no goals

State before:
case Uniqueness
U : Type
⊢ ∀ (A_1 A_2 : Set U), (∀ (B : Set U), A_1 ∪ B = B) → (∀ (B : Set U), A_2 ∪ B = B) → A_1 = A_2
Tactic:
fix C : Set U
State after:
case Uniqueness
U : Type
C : Set U
⊢ ∀ (A_2 : Set U), (∀ (B : Set U), C ∪ B = B) → (∀ (B : Set U), A_2 ∪ B = B) → C = A_2

State before:
case Uniqueness
U : Type
C : Set U
⊢ ∀ (A_2 : Set U), (∀ (B : Set U), C ∪ B = B) → (∀ (B : Set U), A_2 ∪ B = B) → C = A_2
Tactic:
fix D : Set U
State after:
case Uniqueness
U : Type
C D : Set U
⊢ (∀ (B : Set U), C ∪ B = B) → (∀ (B : Set U), D ∪ B = B) → C = D

State before:
case Uniqueness
U : Type
C D : Set U
⊢ (∀ (B : Set U), C ∪ B = B) → (∀ (B : Set U), D ∪ B = B) → C = D
Tactic:
assume h1 : ∀ (B : Set U), C ∪ B = B
State after:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
⊢ (∀ (B : Set U), D ∪ B = B) → C = D

State before:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
⊢ (∀ (B : Set U), D ∪ B = B) → C = D
Tactic:
assume h2 : ∀ (B : Set U), D ∪ B = B
State after:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
⊢ C = D

State before:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
⊢ C = D
Tactic:
have h3 : C ∪ D = D := h1 D
State after:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
h3 : C ∪ D = D
⊢ C = D

State before:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
h3 : C ∪ D = D
⊢ C = D
Tactic:
have h4 : D ∪ C = C := h2 C
State after:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
h3 : C ∪ D = D
h4 : D ∪ C = C
⊢ C = D

State before:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
h3 : C ∪ D = D
h4 : D ∪ C = C
⊢ C = D
Tactic:
show C = D from
  calc C
    _ = D ∪ C := h4.symm
    _ = C ∪ D := union_comm D C
    _ = D := h3
State after:
no goals