awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
pos :
  ∀ (hn : ∃ (j : ℕ), p ^ j = n),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (p ^ i * n) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ i) :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            n :
          R)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ i * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ i) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)
have neg : ∀ (hn : ¬∃ (j : ℕ), p ^ j = n),
  (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ i * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ i) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)
Tactic: by_cases hn : ∃ j, p ^ j = n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
hn : ∃ (j : ℕ), p ^ j = n
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ i * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ i) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)
have pos : ∀ (j : ℕ) (hmn : (p ^ i).Coprime (p ^ j)),
  (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ i * p ^ j) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ i) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ j) :
        R)
Tactic: obtain ⟨j, rfl⟩ := hn
Cleared hypotheses: n, hmn, hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i j : ℕ
hmn : (p ^ i).Coprime (p ^ j)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ i * p ^ j) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ i) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ j) :
        R)
have pos : ∀ (hmn : (HPow.hPow (β := ℕ) p 0).Coprime (p ^ j)),
  (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (HPow.hPow (β := ℕ) p 0 * p ^ j) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (HPow.hPow (β := ℕ) p 0) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ j) :
        R)
Tactic: cases i
Cleared hypotheses: i, hmn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i j : ℕ
hmn : (p ^ i).Coprime (p ^ j)
pos :
  ∀ (hmn : (HPow.hPow (β := ℕ) p 0).Coprime (p ^ j)),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (HPow.hPow (β := ℕ) p 0 * p ^ j) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (HPow.hPow (β := ℕ) p 0) :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ j) :
          R)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ i * p ^ j) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ i) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ j) :
        R)
have pos₁ : ∀ (n : ℕ) (hmn : (p ^ (n + 1)).Coprime (p ^ j)),
  (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ (n + 1) * p ^ j) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ (n + 1)) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ j) :
        R)
Tactic: cases i
Cleared hypotheses: i, hmn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
j n : ℕ
hmn : (p ^ (n + 1)).Coprime (p ^ j)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ (n + 1) * p ^ j) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ (n + 1)) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ j) :
        R)
have pos : ∀ (hmn : (p ^ (n + 1)).Coprime (HPow.hPow (β := ℕ) p 0)),
  (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ (n + 1) * HPow.hPow (β := ℕ) p 0) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ (n + 1)) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (HPow.hPow (β := ℕ) p 0) :
        R)
Tactic: cases j
Cleared hypotheses: j, hmn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
j n : ℕ
hmn : (p ^ (n + 1)).Coprime (p ^ j)
pos :
  ∀ (hmn : (p ^ (n + 1)).Coprime (HPow.hPow (β := ℕ) p 0)),
    (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
              (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
            ArithmeticFunction R) :
          (a : ℕ) → R)
        (p ^ (n + 1) * HPow.hPow (β := ℕ) p 0) =
      HMul.hMul (α := R) (β := R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (p ^ (n + 1)) :
          R)
        ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                  (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
                ArithmeticFunction R) :
              (a : ℕ) → R)
            (HPow.hPow (β := ℕ) p 0) :
          R)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ (n + 1) * p ^ j) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ (n + 1)) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ j) :
        R)
have pos₁ : ∀ (n_1 : ℕ) (hmn : (p ^ (n + 1)).Coprime (p ^ (n_1 + 1))),
  (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ (n + 1) * p ^ (n_1 + 1)) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ (n + 1)) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ (n_1 + 1)) :
        R)
