awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
neg :
  HMul.hMul (α := R) (β := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
          (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)) :
        R)
      ((f : (a : ℕ) → R) (x.gcd y) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)
rw : (x.lcm y).factorization.support ⊆ x.primeFactors ∪ y.primeFactors
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)

Tactic:
rw [hf.multiplicative_factorization f (by assumption),
    Finsupp.prod_of_support_subset _ _ _ (fun _ _ => hfi_zero)
      (s := (x.primeFactors ∪ y.primeFactors))]

Premises used: ArithmeticFunction.IsMultiplicative.multiplicative_factorization, Finsupp.prod_of_support_subset
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
⊢ x.gcd y ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
neg :
  HMul.hMul (α := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)))
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.gcd y).factorization : (a : ℕ) → ℕ) x_1 : ℕ))) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)
rw : (x.gcd y).factorization.support ⊆ x.primeFactors ∪ y.primeFactors
⊢ HMul.hMul (α := R) (β := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
          (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)) :
        R)
      ((f : (a : ℕ) → R) (x.gcd y) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)

Tactic:
rw [hf.multiplicative_factorization f (by assumption),
    Finsupp.prod_of_support_subset _ _ _ (fun _ _ => hfi_zero)
      (s := (x.primeFactors ∪ y.primeFactors))]

Premises used: ArithmeticFunction.IsMultiplicative.multiplicative_factorization, Finsupp.prod_of_support_subset
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
⊢ x ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
neg :
  HMul.hMul (α := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)))
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.gcd y).factorization : (a : ℕ) → ℕ) x_1 : ℕ))) =
    HMul.hMul (α := R) (β := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
          (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 ((x.factorization : (a : ℕ) → ℕ) x_1 : ℕ)) :
        R)
      ((f : (a : ℕ) → R) y : R)
rw : x.factorization.support ⊆ x.primeFactors ∪ y.primeFactors
⊢ HMul.hMul (α := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)))
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.gcd y).factorization : (a : ℕ) → ℕ) x_1 : ℕ))) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)

Tactic:
rw [hf.multiplicative_factorization f (by assumption),
    Finsupp.prod_of_support_subset _ _ _ (fun _ _ => hfi_zero)
      (s := (x.primeFactors ∪ y.primeFactors))]

Premises used: ArithmeticFunction.IsMultiplicative.multiplicative_factorization, Finsupp.prod_of_support_subset
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
⊢ y ≠ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
neg :
  HMul.hMul (α := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)))
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.gcd y).factorization : (a : ℕ) → ℕ) x_1 : ℕ))) =
    HMul.hMul (α := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 ((x.factorization : (a : ℕ) → ℕ) x_1 : ℕ)))
      (∏ x ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x ((y.factorization : (a : ℕ) → ℕ) x : ℕ)))
rw : y.factorization.support ⊆ x.primeFactors ∪ y.primeFactors
⊢ HMul.hMul (α := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)))
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.gcd y).factorization : (a : ℕ) → ℕ) x_1 : ℕ))) =
    HMul.hMul (α := R) (β := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
          (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 ((x.factorization : (a : ℕ) → ℕ) x_1 : ℕ)) :
        R)
      ((f : (a : ℕ) → R) y : R)

Tactic:
rw [hf.multiplicative_factorization f (by assumption),
    Finsupp.prod_of_support_subset _ _ _ (fun _ _ => hfi_zero)
      (s := (x.primeFactors ∪ y.primeFactors))]

Premises used: ArithmeticFunction.IsMultiplicative.multiplicative_factorization, Finsupp.prod_of_support_subset
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
neg :
  HMul.hMul (α := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)))
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.gcd y).factorization : (a : ℕ) → ℕ) x_1 : ℕ))) =
    HMul.hMul (α := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 ((x.factorization : (a : ℕ) → ℕ) x_1 : ℕ)))
      (∏ x ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x ((y.factorization : (a : ℕ) → ℕ) x : ℕ)))
iterate : y.factorization.support ⊆ x.primeFactors ∪ y.primeFactors
iterate₁ : x.factorization.support ⊆ x.primeFactors ∪ y.primeFactors
iterate₂ : (x.gcd y).factorization.support ⊆ x.primeFactors ∪ y.primeFactors
iterate₃ : (x.lcm y).factorization.support ⊆ x.primeFactors ∪ y.primeFactors
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)

Tactic:
iterate 4 rw [hf.multiplicative_factorization f (by assumption),
    Finsupp.prod_of_support_subset _ _ _ (fun _ _ => hfi_zero)
      (s := (x.primeFactors ∪ y.primeFactors))]

