Theorem: HTPI.eq_numElts_of_equinum (HTPILib/Chap8Part2.lean)

State before:
U V : Type
A : Set U
B : Set V
n : ℕ
h1 : A ∼ B
h2 : numElts A n
⊢ numElts B n
Tactic:
rewrite [numElts_def] at h2
State after:
U V : Type
A : Set U
B : Set V
n : ℕ
h1 : A ∼ B
h2 : I n ∼ A
⊢ numElts B n

State before:
U V : Type
A : Set U
B : Set V
n : ℕ
h1 : A ∼ B
h2 : I n ∼ A
⊢ numElts B n
Tactic:
rewrite [numElts_def]
State after:
U V : Type
A : Set U
B : Set V
n : ℕ
h1 : A ∼ B
h2 : I n ∼ A
⊢ I n ∼ B

State before:
U V : Type
A : Set U
B : Set V
n : ℕ
h1 : A ∼ B
h2 : I n ∼ A
⊢ I n ∼ B
Tactic:
show I n ∼ B from Theorem_8_1_3_3 h2 h1
State after:
no goals