-- 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
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.1 * x₁.1.2 = m ∧ ¬m = 0) ∧ x₁.2.1 * x₁.2.2 = n ∧ ¬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.1 * x₂.2.1 ∧ x₁.1.2 * x₁.2.2 = x₂.1.2 * x₂.2.2 → x₁ = x₂

Tactic:
rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩ ⟨⟨c1, c2⟩, ⟨d1, d2⟩⟩ hcd h

Result:
case i_inj.mk.mk.mk.intro.intro.intro.mk.mk.mk
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, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)

Proof state:
case i_inj.mk.mk.mk.intro.intro.intro.mk.mk.mk.snd.snd
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 = d2

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

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

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

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
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ b1 * b2 = n * m

Tactic:
rw [mul_comm n m, h.1]

Result:
no goals

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 = 0 ∨ a2 = 0)
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬(b1 = 0 ∨ b2 = 0)
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)

Tactic:
apply not_or_intro ha hb

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 ∈ 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

Tactic:
simp only [mem_divisorsAntidiagonal, Ne, mem_product]

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
⊢ ∀ (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)

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

Tactic:
simp [hf.1, hg.1]

Result:
no goals

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

Tactic:
simp only [mul_apply]

Result:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ ∀ {m n : ℕ},
    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

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, 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)

Tactic:
dsimp only

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 * b1) * g (a2 * b2)