awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
ι : Type u_2
inst : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (Coprime on g)),
    Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ s, g i) : R) (∏ i ∈ s, (f : (a : ℕ) → R) (g i) : R)
hs : (↑(insert a s) : Set ι).Pairwise (Coprime on g)
⊢ (↑s : Set ι).Pairwise (Coprime on g) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (Coprime on g) a b

Tactic:
rw [coe_insert, Set.pairwise_insert_of_symmetric (Coprime.symmetric.comap g)] at hs

Premises used: Symmetric.comap, Set.pairwise_insert_of_symmetric, Nat.Coprime.symmetric, Finset.coe_insert
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
ι : Type u_2
inst : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (Coprime on g)),
    Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ s, g i) : R) (∏ i ∈ s, (f : (a : ℕ) → R) (g i) : R)
hs : (↑s : Set ι).Pairwise (Coprime on g) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (Coprime on g) a b
insert : (g a).gcd (∏ x ∈ s, g x) = 1
⊢ Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ Insert.insert a s, g i) : R)
    (∏ i ∈ Insert.insert a s, (f : (a : ℕ) → R) (g i) : R)

Tactic:
rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]

Premises used: Finset.prod_insert, And.left, ArithmeticFunction.IsMultiplicative.map_mul_of_coprime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
ι : Type u_2
inst : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (Coprime on g)),
    Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ s, g i) : R) (∏ i ∈ s, (f : (a : ℕ) → R) (g i) : R)
hs : (↑s : Set ι).Pairwise (Coprime on g) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (Coprime on g) a b
⊢ (g a).gcd (∏ x ∈ s, g x) = 1

Tactic:
Coprime.prod_right fun i hi => hs.2 _ hi (hi.ne_of_notMem has).symm

Premises used: Membership.mem.ne_of_notMem, Ne.symm, Nat.Coprime.prod_right, And.right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
ι : Type u_2
inst : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (Coprime on g)),
    Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ s, g i) : R) (∏ i ∈ s, (f : (a : ℕ) → R) (g i) : R)
hs : (↑s : Set ι).Pairwise (Coprime on g) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (Coprime on g) a b
⊢ (g a).gcd (∏ x ∈ s, g x) = 1

Tactic:
exact Coprime.prod_right fun i hi => hs.2 _ hi (hi.ne_of_notMem has).symm

Premises used: Membership.mem.ne_of_notMem, Ne.symm, Nat.Coprime.prod_right, And.right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
ι : Type u_2
inst : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
s : Finset ι
hs : (↑s : Set ι).Pairwise (Coprime on g)
empty :
  ∀ (hs : (↑∅ : Set ι).Pairwise (Coprime on g)),
    Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ ∅, g i) : R) (∏ i ∈ ∅, (f : (a : ℕ) → R) (g i) : R)
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih :
      ∀ (hs : (↑s : Set ι).Pairwise (Coprime on g)),
        Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ s, g i) : R) (∏ i ∈ s, (f : (a : ℕ) → R) (g i) : R))
    (hs : (↑(Insert.insert a s) : Set ι).Pairwise (Coprime on g)),
    Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ Insert.insert a s, g i) : R)
      (∏ i ∈ Insert.insert a s, (f : (a : ℕ) → R) (g i) : R)
⊢ Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ s, g i) : R) (∏ i ∈ s, (f : (a : ℕ) → R) (g i) : R)

Tactic:
induction s using Finset.induction_on with
    | empty => simp [hf]
    | insert _ _ has ih =>
      rw [coe_insert, Set.pairwise_insert_of_symmetric (Coprime.symmetric.comap g)] at hs
      rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]
      exact Coprime.prod_right fun i hi => hs.2 _ hi (hi.ne_of_notMem has).symm

Premises used: Symmetric.comap, Insert.insert, Set.pairwise_insert_of_symmetric, Nat.Coprime.symmetric, Finset.coe_insert, ArithmeticFunction.IsMultiplicative.map_mul_of_coprime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
ι : Type u_2
inst : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
s : Finset ι
hs : (↑s : Set ι).Pairwise (Coprime on g)
empty :
  ∀ (hs : (↑∅ : Set ι).Pairwise (Coprime on g)),
    Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ ∅, g i) : R) (∏ i ∈ ∅, (f : (a : ℕ) → R) (g i) : R)
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih :
      ∀ (hs : (↑s : Set ι).Pairwise (Coprime on g)),
        Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ s, g i) : R) (∏ i ∈ s, (f : (a : ℕ) → R) (g i) : R))
    (hs : (↑(Insert.insert a s) : Set ι).Pairwise (Coprime on g)),
    Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ Insert.insert a s, g i) : R)
      (∏ i ∈ Insert.insert a s, (f : (a : ℕ) → R) (g i) : R)
