-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem mul [CommSemiring R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative)
    (hg : g.IsMultiplicative) : IsMultiplicative (f * g)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 = 0
hb : ¬((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 = 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ¬((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 = 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ¬((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ (b1 * b2).gcd (a1 * b1) = d1

Tactic:
rw [← hcd.2.1, h.1, mul_comm c1 d1, Nat.gcd_mul_left,
  cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one, mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 = 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ¬((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 = 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ¬((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 = 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ¬((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b1 = (b1 * b2).gcd (a1 * b1)

Tactic:
rw [mul_comm, Nat.gcd_mul_right,
  cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one, one_mul]

Result:
no goals

Proof state:
case h.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 = 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ¬((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 = 0
⊢ f a1 * g a2 * (f b1 * g b2) = f (a1 * b1) * g (a2 * b2)

Tactic:
rw [hf.map_mul_of_coprime cop.coprime_mul_right.coprime_mul_right_right,
  hg.map_mul_of_coprime cop.coprime_mul_left.coprime_mul_left_right]

Result:
case h.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 = 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ¬((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 = 0
⊢ f a1 * g a2 * (f b1 * g b2) =
    f ((a1, a2), b1, b2).1.1 * f ((a1, a2), b1, b2).2.1 * (g ((a1, a2), b1, b2).1.2 * g ((a1, a2), b1, b2).2.2)

Proof state:
case hi.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
a1 a2 b1 b2 : ℕ
h : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
⊢ (match ((a1, a2), b1, b2) with
    | ((i, j), k, l) => (i * k, j * l)) ∈
    (m * n).divisorsAntidiagonal

Tactic:
rcases h with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩

Result:
case hi.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ (match ((a1, a2), b1, b2) with
    | ((i, j), k, l) => (i * k, j * l)) ∈
    (a1 * a2 * (b1 * b2)).divisorsAntidiagonal

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ (f * g).IsMultiplicative

Tactic:
refine ⟨by simp [hf.1, hg.1], ?_⟩

Result:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ ∀ {m n : ℕ}, m.Coprime n → (f * g) (m * n) = (f * g) m * (f * g) n

Proof state:
case hi.mk.mk.mk.intro.intro.intro.right
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)

Tactic:
rw [Nat.mul_eq_zero] at *

Result:
case hi.mk.mk.mk.intro.intro.intro.right
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬(a1 = 0 ∨ a2 = 0)
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬(b1 = 0 ∨ b2 = 0)
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2 =
    (∑ x ∈ m.divisorsAntidiagonal, f x.1 * g x.2) * ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2

Tactic:
rw [sum_mul_sum, ← sum_product']

Result:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2 =
    ∑ x ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal, f x.1.1 * g x.1.2 * (f x.2.1 * g x.2.2)

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m = 0 ∧ ¬n = 0
⊢ ((m = m ∧ ¬m = 0) ∧ n = n ∧ ¬n = 0) ∧ (b1.gcd (b1 * b2), b2.gcd (b1 * b2)) = (b1, b2)

Tactic:
simp [h.2.1, h.2.2]

Result:
no goals