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

Tactic:
simp only [Prod.mk.inj_iff] at 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 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)

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

Tactic:
simp only [mem_divisorsAntidiagonal, Ne, mem_product] at 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 = 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

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

Tactic:
dsimp at 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 = 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:
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
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2) ∧ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)

Tactic:
constructor

Result:
case hi.mk.mk.mk.intro.intro.intro.left
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 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2)

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)

Proof state:
case hi.mk.mk.mk.intro.intro.intro.left
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 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2)

Tactic:
ring

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

Tactic:
rw [← hcd.2.1, h.2, Nat.gcd_mul_right,
  cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]

Result:
no goals

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
⊢ Set.InjOn
    (fun x =>
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal)

Tactic:
simp only [Set.InjOn, mem_coe, mem_divisorsAntidiagonal, Ne, mem_product, Prod.mk.inj_iff]

Result:
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₂

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
⊢ Set.SurjOn
    (fun x =>
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) ↑(m * n).divisorsAntidiagonal

Tactic:
simp only [Set.SurjOn, Set.subset_def, mem_coe, mem_divisorsAntidiagonal, Ne, mem_product,
  Set.mem_image, exists_prop, Prod.mk.inj_iff]

Result:
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

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

Tactic:
ring

Result:
no goals