⊢ Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ s, g i) : R) (∏ i ∈ s, (f : (a : ℕ) → R) (g i) : R)

Tactic:
classical
    induction s using Finset.induction_on with
    | empty => simp [hf]
    | insert _ _ has ih =>
      rw [coe_insert, Set.pairwise_insert_of_symmetric (Coprime.symmetric.comap g)] at hs
      rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]
      exact Coprime.prod_right fun i hi => hs.2 _ hi (hi.ne_of_notMem has).symm

Premises used: Symmetric.comap, Insert.insert, Set.pairwise_insert_of_symmetric, Nat.Coprime.symmetric, Finset.coe_insert, ArithmeticFunction.IsMultiplicative.map_mul_of_coprime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
t : Finset ℕ
ht : ∀ p ∈ t, Nat.Prime p
⊢ Eq (α := R) ((f : (a : ℕ) → R) (∏ a ∈ t, a) : R) (∏ a ∈ t, (f : (a : ℕ) → R) a : R)

Tactic:
map_prod _ h_mult t fun x hx y hy hxy => (coprime_primes (ht x hx) (ht y hy)).mpr hxy

Premises used: Iff.mpr, ArithmeticFunction.IsMultiplicative.map_prod, Nat.coprime_primes
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
l : ℕ
t : Finset ℕ
ht : t ⊆ l.primeFactors
⊢ Eq (α := R) ((f : (a : ℕ) → R) (∏ a ∈ t, a) : R) (∏ a ∈ t, (f : (a : ℕ) → R) a : R)

Tactic:
map_prod_of_prime h_mult t fun _ a => prime_of_mem_primeFactors (ht a)

Premises used: ArithmeticFunction.IsMultiplicative.map_prod_of_prime, Nat.prime_of_mem_primeFactors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
l : ℕ
hl : Squarefree l
rw : Eq (α := R) ((f : (a : ℕ) → R) (∏ a ∈ l.primeFactors, a) : R) ((f : (a : ℕ) → R) l : R)
rw₁ rw₂ : Eq (α := R) ((f : (a : ℕ) → R) l : R) ((f : (a : ℕ) → R) l : R)
⊢ Eq (α := R) (∏ a ∈ l.primeFactors, (f : (a : ℕ) → R) a : R) ((f : (a : ℕ) → R) l : R)

Tactic:
rw [← h_mult.map_prod_of_subset_primeFactors l _ Subset.rfl,
    prod_primeFactors_of_squarefree hl]

Premises used: ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors, Finset.Subset.rfl, Nat.prod_primeFactors_of_squarefree
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : GroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : (l / d).Coprime d
hd : Ne (α := R) ((f : (a : ℕ) → R) d : R) (0 : R)
apply : (f : (a : ℕ) → R) l = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (l / d) : R) ((f : (a : ℕ) → R) d : R)
⊢ (f : (a : ℕ) → R) (l / d) = HDiv.hDiv (α := R) (β := R) ((f : (a : ℕ) → R) l : R) ((f : (a : ℕ) → R) d : R)

Tactic:
apply (div_eq_of_eq_mul hd ..).symm

Premises used: div_eq_of_eq_mul, Eq.symm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : GroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : (l / d).Coprime d
hd : Ne (α := R) ((f : (a : ℕ) → R) d : R) (0 : R)
rw : Eq (α := R) ((f : (a : ℕ) → R) l : R) ((f : (a : ℕ) → R) (l / d * d) : R)
rw₁ rw₂ : Eq (α := R) ((f : (a : ℕ) → R) l : R) ((f : (a : ℕ) → R) l : R)
⊢ (f : (a : ℕ) → R) l = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (l / d) : R) ((f : (a : ℕ) → R) d : R)

Tactic:
rw [← hf.right hl, Nat.div_mul_cancel hdl]

