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

State before:
m n : ℕ
h1 : rel_prime m n
⊢ phi (m * n) = phi m * phi n
Tactic:
have h2 : numElts (Set_rp_below m) (phi m) := phi_is_numElts m
State after:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
⊢ phi (m * n) = phi m * phi n

State before:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
⊢ phi (m * n) = phi m * phi n
Tactic:
have h3 : numElts (Set_rp_below n) (phi n) := phi_is_numElts n
State after:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
⊢ phi (m * n) = phi m * phi n

State before:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
⊢ phi (m * n) = phi m * phi n
Tactic:
have h4 : numElts (Set_rp_below (m * n)) (phi (m * n)) :=
  phi_is_numElts (m * n)
State after:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
⊢ phi (m * n) = phi m * phi n

State before:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
⊢ phi (m * n) = phi m * phi n
Tactic:
have h5 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi (m * n)) :=
  eq_numElts_of_equinum (Set_rp_below_prod h1) h4
State after:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
h5 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi (m * n))
⊢ phi (m * n) = phi m * phi n

State before:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
h5 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi (m * n))
⊢ phi (m * n) = phi m * phi n
Tactic:
have h6 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi m * phi n) :=
  numElts_prod h2 h3
State after:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
h5 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi (m * n))
h6 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi m * phi n)
⊢ phi (m * n) = phi m * phi n

State before:
m n : ℕ
h1 : rel_prime m n
h2 : numElts (Set_rp_below m) (phi m)
h3 : numElts (Set_rp_below n) (phi n)
h4 : numElts (Set_rp_below (m * n)) (phi (m * n))
h5 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi (m * n))
h6 : numElts (Set_rp_below m ×ₛ Set_rp_below n) (phi m * phi n)
⊢ phi (m * n) = phi m * phi n
Tactic:
show phi (m * n) = phi m * phi n from numElts_unique h5 h6
State after:
no goals