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