awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ s, g i) : R) (∏ i ∈ s, (f : (a : ℕ) → R) (g i) : R)
have 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 a s) : Set ι).Pairwise (Coprime on g)),
  Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ insert a s, g i) : R) (∏ i ∈ insert a 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
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ s, g i) : R) (∏ i ∈ s, (f : (a : ℕ) → R) (g i) : R)
have empty : ∀ (hs : (↑∅ : Set ι).Pairwise (Coprime on g)),
  Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ ∅, g i) : R) (∏ i ∈ ∅, (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
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ s, g i) : R) (∏ i ∈ s, (f : (a : ℕ) → R) (g i) : R)
have 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 a s) : Set ι).Pairwise (Coprime on g)),
  Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ insert a s, g i) : R) (∏ i ∈ insert a 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
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
l : ℕ
hl : Squarefree l
⊢ Eq (α := R) (∏ a ∈ l.primeFactors, (f : (a : ℕ) → R) a : R) ((f : (a : ℕ) → R) l : R)
have rw : Eq (α := R) ((f : (a : ℕ) → R) (∏ a ∈ l.primeFactors, a) : R) ((f : (a : ℕ) → R) l : R)
Tactic: rw [← h_mult.map_prod_of_subset_primeFactors l _ Subset.rfl,
    prod_primeFactors_of_squarefree hl]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ Eq (α := R) (∏ a ∈ l.primeFactors, (f : (a : ℕ) → R) a : R) ((f : (a : ℕ) → R) l : R)
have rw₁ : Eq (α := R) ((f : (a : ℕ) → R) l : R) ((f : (a : ℕ) → R) l : R)
Tactic: rw [← h_mult.map_prod_of_subset_primeFactors l _ Subset.rfl,
    prod_primeFactors_of_squarefree hl]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ (f : (a : ℕ) → R) (l / d) = HDiv.hDiv (α := R) (β := R) ((f : (a : ℕ) → R) l : R) ((f : (a : ℕ) → R) d : R)
have apply : (f : (a : ℕ) → R) l = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (l / d) : R) ((f : (a : ℕ) → R) d : R)
Tactic: apply (div_eq_of_eq_mul hd ..).symm
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ (f : (a : ℕ) → R) l = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (l / d) : R) ((f : (a : ℕ) → R) d : R)
have rw : Eq (α := R) ((f : (a : ℕ) → R) l : R) ((f : (a : ℕ) → R) (l / d * d) : R)
Tactic: rw [← hf.right hl, Nat.div_mul_cancel hdl]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Defs (goal)
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)
⊢ (f : (a : ℕ) → R) l = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (l / d) : R) ((f : (a : ℕ) → R) d : R)
have rw₁ : Eq (α := R) ((f : (a : ℕ) → R) l : R) ((f : (a : ℕ) → R) l : R)
Tactic: rw [← hf.right hl, Nat.div_mul_cancel hdl]
-- 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
⊢ IsMultiplicative.{u_1} (R := R) (f * g)
have 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)
Tactic: refine ⟨by simp [hf.1, hg.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 : ℕ},
    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)
have 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))
Tactic: simp only [mul_apply]
-- 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
⊢ ∑ 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))
have 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))
Tactic: rw [sum_mul_sum, ← sum_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
m n : ℕ
cop : m.Coprime n
⊢ 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))
have 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))
Tactic: 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
⊢ 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))
have hi : ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
  Membership.mem (α := ℕ × ℕ) (m * n).divisorsAntidiagonal
    (match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) a with
      | ((i, j), k, l) => (i * k, j * l) :
      ℕ × ℕ)
Tactic: apply sum_nbij fun ((i, j), k, l) ↦ (i * k, j * l)
-- 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
hi :
  ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
    Membership.mem (α := ℕ × ℕ) (m * n).divisorsAntidiagonal
      (match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) a with
        | ((i, j), k, l) => (i * k, j * l) :
        ℕ × ℕ)
⊢ 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))
have i_inj : Set.InjOn (β := ℕ × ℕ)
  (fun (x : (ℕ × ℕ) × ℕ × ℕ) ↦
    match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) x with
    | ((i, j), k, l) => (i * k, j * l))
  (↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) : Set ((ℕ × ℕ) × ℕ × ℕ))
Tactic: apply sum_nbij fun ((i, j), k, l) ↦ (i * k, j * l)
-- 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
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 ((ℕ × ℕ) × ℕ × ℕ))
⊢ 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))
have 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 (ℕ × ℕ))
Tactic: apply sum_nbij fun ((i, j), k, l) ↦ (i * k, j * l)
-- 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
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 (ℕ × ℕ))
⊢ 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))
have 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)
Tactic: apply sum_nbij fun ((i, j), k, l) ↦ (i * k, j * l)
-- 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
a1 a2 b1 b2 : ℕ
h : ((a1, a2), b1, b2) ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal
⊢ Membership.mem (α := ℕ × ℕ) (m * n).divisorsAntidiagonal
    (match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) ((a1, a2), b1, b2) with
      | ((i, j), k, l) => (i * k, j * l) :
      ℕ × ℕ)
have h₁ : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
Tactic: simp only [mem_divisorsAntidiagonal, Ne, mem_product] 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
a1 a2 b1 b2 : ℕ
h : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
⊢ Membership.mem (α := ℕ × ℕ) (m * n).divisorsAntidiagonal
    (match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) ((a1, a2), b1, b2) with
      | ((i, j), k, l) => (i * k, j * l) :
      ℕ × ℕ)
have 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) :
      ℕ × ℕ)
Tactic: rcases h with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
Cleared hypotheses: m, n, cop, 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
a1 a2 b1 b2 : ℕ
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) :
      ℕ × ℕ)
have hi : a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2) ∧ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
Tactic: simp only [mem_divisorsAntidiagonal, mul_eq_zero, Ne]
-- 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 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2) ∧ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
have hi : a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2)
Tactic: constructor
-- 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 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
hi : a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2)
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2) ∧ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
have hi₁ : ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
Tactic: constructor
-- 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
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
have ha₁ : ¬(a1 = 0 ∨ a2 = 0)
Tactic: rw [mul_eq_zero] at *
Cleared hypotheses: ha, cop, hb
-- 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
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)
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
have hb₁ : ¬(b1 = 0 ∨ b2 = 0)
Tactic: rw [mul_eq_zero] at *
Cleared hypotheses: ha, cop, hb
-- 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.InjOn (β := ℕ × ℕ)
    (fun (x : (ℕ × ℕ) × ℕ × ℕ) ↦
      match (motive := (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ) x with
      | ((i, j), k, l) => (i * k, j * l))
    (↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) : Set ((ℕ × ℕ) × ℕ × ℕ))
have 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₂
Tactic: simp only [Set.InjOn, mem_coe, mem_divisorsAntidiagonal, mem_product, Prod.mk_inj]
-- 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
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
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
have i_inj : ((a1, a2), b1, b2).1.1 = ((c1, c2), d1, d2).1.1
Tactic: ext
-- 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
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
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
have i_inj₁ : ((a1, a2), b1, b2).1.2 = ((c1, c2), d1, d2).1.2
Tactic: ext
-- 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
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
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
have i_inj₂ : ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).2.1
Tactic: ext