awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_surj :
  ∀ (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) ∧
          (HMul.hMul (α := ℕ) x_1.1.1 x_1.2.1, HMul.hMul (α := ℕ) x_1.1.2 x_1.2.2) = x
⊢ 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 (ℕ × ℕ))

Tactic:
simp only [Set.SurjOn, Set.subset_def, mem_coe, mem_divisorsAntidiagonal, mem_product,
      Set.mem_image]

Premises used: Set.subset_def, Set.SurjOn, Nat.mem_divisorsAntidiagonal, Set.mem_image, 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
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ m * n ≠ 0
h₁ :
  ((((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 = m ∧ m ≠ 0) ∧
      ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2 = n ∧ n ≠ 0) ∧
    (HMul.hMul (α := ℕ) ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1,
        HMul.hMul (α := ℕ) ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2
          ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2) =
      (b1, b2)
⊢ ∃ (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.2 x.2.2) = (b1, b2)

Tactic:
use ((b1.gcd m, b2.gcd m), (b1.gcd n, b2.gcd n))

Premises used: Nat.gcd, Prod.mk
-- 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
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ m * n ≠ 0
h₁ : ((m = m ∧ m ≠ 0) ∧ n = n ∧ n ≠ 0) ∧ (b1.gcd ((b1, b2).1 * (b1, b2).2), b2.gcd ((b1, b2).1 * (b1, b2).2)) = (b1, b2)
rw : b1 * b2 = n * m
⊢ ((((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2 = m ∧ m ≠ 0) ∧
      ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1 * ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2 = n ∧ n ≠ 0) ∧
    (HMul.hMul (α := ℕ) ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.1 ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.1,
        HMul.hMul (α := ℕ) ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).1.2
          ((b1.gcd m, b2.gcd m), b1.gcd n, b2.gcd n).2.2) =
      (b1, b2)

Tactic:
rw [← cop.gcd_mul _, ← cop.gcd_mul _, ← h.1, gcd_mul_gcd_of_coprime_of_mul_eq_mul cop h.1,
      gcd_mul_gcd_of_coprime_of_mul_eq_mul cop.symm _]

Premises used: Nat.Coprime.symm, Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul, Nat.Coprime.gcd_mul, 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
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ m * n ≠ 0
⊢ (b1, b2).1 * (b1, b2).2 = m * n ∧ ¬m = 0 ∧ ¬n = 0

Tactic:
rw [Ne, mul_eq_zero, not_or] at h

Premises used: Ne, not_or, 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
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ ¬m = 0 ∧ ¬n = 0
⊢ ((m = m ∧ m ≠ 0) ∧ n = n ∧ n ≠ 0) ∧ (b1.gcd ((b1, b2).1 * (b1, b2).2), b2.gcd ((b1, b2).1 * (b1, b2).2)) = (b1, b2)

Tactic:
simp [h.2.1, h.2.2]

Premises used: And.right, 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
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ m * n ≠ 0
rw : b1 * b2 = m * n
rw₁ rw₂ : m * n = m * n
⊢ b1 * b2 = n * m

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

Premises used: And.left, mul_comm
-- 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
h :
  ∀ (a : (ℕ × ℕ) × ℕ × ℕ),
    (a.1.1 * a.1.2 = m ∧ m ≠ 0) ∧ a.2.1 * a.2.2 = n ∧ n ≠ 0 →
      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) (HMul.hMul (α := ℕ) a.1.1 a.2.1) : R)
          ((g : (a : ℕ) → R) (HMul.hMul (α := ℕ) a.1.2 a.2.2) : R)
⊢ ∀ 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)

Tactic:
simp only [mem_divisorsAntidiagonal, mem_product]

Premises used: Nat.mem_divisorsAntidiagonal, 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
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
h :
  HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) ((a1, a2), b1, b2).1.1 : R)
        ((g : (a : ℕ) → R) ((a1, a2), b1, b2).1.2 : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) ((a1, a2), b1, b2).2.1 : R)
        ((g : (a : ℕ) → R) ((a1, a2), b1, b2).2.2 : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) ((a1, a2), b1, b2).1.1 : R)
        ((f : (a : ℕ) → R) ((a1, a2), b1, b2).2.1 : R) *
      HMul.hMul (α := R) (β := R) ((g : (a : ℕ) → R) ((a1, a2), b1, b2).1.2 : R)
        ((g : (a : ℕ) → R) ((a1, a2), b1, b2).2.2 : R)
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) ((a1, a2), b1, b2).1.1 : R)
        ((g : (a : ℕ) → R) ((a1, a2), b1, b2).1.2 : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) ((a1, a2), b1, b2).2.1 : R)
        ((g : (a : ℕ) → R) ((a1, a2), b1, b2).2.2 : R) =
    HMul.hMul (α := R) (β := R)
      ((f : (a : ℕ) → R) (HMul.hMul (α := ℕ) ((a1, a2), b1, b2).1.1 ((a1, a2), b1, b2).2.1) : R)
      ((g : (a : ℕ) → R) (HMul.hMul (α := ℕ) ((a1, a2), b1, b2).1.2 ((a1, a2), b1, b2).2.2) : R)

