case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ ∀ (p n : ℕ), Prime p → 0 < n → f (p ^ n) = Finsupp.prod (factorization (p ^ n)) fun p k => f (p ^ k)

case h0
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f 0 = Finsupp.prod (factorization 0) fun p k => f (p ^ k)

case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f 1 = Finsupp.prod (factorization 1) fun p k => f (p ^ k)

case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        coprime a b →
          (f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)) →
            (f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)) →
              f (a * b) = Finsupp.prod (factorization (a * b)) fun p k => f (p ^ k)
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ ∀ {n : ℕ}, f n = Finsupp.prod (factorization n) fun p k => f (p ^ k)
apply Nat.recOnPosPrimePosCoprime
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ k) = Finsupp.prod (factorization (p ^ k)) fun p k => f (p ^ k)
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ ∀ (p n : ℕ), Prime p → 0 < n → f (p ^ n) = Finsupp.prod (factorization (p ^ n)) fun p k => f (p ^ k)
rintro p k hp -
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ k) = Finsupp.prod (single p k) fun p k => f (p ^ k)
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ k) = Finsupp.prod (factorization (p ^ k)) fun p k => f (p ^ k)
simp only [hp.factorization_pow]
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ 0) = 1
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ k) = Finsupp.prod (single p k) fun p k => f (p ^ k)
rw [prod_single_index _]
no goals
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ 0) = 1
simp [hf1]
no goals
case h0
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f 0 = Finsupp.prod (factorization 0) fun p k => f (p ^ k)
simp [hf0]
case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ 1 = Finsupp.prod 0 fun p k => f (p ^ k)
case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f 1 = Finsupp.prod (factorization 1) fun p k => f (p ^ k)
rw [factorization_one, hf1]
no goals
case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ 1 = Finsupp.prod 0 fun p k => f (p ^ k)
simp
case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : coprime a b
ha : f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)
hb : f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)
⊢ f (a * b) = Finsupp.prod (factorization (a * b)) fun p k => f (p ^ k)
case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        coprime a b →
          (f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)) →
            (f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)) →
              f (a * b) = Finsupp.prod (factorization (a * b)) fun p k => f (p ^ k)
intro a b _ _ hab ha hb
case h.hd
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : coprime a b
ha : f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)
hb : f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)
⊢ _root_.Disjoint (factorization a).support (factorization b).support
case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : coprime a b
ha : f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)
hb : f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)
⊢ f (a * b) = Finsupp.prod (factorization (a * b)) fun p k => f (p ^ k)
rw [h_mult a b hab, ha, hb, factorization_mul_of_coprime hab, ← prod_add_index_of_disjoint]
no goals
case h.hd
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), coprime x y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : coprime a b
ha : f a = Finsupp.prod (factorization a) fun p k => f (p ^ k)
hb : f b = Finsupp.prod (factorization b) fun p k => f (p ^ k)
⊢ _root_.Disjoint (factorization a).support (factorization b).support
exact factorization_disjoint_of_coprime hab