awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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
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 :
  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
rw : (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2).gcd (a2 * b2) = ((c1, c2), d1, d2).2.2
rw₁ :
  (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2).gcd
      (HMul.hMul (α := ℕ) ((c1, c2), d1, d2).1.2 ((c1, c2), d1, d2).2.2) =
    ((c1, c2), d1, d2).2.2
rw₂ : ((c1, c2), d1, d2).2.1.gcd ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2 = ((c1, c2), d1, d2).2.2
rw₃ : 1 * ((c1, c2), d1, d2).2.2 = ((c1, c2), d1, d2).2.2
⊢ (b1 * b2).gcd (a2 * b2) = ((c1, c2), d1, d2).2.2
have rw₄ : ((c1, c2), d1, d2).2.2 = ((c1, c2), d1, d2).2.2
Tactic: rw [← hcd.2.1, h.2, gcd_mul_right,
          cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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
⊢ 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 (ℕ × ℕ))
have 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
Tactic: simp only [Set.SurjOn, Set.subset_def, mem_coe, mem_divisorsAntidiagonal, mem_product,
      Set.mem_image]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use ((b1.gcd m, b2.gcd m), (b1.gcd n, b2.gcd n))
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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.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)
have 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)
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 _]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ ((((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)
have rw : b1 * b2 = n * m
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 _]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (hypothesis)
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
⊢ ((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)
have h₁ : (b1, b2).1 * (b1, b2).2 = m * n ∧ ¬m = 0 ∧ ¬n = 0
Tactic: rw [Ne, mul_eq_zero, not_or] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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 = n * m
have rw : b1 * b2 = m * n
Tactic: rw [mul_comm n m, h.1]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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
⊢ b1 * b2 = n * m
have rw₁ : m * n = m * n
Tactic: rw [mul_comm n m, h.1]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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
⊢ ∀ 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)
have 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)
Tactic: simp only [mem_divisorsAntidiagonal, mem_product]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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) (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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
have 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)
Tactic: refine and_congr_right' (forall₂_congr fun m n => ⟨fun h _ _ => h, fun h hmn => ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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
⊢ (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)
have 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)
Tactic: rcases eq_or_ne m 0 with (rfl | hm)
Cleared hypotheses: m, h, hmn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)
have inr : ∀ (hm : m ≠ 0),
  (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)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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
⊢ (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)
have 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)
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n, h, hmn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)
have inr₁ : ∀ (hn : n ≠ 0),
  (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)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
⊢ f = g ↔ ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)
have mp : f = g → ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ f = g ↔ ∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)
have mpr : (∀ (p i : ℕ), Nat.Prime p → Eq (α := R) ((f : (a : ℕ) → R) (p ^ i) : R) ((g : (a : ℕ) → R) (p ^ i) : R)) → f = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ f = g
have mpr : ∀ (n : ℕ), Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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 : ℕ
⊢ Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
have pos : ∀ (hn : n = 0), Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
have neg : ∀ (hn : ¬n = 0), Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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 (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
have pos : Eq (α := R) ((f : (a : ℕ) → R) 0 : R) ((g : (a : ℕ) → R) 0 : R)
Tactic: rw [hn, ArithmeticFunction.map_zero, ArithmeticFunction.map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
have pos₁ : Eq (α := R) (0 : R) ((g : (a : ℕ) → R) 0 : R)
Tactic: rw [hn, ArithmeticFunction.map_zero, ArithmeticFunction.map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ Eq (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
have pos₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [hn, ArithmeticFunction.map_zero, ArithmeticFunction.map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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 (α := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
have 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))
Tactic: rw [multiplicative_factorization f hf hn, multiplicative_factorization g hg hn]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
⊢ 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)
have 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)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
have 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)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (hypothesis)
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)
have hgcd_ne_zero : x.gcd y ≠ 0
Tactic: have hgcd_ne_zero : x.gcd y ≠ 0 := gcd_ne_zero_left hx
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (hypothesis)
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
⊢ 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)
have hlcm_ne_zero : x.lcm y ≠ 0
Tactic: have hlcm_ne_zero : x.lcm y ≠ 0 := lcm_ne_zero hx hy
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
have rw : Eq (α := R) ((f : (a : ℕ) → R) 1 : R) (1 : R)
Tactic: rw [pow_zero, hf.1]