rw [Nat.Prime.coprime_iff_not_dvd hxp]
case a.hs
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
hxp : (↑x).Prime
⊢ (↑x).Coprime ↑y
case a.hs
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
hi :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M),
    i a ha ∈ Finset.filter (fun x => d ∣ x) (d ^ M).divisors
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
x : { x // x ∈ d.primeFactors }
a✝¹ : x ∈ ↑d.primeFactors.attach
y : { x // x ∈ d.primeFactors }
a✝ : y ∈ ↑d.primeFactors.attach
hxy : x ≠ y
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 0 < a a_1 h ∧ a a_1 h ≤ M
hxp : (↑x).Prime
⊢ ¬↑x ∣ ↑y