awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ × ℕ
hx : x ∈ n.divisorsAntidiagonal
rw :
  (Units.coeHom R : (a : Rˣ) → R) (HPow.hPow (β := ℤ) (Units.mk0 (g x.2) ⋯) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) =
    HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
rw₁ :
  (↑(HPow.hPow (β := ℤ) (Units.mk0 (g x.2) ⋯) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) : R) =
    HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
rw₂ :
  HPow.hPow (β := ℤ) (↑(Units.mk0 (g x.2) ⋯) : R) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) =
    HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
rw₃ rw₄ :
  HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
⊢ (Units.coeHom R : (a : Rˣ) → R)
      (HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) =
    HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)

Tactic:
rw [dif_pos (pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)), Units.coeHom_apply,
      Units.val_zpow_eq_zpow_val, Units.val_mk0]

Premises used: Nat.snd_mem_divisors_of_mem_antidiagonal, dif_pos, Units.val_zpow_eq_zpow_val, Units.coeHom_apply, Units.val_mk0, Nat.pos_of_mem_divisors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
mp :
  (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) →
    ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
mpr :
  (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n) →
    ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
⊢ (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (G d) = f n
rw :
  ∀ x ∈ n.divisors,
    HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / x) : ℤ) (g x) =
      HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / x) : ℤ) (G x)
⊢ ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n

Tactic:
rw [sum_divisorsAntidiagonal' (f := fun x y => μ x • g y), ← this, sum_congr rfl]

Premises used: Nat.sum_divisorsAntidiagonal', ArithmeticFunction.moebius, HSMul.hSMul, DFunLike.coe, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (G d) = f n
d : ℕ
hd : d ∈ n.divisors
rw rw₁ :
  HSMul.hSMul (α := ℤ) (β := R) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (∑ i ∈ d.divisors, f i) =
    HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (G d)
⊢ HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (g d) =
    HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (G d)

Tactic:
rw [← h d (pos_of_mem_divisors hd) <| hs d n (dvd_of_mem_divisors hd) hnP]

Premises used: Nat.dvd_of_mem_divisors, Nat.pos_of_mem_divisors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
mp : ∑ d ∈ n.divisors, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (G d) = f n
⊢ ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n

Tactic:
suffices ∑ d ∈ n.divisors, μ (n / d) • G d = f n by
      rw [sum_divisorsAntidiagonal' (f := fun x y => μ x • g y), ← this, sum_congr rfl]
      intro d hd
      rw [← h d (pos_of_mem_divisors hd) <| hs d n (dvd_of_mem_divisors hd) hnP]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
mp : ∑ i ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) i.1 : ℤ) (G i.2) = f n
⊢ ∑ d ∈ n.divisors, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (G d) = f n

Tactic:
rw [← sum_divisorsAntidiagonal' (f := fun x y => μ x • G y)]

Premises used: Nat.sum_divisorsAntidiagonal', ArithmeticFunction.moebius, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
apply : ∀ n > 0, ∑ i ∈ n.divisors, f i = G n
⊢ ∑ i ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) i.1 : ℤ) (G i.2) = f n

Tactic:
apply sum_eq_iff_sum_smul_moebius_eq.mp _ n hn

Premises used: ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq, Iff.mp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
n_1 : ℕ
_ : n_1 > 0 → ∑ i ∈ n_1.divisors, f i = G n_1
⊢ n_1 > 0 → ∑ i ∈ n_1.divisors, f i = G n_1

Tactic:
_
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
n_1 : ℕ
h_1 : n_1 > 0
⊢ ∑ i ∈ n_1.divisors, f i = G n_1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
F : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2)
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, F d = g n
rw : ∀ x ∈ n.divisors, f x = F x
⊢ ∑ i ∈ n.divisors, f i = g n

Tactic:
rw [← this, sum_congr rfl]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
F : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2)
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, F d = g n
d : ℕ
hd : d ∈ n.divisors
rw rw₁ : ∑ x ∈ d.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = F d
⊢ f d = F d

Tactic:
rw [← h d (pos_of_mem_divisors hd) <| hs d n (dvd_of_mem_divisors hd) hnP]

Premises used: Nat.dvd_of_mem_divisors, Nat.pos_of_mem_divisors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
F : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2)
n : ℕ
hn : n > 0
hnP : n ∈ s
mpr : ∑ d ∈ n.divisors, F d = g n
⊢ ∑ i ∈ n.divisors, f i = g n

Tactic:
suffices ∑ d ∈ n.divisors, F d = g n by
      rw [← this, sum_congr rfl]
      intro d hd
      rw [← h d (pos_of_mem_divisors hd) <| hs d n (dvd_of_mem_divisors hd) hnP]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
F : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2)
n : ℕ
hn : n > 0
hnP : n ∈ s
apply : ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = F n
⊢ ∑ d ∈ n.divisors, F d = g n

Tactic:
apply sum_eq_iff_sum_smul_moebius_eq.mpr _ n hn