Premises used: ArithmeticFunction.IsMultiplicative.multiplicative_factorization, Finsupp.prod_of_support_subset
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
neg :
  Eq.{u_1 + 1} (α := R)
    (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
      HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.gcd y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R))
    (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
      HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 ((x.factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 ((y.factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R))
⊢ HMul.hMul (α := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)))
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.gcd y).factorization : (a : ℕ) → ℕ) x_1 : ℕ))) =
    HMul.hMul (α := R)
      (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 ((x.factorization : (a : ℕ) → ℕ) x_1 : ℕ)))
      (∏ x ∈ x.primeFactors ∪ y.primeFactors,
        (f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x ((y.factorization : (a : ℕ) → ℕ) x : ℕ)))

Tactic:
rw [← prod_mul_distrib, ← prod_mul_distrib]

Premises used: Finset.prod_mul_distrib
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
neg :
  ∀ x_1 ∈ x.primeFactors ∪ y.primeFactors,
    HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.gcd y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R) =
      HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 ((x.factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 ((y.factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R)
⊢ Eq.{u_1 + 1} (α := R)
    (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
      HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.lcm y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 (((x.gcd y).factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R))
    (∏ x_1 ∈ x.primeFactors ∪ y.primeFactors,
      HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 ((x.factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) x_1 ((y.factorization : (a : ℕ) → ℕ) x_1 : ℕ)) : R))

Tactic:
apply prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
p : ℕ
neg :
  p ∈ x.primeFactors ∪ y.primeFactors →
    HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.lcm y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.gcd y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((y.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
⊢ p ∈ x.primeFactors ∪ y.primeFactors →
    HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.lcm y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.gcd y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((y.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)

Tactic:
_
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
p : ℕ
h : p ∈ x.primeFactors ∪ y.primeFactors
neg :
  ∀ (h : LE.le (α := ℕ) ((x.factorization : (a : ℕ) → ℕ) p : ℕ) ((y.factorization : (a : ℕ) → ℕ) p : ℕ)),
    HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.lcm y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.gcd y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((y.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
neg₁ :
  ∀ (h : LE.le (α := ℕ) ((y.factorization : (a : ℕ) → ℕ) p : ℕ) ((x.factorization : (a : ℕ) → ℕ) p : ℕ)),
    HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.lcm y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.gcd y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
        ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((y.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
⊢ HMul.hMul (α := R) (β := R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.lcm y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.gcd y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((y.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)

Tactic:
rcases Nat.le_or_le (x.factorization p) (y.factorization p) with h | h

Premises used: Nat.le_or_le, DFunLike.coe, Nat.factorization
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
p : ℕ
h_1 : p ∈ x.primeFactors ∪ y.primeFactors
h : LE.le (α := ℕ) ((x.factorization : (a : ℕ) → ℕ) p : ℕ) ((y.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HMul.hMul (α := R) (β := R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.lcm y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.gcd y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((y.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)

Tactic:
simp only [factorization_lcm hx hy, Finsupp.sup_apply, h, sup_of_le_right,
        sup_of_le_left, inf_of_le_right, factorization_gcd hx hy, Finsupp.inf_apply,
        inf_of_le_left, mul_comm]

Premises used: inf_of_le_left, inf_of_le_right, Finsupp.inf_apply, Nat.factorization_lcm, sup_of_le_right, Finsupp.sup_apply, mul_comm, Nat.factorization_gcd, sup_of_le_left
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
p : ℕ
h_1 : p ∈ x.primeFactors ∪ y.primeFactors
h : LE.le (α := ℕ) ((y.factorization : (a : ℕ) → ℕ) p : ℕ) ((x.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HMul.hMul (α := R) (β := R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.lcm y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p (((x.gcd y).factorization : (a : ℕ) → ℕ) p : ℕ)) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((x.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)
      ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) p ((y.factorization : (a : ℕ) → ℕ) p : ℕ)) : R)

Tactic:
simp only [factorization_lcm hx hy, Finsupp.sup_apply, h, sup_of_le_right,
        sup_of_le_left, inf_of_le_right, factorization_gcd hx hy, Finsupp.inf_apply,
        inf_of_le_left, mul_comm]

Premises used: inf_of_le_left, inf_of_le_right, Finsupp.inf_apply, Nat.factorization_lcm, sup_of_le_right, Finsupp.sup_apply, mul_comm, Nat.factorization_gcd, sup_of_le_left
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
⊢ y.factorization.support ⊆ x.primeFactors ∪ y.primeFactors

Tactic:
apply subset_union_right

Premises used: Finset.subset_union_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
⊢ x.factorization.support ⊆ x.primeFactors ∪ y.primeFactors

Tactic:
apply subset_union_left

Premises used: Finset.subset_union_left
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
rw : x.factorization.support ∩ y.factorization.support ⊆ x.primeFactors ∪ y.primeFactors
⊢ (x.gcd y).factorization.support ⊆ x.primeFactors ∪ y.primeFactors

Tactic:
rw [factorization_gcd hx hy, Finsupp.support_inf]

Premises used: Finsupp.support_inf, Nat.factorization_gcd
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
⊢ x.factorization.support ∩ y.factorization.support ⊆ x.primeFactors ∪ y.primeFactors

Tactic:
apply inter_subset_union

Premises used: Finset.inter_subset_union
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
⊢ (x.lcm y).factorization.support ⊆ x.primeFactors ∪ y.primeFactors

Tactic:
simp [factorization_lcm hx hy]

Premises used: Nat.factorization_lcm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_lcm : Ne (α := R) ((f : (a : ℕ) → R) (x.lcm y) : R) (0 : R)
rw :
  (f : (a : ℕ) → R) (x.gcd y) =
    HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R))
      ((f : (a : ℕ) → R) (x.lcm y) : R)
rw₁ rw₂ : Eq (α := R) ((f : (a : ℕ) → R) (x.gcd y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R)
⊢ (f : (a : ℕ) → R) (x.gcd y) =
    HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R))
      ((f : (a : ℕ) → R) (x.lcm y) : R)

Tactic:
rw [← hf.lcm_apply_mul_gcd_apply, mul_div_cancel_left₀ _ hf_lcm]

Premises used: mul_div_cancel_left₀, ArithmeticFunction.IsMultiplicative.lcm_apply_mul_gcd_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_gcd : Ne (α := R) ((f : (a : ℕ) → R) (x.gcd y) : R) (0 : R)
rw :
  (f : (a : ℕ) → R) (x.lcm y) =
    HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R))
      ((f : (a : ℕ) → R) (x.gcd y) : R)
rw₁ rw₂ : Eq (α := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.lcm y) : R)
⊢ (f : (a : ℕ) → R) (x.lcm y) =
    HDiv.hDiv (β := R) (HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R))
      ((f : (a : ℕ) → R) (x.gcd y) : R)

Tactic:
rw [← hf.lcm_apply_mul_gcd_apply, mul_div_cancel_right₀ _ hf_gcd]

Premises used: mul_div_cancel_right₀, ArithmeticFunction.IsMultiplicative.lcm_apply_mul_gcd_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
m n : ℕ
hn : Squarefree n
hmn : m ∣ n
h_zero : Eq (α := R) ((f : (a : ℕ) → R) m : R) (0 : R)
rcases : ∀ (k : ℕ) (hn : Squarefree (m * k)), Eq (α := R) ((f : (a : ℕ) → R) (m * k) : R) (0 : R)
⊢ Eq (α := R) ((f : (a : ℕ) → R) n : R) (0 : R)

Tactic:
rcases hmn with ⟨k, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
m : ℕ
h_zero : Eq (α := R) ((f : (a : ℕ) → R) m : R) (0 : R)
k : ℕ
hn : Squarefree (m * k)
⊢ Eq (α := R) ((f : (a : ℕ) → R) (m * k) : R) (0 : R)

Tactic:
simp only [zero_mul, hf.map_mul_of_coprime (coprime_of_squarefree_mul hn), h_zero]

Premises used: MulZeroClass.zero_mul, ArithmeticFunction.IsMultiplicative.map_mul_of_coprime, Nat.coprime_of_squarefree_mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
⊢ Eq.{u_1 + 1} (α := R) ((1 : (a : ℕ) → R) 1 : R) (1 : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
pos :
  ∀ (h : m = 1),
    (1 : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((1 : (a : ℕ) → R) m : R) ((1 : (a : ℕ) → R) n : R)
neg :
  ∀ (h : ¬m = 1),
    (1 : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((1 : (a : ℕ) → R) m : R) ((1 : (a : ℕ) → R) n : R)
⊢ (1 : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((1 : (a : ℕ) → R) m : R) ((1 : (a : ℕ) → R) n : R)

Tactic:
by_cases h : m = 1
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
hmn : m.Coprime n
h : m = 1
⊢ (1 : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((1 : (a : ℕ) → R) m : R) ((1 : (a : ℕ) → R) n : R)

Tactic:
aesop