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

State before:
U : Type
A : Set U
⊢ numElts A 1 ↔ ∃ x, A = {x}
Tactic:
apply Iff.intro
State after:
case mp
U : Type
A : Set U
⊢ numElts A 1 → ∃ x, A = {x}

case mpr
U : Type
A : Set U
⊢ (∃ x, A = {x}) → numElts A 1

State before:
case mp
U : Type
A : Set U
⊢ numElts A 1 → ∃ x, A = {x}
Tactic:
assume h1 : numElts A 1
State after:
case mp
U : Type
A : Set U
h1 : numElts A 1
⊢ ∃ x, A = {x}

State before:
case mp
U : Type
A : Set U
h1 : numElts A 1
⊢ ∃ x, A = {x}
Tactic:
have h2 : 1 > 0 := by decide
State after:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
⊢ ∃ x, A = {x}

State before:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
⊢ ∃ x, A = {x}
Tactic:
obtain (x : U) (h3 : x ∈ A) from nonempty_of_pos_numElts h1 h2
State after:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
⊢ ∃ x, A = {x}

State before:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
⊢ ∃ x, A = {x}
Tactic:
have h4 : numElts (A \ {x}) 0 := remove_one_numElts h1 h3
State after:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
h4 : numElts (A \ {x}) 0
⊢ ∃ x, A = {x}

State before:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
h4 : numElts (A \ {x}) 0
⊢ ∃ x, A = {x}
Tactic:
rewrite [zero_elts_iff_empty] at h4
State after:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
h4 : empty (A \ {x})
⊢ ∃ x, A = {x}

State before:
case mp
U : Type
A : Set U
h1 : numElts A 1
h2 : 1 > 0
x : U
h3 : x ∈ A
h4 : empty (A \ {x})
⊢ ∃ x, A = {x}
Tactic:
show ∃ (x : U), A = {x} from
  Exists.intro x (singleton_of_diff_empty h3 h4)
State after:
no goals

State before:
U : Type
A : Set U
h1 : numElts A 1
⊢ 1 > 0
Tactic:
decide
State after:
no goals

State before:
case mpr
U : Type
A : Set U
⊢ (∃ x, A = {x}) → numElts A 1
Tactic:
assume h1 : ∃ (x : U), A = {x}
State after:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
⊢ numElts A 1

State before:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
⊢ numElts A 1
Tactic:
obtain (x : U) (h2 : A = {x}) from h1
State after:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
x : U
h2 : A = {x}
⊢ numElts A 1

State before:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
x : U
h2 : A = {x}
⊢ numElts A 1
Tactic:
rewrite [h2]
State after:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
x : U
h2 : A = {x}
⊢ numElts {x} 1

State before:
case mpr
U : Type
A : Set U
h1 : ∃ x, A = {x}
x : U
h2 : A = {x}
⊢ numElts {x} 1
Tactic:
show numElts {x} 1 from singleton_one_elt x
State after:
no goals