R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
f1 : ↑f 1 = 1
⊢ ↑(f * g) 1 = 1
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
⊢ ↑(f * g) 1 = 1
have f1 := hf.left
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
f1 : ↑f 1 = 1
g1 : ↑g 1 = 1
⊢ ↑(f * g) 1 = 1
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
f1 : ↑f 1 = 1
⊢ ↑(f * g) 1 = 1
have g1 := hg.left
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
f1 : ↑f 1 = 1
g1 : ↑g 1 = 1
⊢ ↑f 1 * ↑g 1 = 1
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
f1 : ↑f 1 = 1
g1 : ↑g 1 = 1
⊢ ↑(f * g) 1 = 1
simp only [mul_apply, divisorsAntidiagonal_one, ZeroHom.toFun_eq_coe, sum_singleton]
no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
f1 : ↑f 1 = 1
g1 : ↑g 1 = 1
⊢ ↑f 1 * ↑g 1 = 1
rw [f1, g1, mul_one]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
⊢ ∀ {m n : ℕ},
    coprime m n →
      ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd =
        (∑ x in divisorsAntidiagonal m, ↑f x.fst * ↑g x.snd) * ∑ x in divisorsAntidiagonal n, ↑f x.fst * ↑g x.snd
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
⊢ ∀ {m n : ℕ}, coprime m n → ↑(f * g) (m * n) = ↑(f * g) m * ↑(f * g) n
simp only [mul_apply]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd =
    (∑ x in divisorsAntidiagonal m, ↑f x.fst * ↑g x.snd) * ∑ x in divisorsAntidiagonal n, ↑f x.fst * ↑g x.snd
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
⊢ ∀ {m n : ℕ},
    coprime m n →
      ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd =
        (∑ x in divisorsAntidiagonal m, ↑f x.fst * ↑g x.snd) * ∑ x in divisorsAntidiagonal n, ↑f x.fst * ↑g x.snd
intro m n cop
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd =
    ∑ p in divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n, ↑f p.fst.fst * ↑g p.fst.snd * (↑f p.snd.fst * ↑g p.snd.snd)
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd =
    (∑ x in divisorsAntidiagonal m, ↑f x.fst * ↑g x.snd) * ∑ x in divisorsAntidiagonal n, ↑f x.fst * ↑g x.snd
rw [sum_mul_sum]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∑ p in divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n, ↑f p.fst.fst * ↑g p.fst.snd * (↑f p.snd.fst * ↑g p.snd.snd) =
    ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd =
    ∑ p in divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n, ↑f p.fst.fst * ↑g p.fst.snd * (↑f p.snd.fst * ↑g p.snd.snd)
symm
case hi
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (a : (ℕ × ℕ) × ℕ × ℕ),
    a ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
      (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd) ∈ divisorsAntidiagonal (m * n)

case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (a : (ℕ × ℕ) × ℕ × ℕ),
    a ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
      ↑f a.fst.fst * ↑g a.fst.snd * (↑f a.snd.fst * ↑g a.snd.snd) =
        ↑f (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd).fst * ↑g (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd).snd

case i_inj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (a₁ a₂ : (ℕ × ℕ) × ℕ × ℕ),
    a₁ ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
      a₂ ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
        (a₁.fst.fst * a₁.snd.fst, a₁.fst.snd * a₁.snd.snd) = (a₂.fst.fst * a₂.snd.fst, a₂.fst.snd * a₂.snd.snd) →
          a₁ = a₂

case i_surj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (b : ℕ × ℕ), b ∈ divisorsAntidiagonal (m * n) → ∃ a ha, b = (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd)
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∑ p in divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n, ↑f p.fst.fst * ↑g p.fst.snd * (↑f p.snd.fst * ↑g p.snd.snd) =
    ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd
apply sum_bij fun (x : (ℕ × ℕ) × ℕ × ℕ) _h => (x.1.1 * x.2.1, x.1.2 * x.2.2)
case hi.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : ((a1, a2), b1, b2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
⊢ (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) ∈
    divisorsAntidiagonal (m * n)
case hi
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (a : (ℕ × ℕ) × ℕ × ℕ),
    a ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
      (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd) ∈ divisorsAntidiagonal (m * n)
rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ h
case hi.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
⊢ (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) ∈
    divisorsAntidiagonal (m * n)
case hi.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : ((a1, a2), b1, b2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
⊢ (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) ∈
    divisorsAntidiagonal (m * n)
simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at h
case hi.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) ∈
    divisorsAntidiagonal (a1 * a2 * (b1 * b2))
case hi.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
⊢ (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) ∈
    divisorsAntidiagonal (m * n)
rcases h with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
case hi.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2) ∧ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
case hi.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) ∈
    divisorsAntidiagonal (a1 * a2 * (b1 * b2))
