awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)
have h : Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
h : Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)
⊢ Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)
have h₁ : ∀ (n : ℕ), Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) (n + 1) : R) ((f : (a : ℕ) → R) (n + 1) : R)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k : ℕ
h0 : ¬k = 0
simp_rw simp_rw₁ : HPow.hPow (α := R) ((f : (a : ℕ) → R) 0 : R) k = 0
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : ℕ) ↦ HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) 0) 0
have simp_rw₂ : HPow.hPow (α := R) 0 k = 0
Tactic: simp_rw [map_zero, zero_pow h0]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
⊢ f.ppow 0 = (↑ζ : ArithmeticFunction R)
have rw : Eq.{u_1 + 1} (α := ArithmeticFunction R)
  (if h0 : Eq (α := ℕ) 0 0 then (↑ζ : ArithmeticFunction R)
    else { toFun := fun (x : ℕ) ↦ HPow.hPow (α := R) (β := ℕ) ((f : (a : ℕ) → R) x : R) 0, map_zero' := sorry } :
    ArithmeticFunction R)
  (↑ζ : ArithmeticFunction R)
Tactic: rw [ppow, dif_pos rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
rw :
  Eq.{u_1 + 1} (α := ArithmeticFunction R)
    (if h0 : Eq (α := ℕ) 0 0 then (↑ζ : ArithmeticFunction R)
      else { toFun := fun (x : ℕ) ↦ HPow.hPow (α := R) (β := ℕ) ((f : (a : ℕ) → R) x : R) 0, map_zero' := ⋯ } :
      ArithmeticFunction R)
    (↑ζ : ArithmeticFunction R)
⊢ f.ppow 0 = (↑ζ : ArithmeticFunction R)
have rw₁ : Eq.{u_1 + 1} (α := ArithmeticFunction R) ((↑ζ : ArithmeticFunction R) : ArithmeticFunction R)
  (↑ζ : ArithmeticFunction R)
Tactic: rw [ppow, dif_pos rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
⊢ f.ppow 1 = f
have h : ∀ (x : ℕ), Eq (α := R) ((f.ppow 1 : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ (f.ppow k : (a : ℕ) → R) x = HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
have rw : (if h0 : k = 0 then (↑ζ : ArithmeticFunction R)
      else { toFun := fun (x : ℕ) ↦ HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k, map_zero' := sorry } :
      (a : ℕ) → R)
    x =
  HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
Tactic: rw [ppow, dif_neg (Nat.ne_of_gt kpos), coe_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
rw :
  (if h0 : k = 0 then (↑ζ : ArithmeticFunction R)
        else { toFun := fun (x : ℕ) ↦ HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k, map_zero' := ⋯ } :
        (a : ℕ) → R)
      x =
    HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
⊢ (f.ppow k : (a : ℕ) → R) x = HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
have rw₁ : ({ toFun := fun (x : ℕ) ↦ HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k, map_zero' := sorry } : (a : ℕ) → R) x =
  HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
Tactic: rw [ppow, dif_neg (Nat.ne_of_gt kpos), coe_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
rw :
  (if h0 : k = 0 then (↑ζ : ArithmeticFunction R)
        else { toFun := fun (x : ℕ) ↦ HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k, map_zero' := ⋯ } :
        (a : ℕ) → R)
      x =
    HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
rw₁ :
  ({ toFun := fun (x : ℕ) ↦ HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k, map_zero' := ⋯ } : (a : ℕ) → R) x =
    HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
⊢ (f.ppow k : (a : ℕ) → R) x = HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
have rw₂ : HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k = HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k
Tactic: rw [ppow, dif_neg (Nat.ne_of_gt kpos), coe_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k : ℕ
⊢ f.ppow (k + 1) = f.pmul (f.ppow k)
have h : ∀ (x : ℕ), Eq (α := R) ((f.ppow (k + 1) : (a : ℕ) → R) x : R) ((f.pmul (f.ppow k) : (a : ℕ) → R) x : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ Eq (α := R) ((f.ppow (k + 1) : (a : ℕ) → R) x : R) ((f.pmul (f.ppow k) : (a : ℕ) → R) x : R)
have h : HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) =
  (f.pmul (f.ppow k) : (a : ℕ) → R) x
Tactic: rw [ppow_apply (succ_pos k), _root_.pow_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) =
    (f.pmul (f.ppow k) : (a : ℕ) → R) x
have h : HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) (β := ℕ) ((f : (a : ℕ) → R) x : R) 0) =
  (f.pmul (f.ppow 0) : (a : ℕ) → R) x
Tactic: induction k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k x : ℕ
h :
  HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) (β := ℕ) ((f : (a : ℕ) → R) x : R) 0) =
    (f.pmul (f.ppow 0) : (a : ℕ) → R) x
⊢ HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) =
    (f.pmul (f.ppow k) : (a : ℕ) → R) x
have h₁ : ∀ (n : ℕ),
  HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) n) =
      (f.pmul (f.ppow n) : (a : ℕ) → R) x →
    HMul.hMul (α := R) ((f : (a : ℕ) → R) x : R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) (n + 1)) =
      (f.pmul (f.ppow (n + 1)) : (a : ℕ) → R) x
Tactic: induction k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
⊢ f.ppow (k + 1) = (f.ppow k).pmul f
have h : ∀ (x : ℕ), Eq (α := R) ((f.ppow (k + 1) : (a : ℕ) → R) x : R) (((f.ppow k).pmul f : (a : ℕ) → R) x : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ Eq (α := R) ((f.ppow (k + 1) : (a : ℕ) → R) x : R) (((f.ppow k).pmul f : (a : ℕ) → R) x : R)
have h : HMul.hMul (β := R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) ((f : (a : ℕ) → R) x : R) =
  ((f.ppow k).pmul f : (a : ℕ) → R) x
Tactic: rw [ppow_apply (succ_pos k), _root_.pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) ((f : (a : ℕ) → R) x : R) =
    ((f.ppow k).pmul f : (a : ℕ) → R) x
have h : ∀ {kpos : LT.lt (α := ℕ) 0 0},
  HMul.hMul (β := R) (HPow.hPow (α := R) (β := ℕ) ((f : (a : ℕ) → R) x : R) 0) ((f : (a : ℕ) → R) x : R) =
    ((f.ppow 0).pmul f : (a : ℕ) → R) x
Tactic: induction k
Cleared hypotheses: k, kpos
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
h :
  ∀ {kpos : LT.lt (α := ℕ) 0 0},
    HMul.hMul (β := R) (HPow.hPow (α := R) (β := ℕ) ((f : (a : ℕ) → R) x : R) 0) ((f : (a : ℕ) → R) x : R) =
      ((f.ppow 0).pmul f : (a : ℕ) → R) x
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) k) ((f : (a : ℕ) → R) x : R) =
    ((f.ppow k).pmul f : (a : ℕ) → R) x
have h₁ : ∀ (n : ℕ),
  (∀ {kpos : 0 < n},
      HMul.hMul (β := R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) n) ((f : (a : ℕ) → R) x : R) =
        ((f.ppow n).pmul f : (a : ℕ) → R) x) →
    ∀ {kpos : 0 < n + 1},
      HMul.hMul (β := R) (HPow.hPow (α := R) ((f : (a : ℕ) → R) x : R) (n + 1)) ((f : (a : ℕ) → R) x : R) =
        ((f.ppow (n + 1)).pmul f : (a : ℕ) → R) x
Tactic: induction k
Cleared hypotheses: k, kpos
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : DivisionSemiring R
f : ArithmeticFunction R
⊢ f.pdiv (↑ζ : ArithmeticFunction R) = f
have h : ∀ (n : ℕ), Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) n : R) ((f : (a : ℕ) → R) n : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : DivisionSemiring R
f : ArithmeticFunction R
n : ℕ
⊢ Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) n : R) ((f : (a : ℕ) → R) n : R)
have h : Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : DivisionSemiring R
f : ArithmeticFunction R
n : ℕ
h : Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)
⊢ Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) n : R) ((f : (a : ℕ) → R) n : R)
have h₁ : ∀ (n : ℕ), Eq (α := R) ((f.pdiv (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) (n + 1) : R) ((f : (a : ℕ) → R) (n + 1) : R)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (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
m n : ℕ
cop : m.Coprime n
⊢ (f.pmul g : (a : ℕ) → R) (m * n) =
    HMul.hMul (α := R) (β := R) ((f.pmul g : (a : ℕ) → R) m : R) ((f.pmul g : (a : ℕ) → R) n : R)
have simp : HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R) *
    HMul.hMul (α := R) (β := R) ((g : (a : ℕ) → R) m : R) ((g : (a : ℕ) → R) n : R) =
  HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((g : (a : ℕ) → R) m : R) *
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
Tactic: simp only [pmul_apply, hf.map_mul_of_coprime cop, hg.map_mul_of_coprime cop]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ (f.pdiv g : (a : ℕ) → R) (m * n) =
    HMul.hMul (α := R) (β := R) ((f.pdiv g : (a : ℕ) → R) m : R) ((f.pdiv g : (a : ℕ) → R) n : R)
have simp : HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R) *
    HMul.hMul (α := R) (β := R) (((g : (a : ℕ) → R) m)⁻¹ : R) (((g : (a : ℕ) → R) n)⁻¹ : R) =
  HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) (((g : (a : ℕ) → R) m)⁻¹ : R) *
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) (((g : (a : ℕ) → R) n)⁻¹ : R)
Tactic: simp only [pdiv_apply, map_mul_of_coprime hf cop, map_mul_of_coprime hg cop, div_eq_mul_inv,
      mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
k : ℕ
hi : IsMultiplicative.{u_1} (R := R) (f.ppow k)
⊢ IsMultiplicative.{u_1} (R := R) (f.ppow (k + 1))
have succ : IsMultiplicative.{u_1} (R := R) (f.pmul (f.ppow k))
Tactic: rw [ppow_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
k : ℕ
⊢ IsMultiplicative.{u_1} (R := R) (f.ppow k)
have zero : IsMultiplicative.{u_1} (R := R) (f.ppow 0)
Tactic: induction k with
  | zero => exact isMultiplicative_zeta.natCast
  | succ k hi => rw [ppow_succ']; apply hf.pmul hi
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
k : ℕ
zero : IsMultiplicative.{u_1} (R := R) (f.ppow 0)
⊢ IsMultiplicative.{u_1} (R := R) (f.ppow k)
have succ : ∀ (k : ℕ) (hi : IsMultiplicative.{u_1} (R := R) (f.ppow k)), IsMultiplicative.{u_1} (R := R) (f.ppow (k + 1))
Tactic: induction k with
  | zero => exact isMultiplicative_zeta.natCast
  | succ k hi => rw [ppow_succ']; apply hf.pmul hi
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
⊢ HPow.hPow (α := R) (↑p : R) (HAdd.hAdd (α := ℕ) 0 1) ∣ a ^ HPow.hPow (β := ℕ) p 0 - b ^ HPow.hPow (β := ℕ) p 0
have zero : (↑p : R) ∣ a ^ HPow.hPow (β := ℕ) p 0 - b ^ HPow.hPow (β := ℕ) p 0
Tactic: rwa [pow_one, pow_zero, pow_one, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
zero : (↑p : R) ∣ a ^ HPow.hPow (β := ℕ) p 0 - b ^ HPow.hPow (β := ℕ) p 0
⊢ HPow.hPow (α := R) (↑p : R) (HAdd.hAdd (α := ℕ) 0 1) ∣ a ^ HPow.hPow (β := ℕ) p 0 - b ^ HPow.hPow (β := ℕ) p 0
have zero₁ : (↑p : R) ∣ HPow.hPow (β := ℕ) a 1 - HPow.hPow (β := ℕ) b 1
Tactic: rwa [pow_one, pow_zero, pow_one, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
zero : (↑p : R) ∣ a ^ HPow.hPow (β := ℕ) p 0 - b ^ HPow.hPow (β := ℕ) p 0
zero₁ : (↑p : R) ∣ HPow.hPow (β := ℕ) a 1 - HPow.hPow (β := ℕ) b 1
⊢ HPow.hPow (α := R) (↑p : R) (HAdd.hAdd (α := ℕ) 0 1) ∣ a ^ HPow.hPow (β := ℕ) p 0 - b ^ HPow.hPow (β := ℕ) p 0
have zero₂ : (↑p : R) ∣ a - HPow.hPow (β := ℕ) b 1
Tactic: rwa [pow_one, pow_zero, pow_one, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
⊢ HPow.hPow (α := R) (↑p : R) (k + 1 + 1) ∣ a ^ p ^ (k + 1) - b ^ p ^ (k + 1)
have succ : (↑p : R) * HPow.hPow (α := R) (↑p : R) (k + 1) ∣
  (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)) * (a ^ p ^ k - b ^ p ^ k)
Tactic: rw [pow_succ p k, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
⊢ (↑p : R) * HPow.hPow (α := R) (↑p : R) (k + 1) ∣
    (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)) * (a ^ p ^ k - b ^ p ^ k)
have succ : Dvd.dvd.{u_1} (α := R) (↑p : R) (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i))
Tactic: refine mul_dvd_mul ?_ ih
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
r : R
⊢ (↑p : R) ∣ r ↔
    Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
      ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
      (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
have rw : (↑p : R) ∣ r ↔ Membership.mem (γ := Ideal R) (span {(↑p : R)}) r
Tactic: rw [eq_zero_iff_mem, mem_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
r : R
rw : (↑p : R) ∣ r ↔ Membership.mem (γ := Ideal R) (span {(↑p : R)}) r
⊢ (↑p : R) ∣ r ↔
    Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
      ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
      (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
have rw₁ : (↑p : R) ∣ r ↔ (↑p : R) ∣ r
Tactic: rw [eq_zero_iff_mem, mem_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
⊢ Dvd.dvd.{u_1} (α := R) (↑p : R) (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i))
have hf : ∀ (r : R),
  (↑p : R) ∣ r ↔
    Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
      ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
      (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
Tactic: have hf : ∀ r : R, (p : R) ∣ r ↔ f r = 0 := fun r ↦ by rw [eq_zero_iff_mem, mem_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
hf :
  ∀ (r : R),
    (↑p : R) ∣ r ↔
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
⊢ Dvd.dvd.{u_1} (α := R) (↑p : R) (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i))
have h₁ : Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
  ((f : (a : R) → R ⧸ span {(↑p : R)}) a : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
  ((f : (a : R) → R ⧸ span {(↑p : R)}) b : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
Tactic: rw [hf, map_sub, sub_eq_zero] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
h :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) a : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) b : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
hf :
  ∀ (r : R),
    (↑p : R) ∣ r ↔
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
⊢ Dvd.dvd.{u_1} (α := R) (↑p : R) (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i))
have succ : Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)})) (↑p : R ⧸ span {(↑p : R)}) 0
Tactic: rw [hf, RingHom.map_geom_sum₂, map_pow, map_pow, h, geom_sum₂_self, mul_eq_zero_of_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
h :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) a : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) b : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
hf :
  ∀ (r : R),
    (↑p : R) ∣ r ↔
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
⊢ Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)})) (↑p : R ⧸ span {(↑p : R)}) 0
have succ : Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)})) ((f : (a : R) → R ⧸ span {(↑p : R)}) (↑p : R)) 0
Tactic: rw [← map_natCast f, eq_zero_iff_mem, mem_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
h :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) a : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) b : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
hf :
  ∀ (r : R),
    (↑p : R) ∣ r ↔
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
succ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)})) ((f : (a : R) → R ⧸ span {(↑p : R)}) (↑p : R)) 0
⊢ Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)})) (↑p : R ⧸ span {(↑p : R)}) 0
have succ₁ : Membership.mem (γ := Ideal R) (span {(↑p : R)}) (↑p : R)
Tactic: rw [← map_natCast f, eq_zero_iff_mem, mem_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
h :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) a : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) b : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
hf :
  ∀ (r : R),
    (↑p : R) ∣ r ↔
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
succ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)})) ((f : (a : R) → R ⧸ span {(↑p : R)}) (↑p : R)) 0
succ₁ : Membership.mem (γ := Ideal R) (span {(↑p : R)}) (↑p : R)
⊢ Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)})) (↑p : R ⧸ span {(↑p : R)}) 0
have succ₂ : Dvd.dvd.{u_1} (α := R) (↑p : R) (↑p : R)
Tactic: rw [← map_natCast f, eq_zero_iff_mem, mem_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
⊢ HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
have zero : HPow.hPow (α := R) (↑p : R) (HAdd.hAdd (α := ℕ) 0 1) ∣ a ^ HPow.hPow (β := ℕ) p 0 - b ^ HPow.hPow (β := ℕ) p 0
Tactic: induction k with
  | zero => rwa [pow_one, pow_zero, pow_one, pow_one]
  | succ k ih =>
    rw [pow_succ p k, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ']
    refine mul_dvd_mul ?_ ih
    let f : R →+* R ⧸ span {(p : R)} := mk (span {(p : R)})
    have hf : ∀ r : R, (p : R) ∣ r ↔ f r = 0 := fun r ↦ by rw [eq_zero_iff_mem, mem_span_singleton]
    rw [hf, map_sub, sub_eq_zero] at h
    rw [hf, RingHom.map_geom_sum₂, map_pow, map_pow, h, geom_sum₂_self, mul_eq_zero_of_left]
    rw [← map_natCast f, eq_zero_iff_mem, mem_span_singleton]
Cleared hypotheses: k