-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem lcm_apply_mul_gcd_apply [CommMonoidWithZero R] {f : ArithmeticFunction R}
    (hf : f.IsMultiplicative) {x y : ℕ} :
    f (x.lcm y) * f (x.gcd y) = f x * f y

Proof state:
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 : ℕ}, f (i ^ 0) = 1
⊢ (x.gcd y).factorization.support ⊆ x.primeFactors ⊔ y.primeFactors

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

Result:
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 : ℕ}, f (i ^ 0) = 1
⊢ x.factorization.support ∩ y.factorization.support ⊆ x.primeFactors ∪ y.primeFactors

Proof state:
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 : ℕ}, f (i ^ 0) = 1
⊢ (x.lcm y).factorization.support ⊆ x.primeFactors ⊔ y.primeFactors

Tactic:
simp [factorization_lcm hx hy]

Result:
no goals

Proof state:
case neg
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
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

Tactic:
have hfi_zero : ∀ {i}, f (i ^ 0) = 1 := by
  intro i; rw [Nat.pow_zero, hf.1]

Result:
case neg
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 : ℕ}, f (i ^ 0) = 1
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

Proof state:
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
⊢ ∀ {i : ℕ}, f (i ^ 0) = 1

Tactic:
intro i

Result:
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
i : ℕ
⊢ f (i ^ 0) = 1

Proof state:
case neg
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
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

Tactic:
have hlcm_ne_zero : x.lcm y ≠ 0 := lcm_ne_zero hx hy

Result:
case neg
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
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

Proof state:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : y = 0
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

Tactic:
simp only [hy, f.map_zero, mul_zero, Nat.lcm_zero_right, Nat.gcd_zero_right, zero_mul]

Result:
no goals

Proof state:
case neg
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 : ℕ}, f (i ^ 0) = 1
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

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

Result:
case neg
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 : ℕ}, f (i ^ 0) = 1
⊢ (∏ x_1 ∈ x.primeFactors ⊔ y.primeFactors, f (x_1 ^ (x.lcm y).factorization x_1)) *
      ∏ x_1 ∈ x.primeFactors ⊔ y.primeFactors, f (x_1 ^ (x.gcd y).factorization x_1) =
    (∏ x_1 ∈ x.primeFactors ⊔ y.primeFactors, f (x_1 ^ x.factorization x_1)) *
      ∏ x ∈ x.primeFactors ⊔ y.primeFactors, f (x ^ y.factorization x)

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 : ℕ}, f (i ^ 0) = 1
⊢ y.factorization.support ⊆ x.primeFactors ⊔ y.primeFactors

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 : ℕ}, f (i ^ 0) = 1
⊢ x.factorization.support ⊆ x.primeFactors ⊔ y.primeFactors

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 : ℕ}, f (i ^ 0) = 1
⊢ (x.gcd y).factorization.support ⊆ x.primeFactors ⊔ y.primeFactors

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 : ℕ}, f (i ^ 0) = 1
⊢ (x.lcm y).factorization.support ⊆ x.primeFactors ⊔ y.primeFactors

Proof state:
case neg
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 : ℕ}, f (i ^ 0) = 1
p : ℕ
a✝ : p ∈ x.primeFactors ⊔ y.primeFactors
⊢ f (p ^ (x.lcm y).factorization p) * f (p ^ (x.gcd y).factorization p) =
    f (p ^ x.factorization p) * f (p ^ y.factorization p)

Tactic:
rcases Nat.le_or_le (x.factorization p) (y.factorization p) with h | h <;>
  simp only [factorization_lcm hx hy, Finsupp.sup_apply, h, sup_of_le_right,
    sup_of_le_left, inf_of_le_right, Nat.factorization_gcd hx hy, Finsupp.inf_apply,
    inf_of_le_left, mul_comm]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

Tactic:
by_cases hy : y = 0

Result:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : y = 0
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

Proof state:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : x = 0
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

Tactic:
simp only [hx, f.map_zero, zero_mul, Nat.lcm_zero_left, Nat.gcd_zero_left]

Result:
no goals

Proof state:
case neg
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 : ℕ}, f (i ^ 0) = 1
⊢ ∏ x_1 ∈ x.primeFactors ⊔ y.primeFactors,
      f (x_1 ^ (x.lcm y).factorization x_1) * f (x_1 ^ (x.gcd y).factorization x_1) =
    ∏ x_1 ∈ x.primeFactors ⊔ y.primeFactors, f (x_1 ^ x.factorization x_1) * f (x_1 ^ y.factorization x_1)

Tactic:
apply Finset.prod_congr rfl

Result:
case neg
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 : ℕ}, f (i ^ 0) = 1
⊢ ∀ x_1 ∈ x.primeFactors ⊔ y.primeFactors,
    f (x_1 ^ (x.lcm y).factorization x_1) * f (x_1 ^ (x.gcd y).factorization x_1) =
      f (x_1 ^ x.factorization x_1) * f (x_1 ^ y.factorization x_1)