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

Proof state:
case i_inj.mk.mk.mk.intro.intro.intro.mk.mk.mk.fst.fst
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
⊢ a1 = c1

Tactic:
trans Nat.gcd (a1 * a2) (a1 * b1)

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

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

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

Tactic:
rw [← hcd.1.1, ← hcd.2.1] at cop

Result:
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
⊢ (a1 * a2).gcd (a1 * b1) = c1

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

Tactic:
rw [Nat.gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_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
⊢ ∀ (a : (ℕ × ℕ) × ℕ × ℕ),
    (a.1.1 * a.1.2 = m ∧ ¬m = 0) ∧ a.2.1 * a.2.2 = n ∧ ¬n = 0 →
      f a.1.1 * g a.1.2 * (f a.2.1 * g a.2.2) = f (a.1.1 * a.2.1) * g (a.1.2 * a.2.2)

Tactic:
rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩

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, a2), b1, b2).1.1 * g ((a1, a2), b1, b2).1.2 * (f ((a1, a2), b1, b2).2.1 * g ((a1, a2), b1, b2).2.2) =
    f (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1) * g (((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2)

Proof state:
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

Tactic:
rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ h

Result:
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), b1, b2) ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal
⊢ (match ((a1, a2), b1, b2) with
    | ((i, j), k, l) => (i * k, j * l)) ∈
    (m * n).divisorsAntidiagonal