Tactic: cases j
Cleared hypotheses: j, hmn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
hn : ¬∃ (j : ℕ), p ^ j = n
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (p ^ i * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          (p ^ i) :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)
have neg : Function.extend (fun (x : ℕ) ↦ p ^ x)
    (fun (x : ℕ) ↦
      (PowerSeries.coeff x : (a : PowerSeries R) → R)
        (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
    0 (p ^ i * n) =
  HMul.hMul (α := R)
    (Function.extend (fun (x : ℕ) ↦ p ^ x)
      (fun (x : ℕ) ↦
        (PowerSeries.coeff x : (a : PowerSeries R) → R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
      0 (p ^ i))
    (Function.extend (fun (x : ℕ) ↦ p ^ x)
      (fun (x : ℕ) ↦
        (PowerSeries.coeff x : (a : PowerSeries R) → R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
      0 n)
Tactic: simp_rw [ofPowerSeries_apply hp.one_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
hn : ¬∃ (j : ℕ), p ^ j = n
⊢ Function.extend (fun (x : ℕ) ↦ p ^ x)
      (fun (x : ℕ) ↦
        (PowerSeries.coeff x : (a : PowerSeries R) → R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
      0 (p ^ i * n) =
    HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 (p ^ i))
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 n)
have neg : ¬∃ (a : ℕ), p ^ a = p ^ i * n
Tactic: rw [Function.extend_apply', Function.extend_apply' _ _ _ hn,
        Pi.zero_apply, Pi.zero_apply, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
hn : ¬∃ (j : ℕ), p ^ j = n
⊢ ¬∃ (a : ℕ), p ^ a = p ^ i * n
have neg : ∀ (hn : ∃ (a : ℕ), p ^ a = p ^ i * n), ∃ (j : ℕ), p ^ j = n
Tactic: contrapose! hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
hn : ∃ (a : ℕ), p ^ a = p ^ i * n
⊢ ∃ (j : ℕ), p ^ j = n
have neg : ∀ (j : ℕ) (hj : p ^ j = p ^ i * n), ∃ (j : ℕ), p ^ j = n
Tactic: obtain ⟨j, hj⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
j : ℕ
hj : p ^ j = p ^ i * n
⊢ ∃ (j : ℕ), p ^ j = n
have neg : ∀ (v : ℕ) (hmn : (p ^ i).Coprime (p ^ v)) (hj : p ^ j = p ^ i * p ^ v), ∃ (j : ℕ), p ^ j = p ^ v
Tactic: obtain ⟨v, -, rfl⟩ := (Nat.dvd_prime_pow hp).mp (Dvd.intro_left _ hj.symm)
Cleared hypotheses: n, hmn, hj
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hm : ¬∃ (i : ℕ), p ^ i = m
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (m * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          m :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)
have neg : Function.extend (fun (x : ℕ) ↦ p ^ x)
    (fun (x : ℕ) ↦
      (PowerSeries.coeff x : (a : PowerSeries R) → R)
        (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
    0 (m * n) =
  HMul.hMul (α := R)
    (Function.extend (fun (x : ℕ) ↦ p ^ x)
      (fun (x : ℕ) ↦
        (PowerSeries.coeff x : (a : PowerSeries R) → R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
      0 m)
    (Function.extend (fun (x : ℕ) ↦ p ^ x)
      (fun (x : ℕ) ↦
        (PowerSeries.coeff x : (a : PowerSeries R) → R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
      0 n)
Tactic: simp_rw [ofPowerSeries_apply hp.one_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hm : ¬∃ (i : ℕ), p ^ i = m
⊢ Function.extend (fun (x : ℕ) ↦ p ^ x)
      (fun (x : ℕ) ↦
        (PowerSeries.coeff x : (a : PowerSeries R) → R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
      0 (m * n) =
    HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 m)
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 n)
have neg : ¬∃ (a : ℕ), p ^ a = m * n
Tactic: rw [Function.extend_apply', Function.extend_apply' _ _ _ hm,
      Pi.zero_apply, Pi.zero_apply, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hm : ¬∃ (i : ℕ), p ^ i = m
⊢ ¬∃ (a : ℕ), p ^ a = m * n
have neg : ∀ (hm : ∃ (a : ℕ), p ^ a = m * n), ∃ (i : ℕ), p ^ i = m
Tactic: contrapose! hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hm : ∃ (a : ℕ), p ^ a = m * n
⊢ ∃ (i : ℕ), p ^ i = m
have neg : ∀ (i : ℕ) (hi : p ^ i = m * n), ∃ (i : ℕ), p ^ i = m
Tactic: obtain ⟨i, hi⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hi : p ^ i = m * n
⊢ ∃ (i : ℕ), p ^ i = m
have neg : ∀ (j : ℕ) (hmn : (p ^ j).Coprime n) (hi : p ^ i = p ^ j * n), ∃ (i : ℕ), p ^ i = p ^ j
Tactic: obtain ⟨j, -, rfl⟩ := (Nat.dvd_prime_pow hp).mp ⟨n, hi⟩
Cleared hypotheses: m, hmn, hi
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
F : Filter ι
g : ArithmeticFunction R
this : UniformSpace R := ⊥
⊢ Tendsto f F (nhds g) ↔ ∀ (n : ℕ), ∀ᶠ (i : ι) in F, Eq (α := R) ((f i : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
have this₁ : Topology.IsInducing.{u_2, u_2} (X := ArithmeticFunction R) (Y := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
Tactic: have : Topology.IsInducing ((↑) : ArithmeticFunction R → (ℕ → R)) := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.LFunction (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
this : UniformSpace R := ⊥
⊢ CompleteSpace.{u_2} (ArithmeticFunction R)
have apply : IsComplete.{u_2} (α := (a : ℕ) → R) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))
Tactic: apply IsUniformInducing.completeSpace ⟨rfl⟩