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
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
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
have i_inj₃ : ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).2.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
⊢ ((a1, a2), b1, b2).1.1 = ((c1, c2), d1, d2).1.1
have trans : ((a1, a2), b1, b2).1.1 = (a1 * a2).gcd (a1 * b1)
Tactic: trans gcd (a1 * a2) (a1 * b1)
-- 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
trans : ((a1, a2), b1, b2).1.1 = (a1 * a2).gcd (a1 * b1)
⊢ ((a1, a2), b1, b2).1.1 = ((c1, c2), d1, d2).1.1
have trans₁ : (a1 * a2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
Tactic: trans gcd (a1 * a2) (a1 * b1)
-- 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).1.1 = (a1 * a2).gcd (a1 * b1)
have rw : ((a1, a2), b1, b2).1.1 = a1 * a2.gcd b1
Tactic: rw [gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
-- 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
rw : ((a1, a2), b1, b2).1.1 = a1 * a2.gcd b1
⊢ ((a1, a2), b1, b2).1.1 = (a1 * a2).gcd (a1 * b1)
have rw₁ : ((a1, a2), b1, b2).1.1 = a1 * 1
Tactic: rw [gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
-- 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
rw : ((a1, a2), b1, b2).1.1 = a1 * a2.gcd b1
rw₁ : ((a1, a2), b1, b2).1.1 = a1 * 1
⊢ ((a1, a2), b1, b2).1.1 = (a1 * a2).gcd (a1 * b1)
have rw₂ : ((a1, a2), b1, b2).1.1 = a1
Tactic: rw [gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
-- 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), 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).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
have 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)
Tactic: rw [← hcd.1.1, ← hcd.2.1] at cop
Cleared hypotheses: cop, hcd, 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), 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
⊢ (a1 * a2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
have rw : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
Tactic: rw [← hcd.1.1, h.1, gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one,
          mul_one]
-- 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).1.1 * ((c1, c2), d1, d2).1.2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
⊢ (a1 * a2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
have rw₁ : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).gcd
    (HMul.hMul (α := ℕ) ((c1, c2), d1, d2).1.1 ((c1, c2), d1, d2).2.1) =
  ((c1, c2), d1, d2).1.1
Tactic: rw [← hcd.1.1, h.1, gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one,
          mul_one]
-- 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).1.1 * ((c1, c2), d1, d2).1.2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
rw₁ :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).gcd
      (HMul.hMul (α := ℕ) ((c1, c2), d1, d2).1.1 ((c1, c2), d1, d2).2.1) =
    ((c1, c2), d1, d2).1.1
⊢ (a1 * a2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
have rw₂ : ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2.gcd ((c1, c2), d1, d2).2.1 = ((c1, c2), d1, d2).1.1
Tactic: rw [← hcd.1.1, h.1, gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one,
          mul_one]
-- 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).1.1 * ((c1, c2), d1, d2).1.2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
rw₁ :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).gcd
      (HMul.hMul (α := ℕ) ((c1, c2), d1, d2).1.1 ((c1, c2), d1, d2).2.1) =
    ((c1, c2), d1, d2).1.1
rw₂ : ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2.gcd ((c1, c2), d1, d2).2.1 = ((c1, c2), d1, d2).1.1
⊢ (a1 * a2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
have rw₃ : ((c1, c2), d1, d2).1.1 * 1 = ((c1, c2), d1, d2).1.1
Tactic: rw [← hcd.1.1, h.1, gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one,
          mul_one]
-- 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).1.1 * ((c1, c2), d1, d2).1.2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
rw₁ :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).gcd
      (HMul.hMul (α := ℕ) ((c1, c2), d1, d2).1.1 ((c1, c2), d1, d2).2.1) =
    ((c1, c2), d1, d2).1.1
rw₂ : ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2.gcd ((c1, c2), d1, d2).2.1 = ((c1, c2), d1, d2).1.1
rw₃ : ((c1, c2), d1, d2).1.1 * 1 = ((c1, c2), d1, d2).1.1
⊢ (a1 * a2).gcd (a1 * b1) = ((c1, c2), d1, d2).1.1
have rw₄ : ((c1, c2), d1, d2).1.1 = ((c1, c2), d1, d2).1.1
Tactic: rw [← hcd.1.1, h.1, gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one,
          mul_one]
-- 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).1.2 = ((c1, c2), d1, d2).1.2
have trans : ((a1, a2), b1, b2).1.2 = (a1 * a2).gcd (a2 * b2)
Tactic: trans gcd (a1 * a2) (a2 * b2)
-- 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
trans : ((a1, a2), b1, b2).1.2 = (a1 * a2).gcd (a2 * b2)
⊢ ((a1, a2), b1, b2).1.2 = ((c1, c2), d1, d2).1.2
have trans₁ : (a1 * a2).gcd (a2 * b2) = ((c1, c2), d1, d2).1.2
Tactic: trans gcd (a1 * a2) (a2 * b2)
-- 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).1.2 = (a1 * a2).gcd (a2 * b2)
have rw : ((a1, a2), b1, b2).1.2 = (a2 * a1).gcd (a2 * b2)
Tactic: rw [mul_comm, gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one,
          mul_one]
-- 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
rw : ((a1, a2), b1, b2).1.2 = (a2 * a1).gcd (a2 * b2)
⊢ ((a1, a2), b1, b2).1.2 = (a1 * a2).gcd (a2 * b2)
have rw₁ : ((a1, a2), b1, b2).1.2 = a2 * a1.gcd b2
Tactic: rw [mul_comm, gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one,
          mul_one]
-- 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
rw : ((a1, a2), b1, b2).1.2 = (a2 * a1).gcd (a2 * b2)
rw₁ : ((a1, a2), b1, b2).1.2 = a2 * a1.gcd b2
⊢ ((a1, a2), b1, b2).1.2 = (a1 * a2).gcd (a2 * b2)
have rw₂ : ((a1, a2), b1, b2).1.2 = a2 * 1
Tactic: rw [mul_comm, gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one,
          mul_one]