Tactic:
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]

Premises used: Nat.Coprime.coprime_mul_left_right, Nat.Coprime.coprime_mul_right, Nat.Coprime.coprime_mul_right_right, Nat.Coprime.coprime_mul_left, ArithmeticFunction.IsMultiplicative.map_mul_of_coprime
-- 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
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) ((a1, a2), b1, b2).1.1 : R)
        ((g : (a : ℕ) → R) ((a1, a2), b1, b2).1.2 : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) ((a1, a2), b1, b2).2.1 : R)
        ((g : (a : ℕ) → R) ((a1, a2), b1, b2).2.2 : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) ((a1, a2), b1, b2).1.1 : R)
        ((f : (a : ℕ) → R) ((a1, a2), b1, b2).2.1 : R) *
      HMul.hMul (α := R) (β := R) ((g : (a : ℕ) → R) ((a1, a2), b1, b2).1.2 : R)
        ((g : (a : ℕ) → R) ((a1, a2), b1, b2).2.2 : R)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : n ≠ 0
⊢ Eq (α := R) ((f : (a : ℕ) → R) n : R) (n.factorization.prod fun (p k : ℕ) ↦ (f : (a : ℕ) → R) (p ^ k) : R)

Tactic:
Nat.multiplicative_factorization f (fun _ _ => hf.2) hf.1 hn

Premises used: And.right, And.left, Nat.multiplicative_factorization, DFunLike.coe
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
⊢ f.IsMultiplicative ↔
    Eq (α := R) ((f : (a : ℕ) → R) 1 : R) (1 : R) ∧
      ∀ {m n : ℕ},
        m ≠ 0 →
          n ≠ 0 →
            m.Coprime n →
              (f : (a : ℕ) → R) (m * n) =
                HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)

Tactic:
and_congr_right' (forall₂_congr fun m n => ⟨fun h _ _ => h, fun h hmn => ?_⟩)

Premises used: and_congr_right', ArithmeticFunction.IsMultiplicative, forall₂_congr, Iff.intro
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
refine :
  ∀ (m n : ℕ)
    (h :
      m ≠ 0 →
        n ≠ 0 →
          m.Coprime n →
            (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R))
    (hmn : m.Coprime n),
    (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)
⊢ f.IsMultiplicative ↔
    Eq (α := R) ((f : (a : ℕ) → R) 1 : R) (1 : R) ∧
      ∀ {m n : ℕ},
        m ≠ 0 →
          n ≠ 0 →
            m.Coprime n →
              (f : (a : ℕ) → R) (m * n) =
                HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)

Tactic:
refine and_congr_right' (forall₂_congr fun m n => ⟨fun h _ _ => h, fun h hmn => ?_⟩)

Premises used: and_congr_right', forall₂_congr, Iff.intro
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h :
  m ≠ 0 →
    n ≠ 0 →
      m.Coprime n →
        (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)
hmn : m.Coprime n
inl :
  ∀
    (h :
      Ne (α := ℕ) 0 0 →
        n ≠ 0 →
          Coprime 0 n →
            (f : (a : ℕ) → R) (0 * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) n : R))
    (hmn : Coprime 0 n),
    (f : (a : ℕ) → R) (0 * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) n : R)
inr :
  ∀ (hm : m ≠ 0),
    (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)
⊢ (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
n : ℕ
h :
  Ne (α := ℕ) 0 0 →
    n ≠ 0 →
      Coprime 0 n →
        (f : (a : ℕ) → R) (0 * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) n : R)
hmn : Coprime 0 n
⊢ (f : (a : ℕ) → R) (0 * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) n : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h :
  m ≠ 0 →
    n ≠ 0 →
      m.Coprime n →
        (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)
hmn : m.Coprime n
hm : m ≠ 0
inr :
  ∀
    (h :
      m ≠ 0 →
        Ne (α := ℕ) 0 0 →
          m.Coprime 0 →
            (f : (a : ℕ) → R) (m * 0) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) 0 : R))
    (hmn : m.Coprime 0),
    (f : (a : ℕ) → R) (m * 0) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) 0 : R)
inr₁ :
  ∀ (hn : n ≠ 0),
    (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)
⊢ (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
m : ℕ
hm : m ≠ 0
h :
  m ≠ 0 →
    Ne (α := ℕ) 0 0 →
      m.Coprime 0 →
        (f : (a : ℕ) → R) (m * 0) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) 0 : R)
hmn : m.Coprime 0
⊢ (f : (a : ℕ) → R) (m * 0) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) 0 : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h :
  m ≠ 0 →
    n ≠ 0 →
      m.Coprime n →
        (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)
