Theorem: HTPI.singleton_of_diff_empty (HTPILib/Chap8Part1.lean)

State before:
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
⊢ A = {a}
Tactic:
apply Set.ext
State after:
case h
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
⊢ ∀ (x : U), x ∈ A ↔ x ∈ {a}

State before:
case h
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
⊢ ∀ (x : U), x ∈ A ↔ x ∈ {a}
Tactic:
fix x : U
State after:
case h
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ A ↔ x ∈ {a}

State before:
case h
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ A ↔ x ∈ {a}
Tactic:
apply Iff.intro
State after:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ A → x ∈ {a}

case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ {a} → x ∈ A

State before:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ A → x ∈ {a}
Tactic:
assume h3 : x ∈ A
State after:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
⊢ x ∈ {a}

State before:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
⊢ x ∈ {a}
Tactic:
contradict h2 with h4
State after:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ ∃ x, x ∈ A \ {a}

State before:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ ∃ x, x ∈ A \ {a}
Tactic:
apply Exists.intro x
State after:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ x ∈ A \ {a}

State before:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ x ∈ A \ {a}
Tactic:
define
State after:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ x ∈ A ∧ x ∉ {a}

State before:
case h.mp
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ A
h4 : ¬x ∈ {a}
⊢ x ∈ A ∧ x ∉ {a}
Tactic:
show x ∈ A ∧ ¬x ∈ {a} from And.intro h3 h4
State after:
no goals

State before:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
⊢ x ∈ {a} → x ∈ A
Tactic:
assume h3 : x ∈ {a}
State after:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ {a}
⊢ x ∈ A

State before:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x ∈ {a}
⊢ x ∈ A
Tactic:
define at h3
State after:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x = a
⊢ x ∈ A

State before:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x = a
⊢ x ∈ A
Tactic:
rewrite [h3]
State after:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x = a
⊢ a ∈ A

State before:
case h.mpr
U : Type
A : Set U
a : U
h1 : a ∈ A
h2 : empty (A \ {a})
x : U
h3 : x = a
⊢ a ∈ A
Tactic:
show a ∈ A from h1
State after:
no goals