Premises used: Nat.div_mul_cancel, And.right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
f : ArithmeticFunction ℕ
inst : Semiring R
h : f.IsMultiplicative
⊢ Eq.{u_1 + 1} (α := R) ((((↑f : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) 1 : R) (1 : R)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
f : ArithmeticFunction ℕ
inst : Semiring R
h : f.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ (((↑f : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) (m * n) =
    HMul.hMul (α := R) (β := R) ((((↑f : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) m : R)
      ((((↑f : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) n : R)

Tactic:
simp [h.2 cop]

Premises used: And.right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
f : ArithmeticFunction ℤ
inst : Ring R
h : f.IsMultiplicative
⊢ Eq.{u_1 + 1} (α := R) ((((↑f : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) 1 : R) (1 : R)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
f : ArithmeticFunction ℤ
inst : Ring R
h : f.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ (((↑f : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) (m * n) =
    HMul.hMul (α := R) (β := R) ((((↑f : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) m : R)
      ((((↑f : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) n : R)

Tactic:
simp [h.2 cop]

Premises used: And.right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
⊢ Eq (α := R) ((f * g : (a : ℕ) → R) 1 : R) (1 : R)

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

Premises used: And.left
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
refine :
  ∀ {m n : ℕ},
    m.Coprime n →
      (f * g : (a : ℕ) → R) (m * n) =
        HMul.hMul (α := R) (β := R) ((f * g : (a : ℕ) → R) m : R) ((f * g : (a : ℕ) → R) n : R)
⊢ IsMultiplicative.{u_1} (R := R) (f * g)

Tactic:
refine ⟨by simp [hf.1, hg.1], ?_⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
simp :
  ∀ {m n : ℕ},
    m.Coprime n →
      ∑ x ∈ (m * n).divisorsAntidiagonal,
          HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R) =
        HMul.hMul (α := R)
          (∑ x ∈ m.divisorsAntidiagonal,
            HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
          (∑ x ∈ n.divisorsAntidiagonal,
            HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
⊢ ∀ {m n : ℕ},
    m.Coprime n →
      (f * g : (a : ℕ) → R) (m * n) =
        HMul.hMul (α := R) (β := R) ((f * g : (a : ℕ) → R) m : R) ((f * g : (a : ℕ) → R) n : R)

Tactic:
simp only [mul_apply]

Premises used: ArithmeticFunction.mul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
m n : ℕ
cop : m.Coprime n
rw :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ (m * n).divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
    (∑ x ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1.1 : R) ((g : (a : ℕ) → R) x.1.2 : R) *
        HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.2.1 : R) ((g : (a : ℕ) → R) x.2.2 : R))
⊢ ∑ x ∈ (m * n).divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R) =
    HMul.hMul (α := R)
      (∑ x ∈ m.divisorsAntidiagonal,
        HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
      (∑ x ∈ n.divisorsAntidiagonal,
        HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))

Tactic:
rw [sum_mul_sum, ← sum_product']

Premises used: Finset.sum_product', Finset.sum_mul_sum
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
m n : ℕ
cop : m.Coprime n
symm :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1.1 : R) ((g : (a : ℕ) → R) x.1.2 : R) *
        HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.2.1 : R) ((g : (a : ℕ) → R) x.2.2 : R))
    (∑ x ∈ (m * n).divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ (m * n).divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
    (∑ x ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1.1 : R) ((g : (a : ℕ) → R) x.1.2 : R) *
        HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.2.1 : R) ((g : (a : ℕ) → R) x.2.2 : R))

Tactic:
symm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
m n : ℕ
cop : m.Coprime n
hi :
  ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
    Membership.mem (α := ℕ × ℕ) (m * n).divisorsAntidiagonal
      (match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) a with
        | ((i, j), k, l) => (i * k, j * l) :
        ℕ × ℕ)
i_inj :
  Set.InjOn (β := ℕ × ℕ)
    (fun (x : (ℕ × ℕ) × ℕ × ℕ) ↦
      match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) x with
      | ((i, j), k, l) => (i * k, j * l))
    (↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) : Set ((ℕ × ℕ) × ℕ × ℕ))
i_surj :
  Set.SurjOn
    (fun (x : (ℕ × ℕ) × ℕ × ℕ) ↦
      match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) x with
      | ((i, j), k, l) => (i * k, j * l))
    (↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) : Set ((ℕ × ℕ) × ℕ × ℕ))
    (↑(m * n).divisorsAntidiagonal : Set (ℕ × ℕ))
h :
  ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) a.1.1 : R) ((g : (a : ℕ) → R) a.1.2 : R) *
        HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) a.2.1 : R) ((g : (a : ℕ) → R) a.2.2 : R) =
      HMul.hMul (α := R) (β := R)
        ((f : (a : ℕ) → R)
            (match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) a with
              | ((i, j), k, l) => (i * k, j * l)).1 :
          R)
        ((g : (a : ℕ) → R)
            (match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) a with
              | ((i, j), k, l) => (i * k, j * l)).2 :
          R)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1.1 : R) ((g : (a : ℕ) → R) x.1.2 : R) *
        HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.2.1 : R) ((g : (a : ℕ) → R) x.2.2 : R))
    (∑ x ∈ (m * n).divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))

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

