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

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

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

State before:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ A
⊢ m = n
Tactic:
have h3 : A ∼ I n := Theorem_8_1_3_2 h2
State after:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ A
h3 : A ∼ I n
⊢ m = n

State before:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ A
h3 : A ∼ I n
⊢ m = n
Tactic:
have h4 : I m ∼ I n := Theorem_8_1_3_3 h1 h3
State after:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ A
h3 : A ∼ I n
h4 : I m ∼ I n
⊢ m = n

State before:
U : Type
A : Set U
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ A
h3 : A ∼ I n
h4 : I m ∼ I n
⊢ m = n
Tactic:
show m = n from eq_of_I_equinum h4
State after:
no goals