-- 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
m n : ℕ
cop : m.Coprime n
⊢ ∑ x ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal, f x.1.1 * g x.1.2 * (f x.2.1 * g x.2.2) =
    ∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2

Tactic:
apply sum_nbij fun ((i, j), k, l) ↦ (i * k, j * l)

Result:
case hi
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
    (match a with
      | ((i, j), k, l) => (i * k, j * l)) ∈
      (m * n).divisorsAntidiagonal

case i_inj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ Set.InjOn
    (fun x =>
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal)

case i_surj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ Set.SurjOn
    (fun x =>
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) ↑(m * n).divisorsAntidiagonal

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
⊢ ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
    f a.1.1 * g a.1.2 * (f a.2.1 * g a.2.2) =
      f
          (match a with
            | ((i, j), k, l) => (i * k, j * l)).1 *
        g
          (match a with
            | ((i, j), k, l) => (i * k, j * l)).2

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
⊢ a2 = (a1 * a2).gcd (a2 * b2)

Tactic:
rw [mul_comm, Nat.gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one,
  mul_one]

Result:
no goals

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 * n = 0
⊢ ((((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 = m ∧ ¬m = 0) ∧
      ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2 = n ∧ ¬n = 0) ∧
    (((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1,
        ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2) =
      (b1, b2)

Tactic:
rw [← cop.gcd_mul _, ← cop.gcd_mul _, ← h.1, Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul cop h.1,
  Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul cop.symm _]

Result:
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 * n = 0
⊢ ((m = m ∧ ¬m = 0) ∧ n = n ∧ ¬n = 0) ∧ (b1.gcd (b1 * b2), b2.gcd (b1 * b2)) = (b1, b2)

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 * n = 0
⊢ b1 * b2 = n * m

Proof state:
case i_surj.mk
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 * n = 0
⊢ ∃ x, ((x.1.1 * x.1.2 = m ∧ ¬m = 0) ∧ x.2.1 * x.2.2 = n ∧ ¬n = 0) ∧ (x.1.1 * x.2.1, x.1.2 * x.2.2) = (b1, b2)

Tactic:
use ((b1.gcd m, b2.gcd m), (b1.gcd n, b2.gcd n))

Result:
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 * n = 0
⊢ ((((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 = m ∧ ¬m = 0) ∧
      ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2 = n ∧ ¬n = 0) ∧
    (((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1,
        ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2) =
      (b1, b2)

Proof state:
case i_surj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ∀ (x : ℕ × ℕ),
    x.1 * x.2 = m * n ∧ ¬m * n = 0 →
      ∃ x_1,
        ((x_1.1.1 * x_1.1.2 = m ∧ ¬m = 0) ∧ x_1.2.1 * x_1.2.2 = n ∧ ¬n = 0) ∧ (x_1.1.1 * x_1.2.1, x_1.1.2 * x_1.2.2) = x

Tactic:
rintro ⟨b1, b2⟩ h

Result:
case i_surj.mk
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).1 * (b1, b2).2 = m * n ∧ ¬m * n = 0
⊢ ∃ x, ((x.1.1 * x.1.2 = m ∧ ¬m = 0) ∧ x.2.1 * x.2.2 = n ∧ ¬n = 0) ∧ (x.1.1 * x.2.1, x.1.2 * x.2.2) = (b1, b2)

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
⊢ b2 = (b1 * b2).gcd (a2 * b2)

Tactic:
rw [Nat.gcd_mul_right, cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one,
  one_mul]

Result:
no goals

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 ×ˢ n.divisorsAntidiagonal, f x.1.1 * g x.1.2 * (f x.2.1 * g x.2.2)

Tactic:
symm

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.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal, f x.1.1 * g x.1.2 * (f x.2.1 * g x.2.2) =
    ∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2