awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ Eq.{u_1 + 1} (α := Rˣ)
      (∏ x ∈ n.divisorsAntidiagonal,
        HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
      (if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n
have rw : ∀ x ∈ n.divisorsAntidiagonal,
  (Units.coeHom R : (a : Rˣ) → R)
      (HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) sorry else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) =
    HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
Tactic: rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ (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 : ℤ)
have rw : (Units.coeHom R : (a : Rˣ) → R) (HPow.hPow (β := ℤ) (Units.mk0 (g x.2) sorry) ((μ : (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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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 : ℤ)
⊢ (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 : ℤ)
have rw₁ : (↑(HPow.hPow (β := ℤ) (Units.mk0 (g x.2) sorry) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) : R) =
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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 : ℤ)
⊢ (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 : ℤ)
have rw₂ : HPow.hPow (β := ℤ) (↑(Units.mk0 (g x.2) sorry) : R) ((μ : (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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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 : ℤ)
⊢ (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 : ℤ)
have rw₃ : HPow.hPow (β := ℤ) (g x.2) ((μ : (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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : AddCommGroup 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, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ (∀ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
have rw : ∀ x ∈ n.divisors,
  HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / x) : ℤ) (g x) =
    HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / x) : ℤ) (G x)
Tactic: rw [sum_divisorsAntidiagonal' (f := fun x y => μ x • g y), ← this, sum_congr rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (g d) =
    HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (G d)
have rw : HSMul.hSMul (α := ℤ) (β := R) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (∑ i ∈ d.divisors, f i) =
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
have mp : ∑ d ∈ n.divisors, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (G d) = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ ∑ d ∈ n.divisors, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) (n / d) : ℤ) (G d) = f n
have mp : ∑ i ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) i.1 : ℤ) (G i.2) = f n
Tactic: rw [← sum_divisorsAntidiagonal' (f := fun x y => μ x • G y)]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ ∑ i ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) i.1 : ℤ) (G i.2) = f n
have apply : ∀ n > 0, ∑ i ∈ n.divisors, f i = G n
Tactic: apply sum_eq_iff_sum_smul_moebius_eq.mp _ n hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ ∑ i ∈ n.divisors, f i = g n
have rw : ∀ x ∈ n.divisors, f x = F x
Tactic: rw [← this, sum_congr rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ f d = F d
have rw : ∑ x ∈ d.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = F d
Tactic: rw [← h d (pos_of_mem_divisors hd) <| hs d n (dvd_of_mem_divisors hd) hnP]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ ∑ i ∈ n.divisors, f i = g n
have mpr : ∑ d ∈ n.divisors, F d = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ ∑ d ∈ n.divisors, F d = g n
have apply : ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = F n
Tactic: apply sum_eq_iff_sum_smul_moebius_eq.mpr _ n hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
have refine : ∀ (n : ℕ) (h : n > 0 → n ∈ s → P n) (hn : n ∈ s), n > 0
Tactic: refine forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h ?_ hn⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ n > 0
have contrapose! : ∀ (hs₀ : n ≤ 0), 0 ∈ s
Tactic: contrapose! hs₀
Cleared hypotheses: hs₀
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (hypothesis)
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
⊢ (∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔
    ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
have this : ∀ (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
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : NonAssocRing 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, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f n
have 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
Tactic: rw [sum_eq_iff_sum_smul_moebius_eq_on s hs]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ 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
have 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
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
have 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)
Tactic: refine imp_congr_right ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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)
have 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
Tactic: refine fun _ => imp_congr_right fun _ => (sum_congr rfl fun x _hx => ?_).congr_left
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
h_1 : a ∈ s
x : ℕ × ℕ
_hx : x ∈ a.divisorsAntidiagonal
⊢ HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2
have h : (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2
Tactic: rw [zsmul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
have 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) sorry else 1 : Rˣ)) i)
          ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (g n) sorry else 1 : Rˣ)) 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 => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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)
⊢ (∀ 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
have 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) sorry else 1 : Rˣ)) x.2)
              ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
          ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (f n) sorry else 1 : Rˣ)) 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 => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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)
have 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) sorry else 1 : Rˣ)) i)
        ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (g n) sorry else 1 : Rˣ)) n)
Tactic: refine imp_congr_right fun hn => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
have 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) sorry else 1 : Rˣ)) x.2)
            ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
        ((fun (n : ℕ) ↦ (if h : 0 < n then Units.mk0 (f n) sorry else 1 : Rˣ)) n) ↔
    n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n
Tactic: refine imp_congr_right fun hn => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ 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)
have rw : ∀ x ∈ n.divisors, f x = (Units.coeHom R : (a : Rˣ) → R) (if h : 0 < x then Units.mk0 (f x) sorry else 1)
Tactic: rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ f x = (Units.coeHom R : (a : Rˣ) → R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)
have rw : f x = (Units.coeHom R : (a : Rˣ) → R) (Units.mk0 (f x) sorry)
Tactic: rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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) ⋯)
⊢ f x = (Units.coeHom R : (a : Rˣ) → R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)
have rw₁ : f x = (↑(Units.mk0 (f x) sorry) : R)
Tactic: rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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)
⊢ f x = (Units.coeHom R : (a : Rˣ) → R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)
have rw₂ : f x = f x
Tactic: rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]