Premises used: Finset.sum_nbij
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
m n : ℕ
cop : m.Coprime n
a1 a2 b1 b2 : ℕ
h : ((a1, a2), b1, b2) ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal
⊢ (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0

Tactic:
simp only [mem_divisorsAntidiagonal, Ne, mem_product] at h

Premises used: Nat.mem_divisorsAntidiagonal, Ne, Finset.mem_product
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
m n : ℕ
cop : m.Coprime n
a1 a2 b1 b2 : ℕ
h : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
hi :
  ∀ (ha : ¬a1 * a2 = 0) (cop : (a1 * a2).Coprime (b1 * b2)) (hb : ¬b1 * b2 = 0),
    Membership.mem (α := ℕ × ℕ) (a1 * a2 * (b1 * b2)).divisorsAntidiagonal
      (match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) ((a1, a2), b1, b2) with
        | ((i, j), k, l) => (i * k, j * l) :
        ℕ × ℕ)
⊢ Membership.mem (α := ℕ × ℕ) (m * n).divisorsAntidiagonal
    (match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) ((a1, a2), b1, b2) with
      | ((i, j), k, l) => (i * k, j * l) :
      ℕ × ℕ)

Tactic:
rcases h with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
hi : a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2) ∧ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
⊢ Membership.mem (α := ℕ × ℕ) (a1 * a2 * (b1 * b2)).divisorsAntidiagonal
    (match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) ((a1, a2), b1, b2) with
      | ((i, j), k, l) => (i * k, j * l) :
      ℕ × ℕ)

Tactic:
simp only [mem_divisorsAntidiagonal, mul_eq_zero, Ne]

Premises used: Nat.mem_divisorsAntidiagonal, Ne, Nat.mul_eq_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
hi : a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2)
hi₁ : ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2) ∧ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
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
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ¬(a1 = 0 ∨ a2 = 0)

Tactic:
rw [mul_eq_zero] at *

Premises used: Nat.mul_eq_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
ha₁ : ¬(a1 = 0 ∨ a2 = 0)
⊢ (a1 * a2).Coprime (b1 * b2)

Tactic:
rw [mul_eq_zero] at *

Premises used: Nat.mul_eq_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
ha₁ : ¬(a1 = 0 ∨ a2 = 0)
cop₁ : (a1 * a2).Coprime (b1 * b2)
⊢ ¬(b1 = 0 ∨ b2 = 0)

Tactic:
rw [mul_eq_zero] at *

Premises used: Nat.mul_eq_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
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:
not_or_intro ha hb

Premises used: not_or_intro
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
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:
exact not_or_intro ha hb

Premises used: not_or_intro
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
m n : ℕ
cop : m.Coprime n
i_inj :
  ∀ ⦃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 →
          HMul.hMul (α := ℕ) x₁.1.1 x₁.2.1 = HMul.hMul (α := ℕ) x₂.1.1 x₂.2.1 ∧
              HMul.hMul (α := ℕ) x₁.1.2 x₁.2.2 = HMul.hMul (α := ℕ) x₂.1.2 x₂.2.2 →
            x₁ = x₂
⊢ Set.InjOn (β := ℕ × ℕ)
    (fun (x : (ℕ × ℕ) × ℕ × ℕ) ↦
      match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) x with
      | ((i, j), k, l) => (i * k, j * l))
    (↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) : Set ((ℕ × ℕ) × ℕ × ℕ))

Tactic:
simp only [Set.InjOn, mem_coe, mem_divisorsAntidiagonal, mem_product, Prod.mk_inj]

Premises used: Nat.mem_divisorsAntidiagonal, Prod.mk_inj, Set.InjOn, Finset.mem_product, Finset.mem_coe
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
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 :
  HMul.hMul (α := ℕ) ((a1, a2), b1, b2).1.1 ((a1, a2), b1, b2).2.1 =
      HMul.hMul (α := ℕ) ((c1, c2), d1, d2).1.1 ((c1, c2), d1, d2).2.1 ∧
    HMul.hMul (α := ℕ) ((a1, a2), b1, b2).1.2 ((a1, a2), b1, b2).2.2 =
      HMul.hMul (α := ℕ) ((c1, c2), d1, d2).1.2 ((c1, c2), d1, d2).2.2
i_inj : ((a1, a2), b1, b2).1.1 = ((c1, c2), d1, d2).1.1
i_inj₁ : ((a1, a2), b1, b2).1.2 = ((c1, c2), d1, d2).1.2
i_inj₂ : ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).2.1
i_inj₃ : ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)

Tactic:
ext