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

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

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

State before:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
⊢ numElts (A ×ₛ B) (m * n)
Tactic:
rewrite [numElts_def]
State after:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
⊢ I (m * n) ∼ A ×ₛ B

State before:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
⊢ I (m * n) ∼ A ×ₛ B
Tactic:
have h3 : I m ×ₛ I n ∼ A ×ₛ B := Theorem_8_1_2_1 h1 h2
State after:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
h3 : I m ×ₛ I n ∼ A ×ₛ B
⊢ I (m * n) ∼ A ×ₛ B

State before:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
h3 : I m ×ₛ I n ∼ A ×ₛ B
⊢ I (m * n) ∼ A ×ₛ B
Tactic:
have h4 : I (m * n) ∼ I m ×ₛ I n := I_prod m n
State after:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
h3 : I m ×ₛ I n ∼ A ×ₛ B
h4 : I (m * n) ∼ I m ×ₛ I n
⊢ I (m * n) ∼ A ×ₛ B

State before:
U V : Type
A : Set U
B : Set V
m n : ℕ
h1 : I m ∼ A
h2 : I n ∼ B
h3 : I m ×ₛ I n ∼ A ×ₛ B
h4 : I (m * n) ∼ I m ×ₛ I n
⊢ I (m * n) ∼ A ×ₛ B
Tactic:
show I (m * n) ∼ A ×ₛ B from Theorem_8_1_3_3 h4 h3
State after:
no goals