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

State before:
U : Type
u : U
⊢ numElts {u} 1
Tactic:
define
State after:
U : Type
u : U
⊢ ∃ R, matching R (I 1) {u}

State before:
U : Type
u : U
⊢ ∃ R, matching R (I 1) {u}
Tactic:
rewrite [I_1_singleton]
State after:
U : Type
u : U
⊢ ∃ R, matching R {0} {u}

State before:
U : Type
u : U
⊢ ∃ R, matching R {0} {u}
Tactic:
show ∃ (R : Rel Nat U), matching R {0} {u} from
  Exists.intro (one_match 0 u) (one_match_match 0 u)
State after:
no goals