Premises used: Iff.mpr, ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
F : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2)
n : ℕ
hn : n > 0
hnP : n ∈ s
n_1 : ℕ
_ : n_1 > 0 → ∑ x ∈ n_1.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = F n_1
⊢ n_1 > 0 → ∑ x ∈ n_1.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = F n_1

Tactic:
_
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
F : (n : ℕ) → R := fun (n : ℕ) ↦ ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2)
n : ℕ
hn : n > 0
hnP : n ∈ s
n_1 : ℕ
h_1 : n_1 > 0
⊢ ∑ x ∈ n_1.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = F n_1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
P : ℕ → Prop
⊢ (∀ n ∈ s, P n) ↔ ∀ n > 0, n ∈ s → P n

Tactic:
forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h ?_ hn⟩)

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
P : ℕ → Prop
refine : ∀ (n : ℕ) (h : n > 0 → n ∈ s → P n) (hn : n ∈ s), n > 0
⊢ (∀ n ∈ s, P n) ↔ ∀ n > 0, n ∈ s → P n

Tactic:
refine forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h ?_ hn⟩)
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
P : ℕ → Prop
n : ℕ
h : n > 0 → n ∈ s → P n
hn : n ∈ s
contrapose! : ∀ (hs₀ : n ≤ 0), 0 ∈ s
⊢ n > 0

Tactic:
contrapose! hs₀
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
P : ℕ → Prop
n : ℕ
h : n > 0 → n ∈ s → P n
hn : n ∈ s
hs₀ : n ≤ 0
⊢ 0 ∈ s

Tactic:
simpa [nonpos_iff_eq_zero.mp hs₀] using hn

Premises used: Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
⊢ ∀ (P : ℕ → Prop), (∀ n ∈ s, P n) ↔ ∀ n > 0, n ∈ s → P n

Tactic:
have : ∀ P : ℕ → Prop, ((∀ n ∈ s, P n) ↔ (∀ n > 0, n ∈ s → P n)) := fun P ↦ by
    refine forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h ?_ hn⟩)
    contrapose! hs₀
    simpa [nonpos_iff_eq_zero.mp hs₀] using hn
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
this : ∀ (P : ℕ → Prop), (∀ n ∈ s, P n) ↔ ∀ n > 0, n ∈ s → P n
⊢ (∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔
    ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n

Tactic:
simpa only [this] using sum_eq_iff_sum_smul_moebius_eq_on s hs

Premises used: ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
rw :
  (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n) ↔
    ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f n
⊢ (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f n

Tactic:
rw [sum_eq_iff_sum_smul_moebius_eq_on s hs]

Premises used: ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h :
  ∀ (a : ℕ),
    a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f a ↔
      a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f a
⊢ (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n) ↔
    ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f n

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
⊢ a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f a ↔
    a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f a

Tactic:
imp_congr_right ?_

Premises used: imp_congr_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
h :
  a > 0 →
    (a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f a ↔
      a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f a)
⊢ a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f a ↔
    a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f a

Tactic:
refine imp_congr_right ?_

Premises used: imp_congr_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
⊢ a > 0 →
    (a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f a ↔
      a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f a)

Tactic:
fun _ => imp_congr_right fun _ => (sum_congr rfl fun x _hx => ?_).congr_left

Premises used: imp_congr_right, Eq.congr_left, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
h :
  a > 0 →
    a ∈ s →
      ∀ (x : ℕ × ℕ) (_hx : x ∈ a.divisorsAntidiagonal),
        HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2
⊢ a > 0 →
    (a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f a ↔
      a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f a)

Tactic:
refine fun _ => imp_congr_right fun _ => (sum_congr rfl fun x _hx => ?_).congr_left

Premises used: imp_congr_right, Eq.congr_left, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
h_1 : a > 0
h_2 : a ∈ s
x : ℕ × ℕ
_hx : x ∈ a.divisorsAntidiagonal
h h₁ : (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2
⊢ HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2

Tactic:
rw [zsmul_eq_mul]

Premises used: zsmul_eq_mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
@sum_eq_iff_sum_smul_moebius_eq_on (Additive R) _ _ _ s hs

Premises used: Additive, Multiset.prod, Finset.prod, ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
⊢ (∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
Iff.trans
        (Iff.trans (forall_congr' fun n => ?_)
          (@prod_eq_iff_prod_pow_moebius_eq_on Rˣ _
            (fun n => if h : 0 < n then Units.mk0 (f n) (hf n h) else 1)
            (fun n => if h : 0 < n then Units.mk0 (g n) (hg n h) else 1)
            s hs))
        (forall_congr' fun n => ?_)

Premises used: forall_congr', Iff.trans, ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
refine_1 :
  ∀ (n : ℕ),
    n > 0 → n ∈ s → ∏ i ∈ n.divisors, f i = g n ↔
      n > 0 →
        n ∈ s →
          Eq.{u_1 + 1} (α := Rˣ) (∏ i ∈ n.divisors, (fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (f n) ⋯ else 1 : Rˣ)) i)
            ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (g n) ⋯ else 1 : Rˣ)) n)
refine_2 :
  ∀ (n : ℕ),
    n > 0 →
        n ∈ s →
          Eq.{u_1 + 1} (α := Rˣ)
            (∏ x ∈ n.divisorsAntidiagonal,
              HPow.hPow (α := Rˣ) (β := ℤ) ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (g n) ⋯ else 1 : Rˣ)) x.2)
                ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
            ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (f n) ⋯ else 1 : Rˣ)) n) ↔
      n > 0 → n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n
