-- Mathlib/Data/Nat/Factorization/Induction.lean
theorem multiplicative_factorization {β : Type*} [CommMonoid β] (f : ℕ → β)
    (h_mult : ∀ x y : ℕ, Coprime x y → f (x * y) = f x * f y) (hf : f 1 = 1) :
    ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun p k => f (p ^ k)

Proof state:
case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          (a ≠ 0 → f a = a.factorization.prod fun p k => f (p ^ k)) →
            (b ≠ 0 → f b = b.factorization.prod fun p k => f (p ^ k)) →
              a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun p k => f (p ^ k)

Tactic:
intro a b _ _ hab ha hb hab_pos

Result:
case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k => f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k => f (p ^ k)
hab_pos : a * b ≠ 0
⊢ f (a * b) = (a * b).factorization.prod fun p k => f (p ^ k)

Proof state:
case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k => f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k => f (p ^ k)
hab_pos : a * b ≠ 0
⊢ f (a * b) = (a * b).factorization.prod fun p k => f (p ^ k)

Tactic:
rw [h_mult a b hab, ha (left_ne_zero_of_mul hab_pos), hb (right_ne_zero_of_mul hab_pos),
  factorization_mul_of_coprime hab, ← prod_add_index_of_disjoint]

Result:
case h.hd
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k => f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k => f (p ^ k)
hab_pos : a * b ≠ 0
⊢ _root_.Disjoint a.factorization.support b.factorization.support

Proof state:
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun p k => f (p ^ k)

Tactic:
apply Nat.recOnPosPrimePosCoprime

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

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

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

case h
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          (a ≠ 0 → f a = a.factorization.prod fun p k => f (p ^ k)) →
            (b ≠ 0 → f b = b.factorization.prod fun p k => f (p ^ k)) →
              a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun p k => f (p ^ k)

Proof state:
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ 0) = 1

Tactic:
rwa [pow_zero]

Result:
no goals

Proof state:
case h.hd
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k => f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k => f (p ^ k)
hab_pos : a * b ≠ 0
⊢ _root_.Disjoint a.factorization.support b.factorization.support

Tactic:
exact hab.disjoint_primeFactors

Result:
no goals

Proof state:
case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ f 1 = (factorization 1).prod fun p k => f (p ^ k)

Tactic:
rw [factorization_one, hf]

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

Proof state:
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ (p n : ℕ), Prime p → 0 < n → p ^ n ≠ 0 → f (p ^ n) = (p ^ n).factorization.prod fun p k => f (p ^ k)

Tactic:
rintro p k hp - -

Result:
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ k) = (p ^ k).factorization.prod fun p k => f (p ^ k)

Proof state:
case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 1 ≠ 0 → f 1 = (factorization 1).prod fun p k => f (p ^ k)

Tactic:
rintro -

Result:
case h1
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ f 1 = (factorization 1).prod fun p k => f (p ^ k)

Proof state:
case hp
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ k) = (p ^ k).factorization.prod fun p k => f (p ^ k)

Tactic:
rw [Prime.factorization_pow hp, Finsupp.prod_single_index _]

Result:
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
p k : ℕ
hp : Prime p
⊢ f (p ^ 0) = 1

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

Tactic:
simp

Result:
no goals

Proof state:
case h0
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ 0 ≠ 0 → f 0 = (factorization 0).prod fun p k => f (p ^ k)

Tactic:
simp

Result:
no goals