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

State before:
U : Type
A : Set U
n : ℕ
a : U
h1 : numElts A (n + 1)
h2 : a ∈ A
⊢ numElts (A \ {a}) n
Tactic:
have h3 : n ∈ I (n + 1) := I_max n
State after:
U : Type
A : Set U
n : ℕ
a : U
h1 : numElts A (n + 1)
h2 : a ∈ A
h3 : n ∈ I (n + 1)
⊢ numElts (A \ {a}) n

State before:
U : Type
A : Set U
n : ℕ
a : U
h1 : numElts A (n + 1)
h2 : a ∈ A
h3 : n ∈ I (n + 1)
⊢ numElts (A \ {a}) n
Tactic:
rewrite [numElts_def] at h1
State after:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
⊢ numElts (A \ {a}) n

State before:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
⊢ numElts (A \ {a}) n
Tactic:
have h4 : I (n + 1) \ {n} ∼ A \ {a} := remove_one_equinum h1 h3 h2
State after:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
h4 : I (n + 1) \ {n} ∼ A \ {a}
⊢ numElts (A \ {a}) n

State before:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
h4 : I (n + 1) \ {n} ∼ A \ {a}
⊢ numElts (A \ {a}) n
Tactic:
rewrite [I_diff] at h4
State after:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
h4 : I n ∼ A \ {a}
⊢ numElts (A \ {a}) n

State before:
U : Type
A : Set U
n : ℕ
a : U
h1 : I (n + 1) ∼ A
h2 : a ∈ A
h3 : n ∈ I (n + 1)
h4 : I n ∼ A \ {a}
⊢ numElts (A \ {a}) n
Tactic:
show numElts (A \ {a}) n from h4
State after:
no goals