simp only [mem_divisorsAntidiagonal, Nat.mul_eq_zero, Ne.def]
case hi.mk.mk.mk.intro.intro.intro.left
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (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 : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
case hi.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2) ∧ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
constructor
case hi.mk.mk.mk.intro.intro.intro.right
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬(a1 = 0 ∨ a2 = 0)
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬(b1 = 0 ∨ b2 = 0)
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
case hi.mk.mk.mk.intro.intro.intro.right
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
rw [Nat.mul_eq_zero] at *
no goals
case hi.mk.mk.mk.intro.intro.intro.right
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬(a1 = 0 ∨ a2 = 0)
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬(b1 = 0 ∨ b2 = 0)
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
apply not_or_of_not ha hb
no goals
case hi.mk.mk.mk.intro.intro.intro.left
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2)
ring
case h.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : ((a1, a2), b1, b2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
⊢ ↑f ((a1, a2), b1, b2).fst.fst * ↑g ((a1, a2), b1, b2).fst.snd *
      (↑f ((a1, a2), b1, b2).snd.fst * ↑g ((a1, a2), b1, b2).snd.snd) =
    ↑f
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).fst *
      ↑g
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).snd
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (a : (ℕ × ℕ) × ℕ × ℕ),
    a ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
      ↑f a.fst.fst * ↑g a.fst.snd * (↑f a.snd.fst * ↑g a.snd.snd) =
        ↑f (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd).fst * ↑g (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd).snd
rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ h
case h.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
⊢ ↑f ((a1, a2), b1, b2).fst.fst * ↑g ((a1, a2), b1, b2).fst.snd *
      (↑f ((a1, a2), b1, b2).snd.fst * ↑g ((a1, a2), b1, b2).snd.snd) =
    ↑f
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).fst *
      ↑g
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).snd
case h.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : ((a1, a2), b1, b2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
⊢ ↑f ((a1, a2), b1, b2).fst.fst * ↑g ((a1, a2), b1, b2).fst.snd *
      (↑f ((a1, a2), b1, b2).snd.fst * ↑g ((a1, a2), b1, b2).snd.snd) =
    ↑f
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).fst *
      ↑g
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).snd
simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at h
case h.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ↑f ((a1, a2), b1, b2).fst.fst * ↑g ((a1, a2), b1, b2).fst.snd *
      (↑f ((a1, a2), b1, b2).snd.fst * ↑g ((a1, a2), b1, b2).snd.snd) =
    ↑f
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).fst *
      ↑g
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).snd
case h.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
⊢ ↑f ((a1, a2), b1, b2).fst.fst * ↑g ((a1, a2), b1, b2).fst.snd *
      (↑f ((a1, a2), b1, b2).snd.fst * ↑g ((a1, a2), b1, b2).snd.snd) =
    ↑f
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).fst *
      ↑g
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).snd
rcases h with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
case h.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ↑f a1 * ↑g a2 * (↑f b1 * ↑g b2) = ↑f (a1 * b1) * ↑g (a2 * b2)
case h.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ↑f ((a1, a2), b1, b2).fst.fst * ↑g ((a1, a2), b1, b2).fst.snd *
      (↑f ((a1, a2), b1, b2).snd.fst * ↑g ((a1, a2), b1, b2).snd.snd) =
    ↑f
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).fst *
      ↑g
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).snd
dsimp only
case h.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ↑f a1 * ↑g a2 * (↑f b1 * ↑g b2) = ↑f a1 * ↑f b1 * (↑g a2 * ↑g b2)
case h.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ↑f a1 * ↑g a2 * (↑f b1 * ↑g b2) = ↑f (a1 * b1) * ↑g (a2 * b2)
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]
no goals
case h.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ↑f a1 * ↑g a2 * (↑f b1 * ↑g b2) = ↑f a1 * ↑f b1 * (↑g a2 * ↑g b2)
ring
case i_inj.mk.mk.mk.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
hab : ((a1, a2), b1, b2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
hcd : ((c1, c2), d1, d2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
case i_inj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (a₁ a₂ : (ℕ × ℕ) × ℕ × ℕ),
    a₁ ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
      a₂ ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
        (a₁.fst.fst * a₁.snd.fst, a₁.fst.snd * a₁.snd.snd) = (a₂.fst.fst * a₂.snd.fst, a₂.fst.snd * a₂.snd.snd) →
          a₁ = a₂
rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ ⟨⟨c1, c2⟩, ⟨d1, d2⟩⟩ hab hcd h
case i_inj.mk.mk.mk.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
hcd : ((c1, c2), d1, d2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
hab : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
case i_inj.mk.mk.mk.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
hab : ((a1, a2), b1, b2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
hcd : ((c1, c2), d1, d2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at hab
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hcd : ((c1, c2), d1, d2) ∈ divisorsAntidiagonal (a1 * a2) ×ˢ divisorsAntidiagonal (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
case i_inj.mk.mk.mk.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
hcd : ((c1, c2), d1, d2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
hab : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
rcases hab with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hcd : ((c1, c2), d1, d2) ∈ divisorsAntidiagonal (a1 * a2) ×ˢ divisorsAntidiagonal (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at hcd
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
simp only [Prod.mk.inj_iff] at h
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₁.h₁
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a1 = c1

case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₁.h₂
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a2 = c2

case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₂.h₁
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b1 = d1

case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₂.h₂
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b2 = d2
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
ext <;> dsimp only
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a1 = gcd (a1 * a2) (a1 * b1)

R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a1 * b1) = c1
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₁.h₁
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a1 = c1
trans Nat.gcd (a1 * a2) (a1 * b1)
no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a1 = gcd (a1 * a2) (a1 * b1)
rw [Nat.gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a1 * b1) = c1
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a1 * b1) = c1
rw [← hcd.1.1, ← hcd.2.1] at cop
no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a1 * b1) = c1
rw [← hcd.1.1, h.1, Nat.gcd_mul_left,
  cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a2 = gcd (a1 * a2) (a2 * b2)

R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a2 * b2) = c2
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₁.h₂
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a2 = c2
trans Nat.gcd (a1 * a2) (a2 * b2)
no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a2 = gcd (a1 * a2) (a2 * b2)
rw [mul_comm, Nat.gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one,
  mul_one]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a2 * b2) = c2
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a2 * b2) = c2
rw [← hcd.1.1, ← hcd.2.1] at cop
no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a2 * b2) = c2
rw [← hcd.1.1, h.2, mul_comm, Nat.gcd_mul_left,
  cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one, mul_one]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b1 = gcd (b1 * b2) (a1 * b1)

R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a1 * b1) = d1
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₂.h₁
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b1 = d1
trans Nat.gcd (b1 * b2) (a1 * b1)
no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b1 = gcd (b1 * b2) (a1 * b1)
rw [mul_comm, Nat.gcd_mul_right,
  cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one, one_mul]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a1 * b1) = d1
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a1 * b1) = d1
rw [← hcd.1.1, ← hcd.2.1] at cop
no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a1 * b1) = d1
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]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b2 = gcd (b1 * b2) (a2 * b2)