⊢ (∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
refine
      Iff.trans
        (Iff.trans (forall_congr' fun n => ?_)
          (@prod_eq_iff_prod_pow_moebius_eq_on Rˣ _
            (fun n => if h : 0 < n then Units.mk0 (f n) (hf n h) else 1)
            (fun n => if h : 0 < n then Units.mk0 (g n) (hg n h) else 1)
            s hs))
        (forall_congr' fun n => ?_)

Premises used: forall_congr', Iff.trans, ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
⊢ n > 0 → n ∈ s → ∏ i ∈ n.divisors, f i = g n ↔
    n > 0 →
      n ∈ s →
        Eq.{u_1 + 1} (α := Rˣ) (∏ i ∈ n.divisors, (fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (f n) ⋯ else 1 : Rˣ)) i)
          ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (g n) ⋯ else 1 : Rˣ)) n)

Tactic:
imp_congr_right fun hn => ?_

Premises used: imp_congr_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
refine_1 :
  ∀ (hn : n > 0),
    n ∈ s → ∏ i ∈ n.divisors, f i = g n ↔
      n ∈ s →
        Eq.{u_1 + 1} (α := Rˣ) (∏ i ∈ n.divisors, (fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (f n) ⋯ else 1 : Rˣ)) i)
          ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (g n) ⋯ else 1 : Rˣ)) n)
⊢ n > 0 → n ∈ s → ∏ i ∈ n.divisors, f i = g n ↔
    n > 0 →
      n ∈ s →
        Eq.{u_1 + 1} (α := Rˣ) (∏ i ∈ n.divisors, (fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (f n) ⋯ else 1 : Rˣ)) i)
          ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (g n) ⋯ else 1 : Rˣ)) n)

Tactic:
refine imp_congr_right fun hn => ?_

Premises used: imp_congr_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
⊢ n > 0 →
      n ∈ s →
        Eq.{u_1 + 1} (α := Rˣ)
          (∏ x ∈ n.divisorsAntidiagonal,
            HPow.hPow (α := Rˣ) (β := ℤ) ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (g n) ⋯ else 1 : Rˣ)) x.2)
              ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
          ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (f n) ⋯ else 1 : Rˣ)) n) ↔
    n > 0 → n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
imp_congr_right fun hn => ?_

Premises used: imp_congr_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
refine_2 :
  ∀ (hn : n > 0),
    n ∈ s →
        Eq.{u_1 + 1} (α := Rˣ)
          (∏ x ∈ n.divisorsAntidiagonal,
            HPow.hPow (α := Rˣ) (β := ℤ) ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (g n) ⋯ else 1 : Rˣ)) x.2)
              ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
          ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (f n) ⋯ else 1 : Rˣ)) n) ↔
      n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n
⊢ n > 0 →
      n ∈ s →
        Eq.{u_1 + 1} (α := Rˣ)
          (∏ x ∈ n.divisorsAntidiagonal,
            HPow.hPow (α := Rˣ) (β := ℤ) ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (g n) ⋯ else 1 : Rˣ)) x.2)
              ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
          ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (f n) ⋯ else 1 : Rˣ)) n) ↔
    n > 0 → n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
refine imp_congr_right fun hn => ?_

Premises used: imp_congr_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
rw : ∀ x ∈ n.divisors, f x = (Units.coeHom R : (a : Rˣ) → R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)
⊢ n ∈ s → ∏ i ∈ n.divisors, f i = g n ↔
    n ∈ s →
      Eq.{u_1 + 1} (α := Rˣ) (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1)
        (if h : 0 < n then Units.mk0 (g n) ⋯ else 1)

Tactic:
rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]

Premises used: dif_pos, Finset.prod_congr, map_prod, Units.val_inj, Units.coeHom_apply, Units.val_mk0, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ
hx : x ∈ n.divisors
rw : f x = (Units.coeHom R : (a : Rˣ) → R) (Units.mk0 (f x) ⋯)
rw₁ : f x = (↑(Units.mk0 (f x) ⋯) : R)
rw₂ rw₃ : f x = f x
⊢ f x = (Units.coeHom R : (a : Rˣ) → R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)

Tactic:
rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]

Premises used: dif_pos, Units.coeHom_apply, Units.val_mk0, Nat.pos_of_mem_divisors