hmn : m.Coprime n
hm : m ≠ 0
hn : n ≠ 0
⊢ (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)

Tactic:
h hm hn hmn
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h :
  m ≠ 0 →
    n ≠ 0 →
      m.Coprime n →
        (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)
hmn : m.Coprime n
hm : m ≠ 0
hn : n ≠ 0
⊢ (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)

Tactic:
exact h hm hn hmn
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
mp : f = g → ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)
mpr : (∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)) → f = g
⊢ f = g ↔ ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : f = g
⊢ ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)
mpr : ∀ (n : ℕ), Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
⊢ f = g

Tactic:
ext n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)
n : ℕ
pos : ∀ (hn : n = 0), Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
neg : ∀ (hn : ¬n = 0), Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
⊢ Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)
n : ℕ
hn : n = 0
pos : Eq (α := R) ((f : (a : ℕ) → R) 0 : R) ((g : (a : ℕ) → R) 0 : R)
pos₁ : Eq (α := R) (0 : R) ((g : (a : ℕ) → R) 0 : R)
pos₂ pos₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)

Tactic:
rw [hn, ArithmeticFunction.map_zero, ArithmeticFunction.map_zero]

Premises used: ArithmeticFunction.map_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)
n : ℕ
hn : ¬n = 0
neg :
  Eq.{u_1 + 1} (α := R) (n.factorization.prod fun (p k : ℕ) ↦ (f : (a : ℕ) → R) (p ^ k))
    (n.factorization.prod fun (p k : ℕ) ↦ (g : (a : ℕ) → R) (p ^ k))
⊢ Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)

Tactic:
rw [multiplicative_factorization f hf hn, multiplicative_factorization g hg hn]

Premises used: ArithmeticFunction.IsMultiplicative.multiplicative_factorization
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)
n : ℕ
hn : ¬n = 0
⊢ Eq.{u_1 + 1} (α := R) (n.factorization.prod fun (p k : ℕ) ↦ (f : (a : ℕ) → R) (p ^ k))
    (n.factorization.prod fun (p k : ℕ) ↦ (g : (a : ℕ) → R) (p ^ k))

Tactic:
prod_congr rfl fun p hp ↦ h p _ (prime_of_mem_primeFactors hp)

Premises used: Finset.prod_congr, Nat.prime_of_mem_primeFactors, DFunLike.coe, Nat.factorization, Finsupp.prod, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)
n : ℕ
hn : ¬n = 0
⊢ Eq.{u_1 + 1} (α := R) (n.factorization.prod fun (p k : ℕ) ↦ (f : (a : ℕ) → R) (p ^ k))
    (n.factorization.prod fun (p k : ℕ) ↦ (g : (a : ℕ) → R) (p ^ k))

Tactic:
exact prod_congr rfl fun p hp ↦ h p _ (prime_of_mem_primeFactors hp)

Premises used: Finset.prod_congr, Nat.prime_of_mem_primeFactors, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
pos :
  ∀ (hx : x = 0),
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)
neg :
  ∀ (hx : ¬x = 0),
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : x = 0
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)

Tactic:
simp only [hx, f.map_zero, zero_mul, lcm_zero_left, gcd_zero_left]

Premises used: MulZeroClass.zero_mul, ArithmeticFunction.map_zero, Nat.lcm_zero_left, Nat.gcd_zero_left
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
pos :
  ∀ (hy : y = 0),
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)
neg :
  ∀ (hy : ¬y = 0),
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : y = 0
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x.lcm y) : R) ((f : (a : ℕ) → R) (x.gcd y) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) y : R)

Tactic:
simp only [hy, f.map_zero, mul_zero, lcm_zero_right, gcd_zero_right, zero_mul]

Premises used: Nat.gcd_zero_right, MulZeroClass.zero_mul, Nat.lcm_zero_right, MulZeroClass.mul_zero, ArithmeticFunction.map_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
⊢ x.gcd y ≠ 0

Tactic:
have hgcd_ne_zero : x.gcd y ≠ 0 := gcd_ne_zero_left hx
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
⊢ x.lcm y ≠ 0

Tactic:
have hlcm_ne_zero : x.lcm y ≠ 0 := lcm_ne_zero hx hy
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
i : ℕ
rw : Eq (α := R) ((f : (a : ℕ) → R) 1 : R) (1 : R)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)

Tactic:
rw [pow_zero, hf.1]

Premises used: pow_zero, And.left
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
⊢ ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)

Tactic:
have hfi_zero : ∀ {i}, f (i ^ 0) = 1 := by
    intro i; rw [pow_zero, hf.1]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, Eq (α := R) ((f : (a : ℕ) → R) (HPow.hPow (β := ℕ) i 0) : R) (1 : R)
⊢ x.lcm y ≠ 0

Tactic:
assumption