R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a2 * b2) = d2
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₂.h₂
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b2 = d2
trans Nat.gcd (b1 * b2) (a2 * b2)
no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b2 = gcd (b1 * b2) (a2 * b2)
rw [Nat.gcd_mul_right, cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one,
  one_mul]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a2 * b2) = d2
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a2 * b2) = d2
rw [← hcd.1.1, ← hcd.2.1] at cop
no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a2 * b2) = d2
rw [← hcd.2.1, h.2, Nat.gcd_mul_right,
  cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : (b1, b2) ∈ divisorsAntidiagonal (m * n)
⊢ ∃ a ha, (b1, b2) = (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd)
case i_surj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (b : ℕ × ℕ), b ∈ divisorsAntidiagonal (m * n) → ∃ a ha, b = (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd)
rintro ⟨b1, b2⟩ h
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ∃ a ha, (b1, b2) = (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd)
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : (b1, b2) ∈ divisorsAntidiagonal (m * n)
⊢ ∃ a ha, (b1, b2) = (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd)
simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at h
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ∃ ha,
    (b1, b2) =
      (((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).fst.fst * ((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).snd.fst,
        ((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).fst.snd * ((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).snd.snd)
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ∃ a ha, (b1, b2) = (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd)
use ((b1.gcd m, b2.gcd m), (b1.gcd n, b2.gcd n))
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ((gcd b1 m * gcd b2 m = m ∧ ¬m = 0) ∧ gcd b1 n * gcd b2 n = n ∧ ¬n = 0) ∧
    b1 = gcd b1 m * gcd b1 n ∧ b2 = gcd b2 m * gcd b2 n
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ∃ ha,
    (b1, b2) =
      (((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).fst.fst * ((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).snd.fst,
        ((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).fst.snd * ((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).snd.snd)
simp only [exists_prop, Prod.mk.inj_iff, Ne.def, mem_product, mem_divisorsAntidiagonal]
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ((m = m ∧ ¬m = 0) ∧ n = n ∧ ¬n = 0) ∧ b1 = gcd b1 (b1 * b2) ∧ b2 = gcd b2 (b1 * b2)

R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ b1 * b2 = n * m
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ((gcd b1 m * gcd b2 m = m ∧ ¬m = 0) ∧ gcd b1 n * gcd b2 n = n ∧ ¬n = 0) ∧
    b1 = gcd b1 m * gcd b1 n ∧ b2 = gcd b2 m * gcd b2 n
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 _]
no goals
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ b1 * b2 = n * m
rw [mul_comm n m, h.1]
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m = 0 ∧ ¬n = 0
⊢ ((m = m ∧ ¬m = 0) ∧ n = n ∧ ¬n = 0) ∧ b1 = gcd b1 (b1 * b2) ∧ b2 = gcd b2 (b1 * b2)
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ((m = m ∧ ¬m = 0) ∧ n = n ∧ ¬n = 0) ∧ b1 = gcd b1 (b1 * b2) ∧ b2 = gcd b2 (b1 * b2)
rw [Nat.mul_eq_zero, not_or] at h
no goals
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m = 0 ∧ ¬n = 0
⊢ ((m = m ∧ ¬m = 0) ∧ n = n ∧ ¬n = 0) ∧ b1 = gcd b1 (b1 * b2) ∧ b2 = gcd b2 (b1 * b2)
simp [h.2.1, h.2.2]