awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
⊢ HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (W_ R n)
        (∑ x ∈ range n,
          (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
            (HMul.hMul (α := MvPolynomial ℕ R)
              ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
              (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x))))))
      ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R) =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
have ind : HSub.hSub (α := MvPolynomial ℕ R) (W_ R n)
    (∑ x ∈ range n,
      (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
        (HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x))))) =
  HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
    ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
⊢ HSub.hSub (α := MvPolynomial ℕ R) (W_ R n)
      (∑ x ∈ range n,
        (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          (HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x))))) =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)
have ind : Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
  (∑ x ∈ range n,
    HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X x) (p ^ (n - x))))
  (∑ x ∈ range n,
    (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x)))))
Tactic: rw [wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ_comm,
    tsub_self, pow_zero, pow_one, mul_comm (X n), add_sub_assoc, add_eq_left, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
⊢ Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
    (∑ x ∈ range n,
      HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (X x) (p ^ (n - x))))
    (∑ x ∈ range n,
      (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
        (HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x)))))
have ind : ∀ x ∈ range n,
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X x) (p ^ (n - x))) =
    (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x))))
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
i : ℕ
h : i ∈ range n
⊢ HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
have h₁ : i < n
Tactic: rw [mem_range] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
i : ℕ
h : i < n
⊢ HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
have ind : HMul.hMul (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
    (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
  HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
    ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
      MvPolynomial ℕ R)
    ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))) :
      MvPolynomial ℕ R)
Tactic: rw [map_mul, map_pow (bind₁ _), algHom_C, H i h, algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
i : ℕ
h : i < n
ind :
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
        MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))) :
        MvPolynomial ℕ R)
⊢ HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
have ind₁ : HMul.hMul (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
    (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
  HMul.hMul (α := MvPolynomial ℕ R)
    ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
      MvPolynomial ℕ R)
    (HPow.hPow (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R i) : MvPolynomial ℕ R) (p ^ (n - i)))
Tactic: rw [map_mul, map_pow (bind₁ _), algHom_C, H i h, algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
i : ℕ
h : i < n
ind :
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
        MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))) :
        MvPolynomial ℕ R)
ind₁ :
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
        MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R)
        ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R i) : MvPolynomial ℕ R)
        (p ^ (n - i)))
⊢ HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
have ind₂ : HMul.hMul (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
    (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
  HMul.hMul (α := MvPolynomial ℕ R)
    ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
    (HPow.hPow (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R i) : MvPolynomial ℕ R) (p ^ (n - i)))
Tactic: rw [map_mul, map_pow (bind₁ _), algHom_C, H i h, algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
i : ℕ
h : i < n
ind :
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
        MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))) :
        MvPolynomial ℕ R)
ind₁ :
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i)) :
        MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R)
        ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R i) : MvPolynomial ℕ R)
        (p ^ (n - i)))
ind₂ :
  HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial ℕ R)
      ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) :
        MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R)
        ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R i) : MvPolynomial ℕ R)
        (p ^ (n - i)))
⊢ HMul.hMul (α := MvPolynomial ℕ R)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
      (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
    (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
        (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (n - i))))
have ind₃ : HMul.hMul (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
    (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i))) =
  HMul.hMul (α := MvPolynomial ℕ R)
    ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
    (HPow.hPow (α := MvPolynomial ℕ R) (X i) (p ^ (n - i)))
Tactic: rw [map_mul, map_pow (bind₁ _), algHom_C, H i h, algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.Torsion (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := Subgroup (ZMod p)ˣ) (rootsOfUnity (p - 1) (ZMod p)) ⊤
have h : ∀ (x : (ZMod p)ˣ),
  Membership.mem (γ := Subgroup (ZMod p)ˣ) (rootsOfUnity (p - 1) (ZMod p)) x ↔
    Membership.mem (γ := Subgroup (ZMod p)ˣ) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.Torsion (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ p - 1 ≠ 0
have this : 2 ≤ p
Tactic: have : 2 ≤ p := Nat.Prime.two_le Fact.out
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.Torsion (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ HasEnoughRootsOfUnity (ZMod p) (p - 1)
have this : NeZero (p - 1)
Tactic: have : NeZero (p - 1) := ⟨by have : 2 ≤ p := Nat.Prime.two_le Fact.out; grind⟩
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.Torsion (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : NeZero (p - 1)
⊢ HasEnoughRootsOfUnity (ZMod p) (p - 1)
have refine : p - 1 ≤ Fintype.card ↥(rootsOfUnity (p - 1) (ZMod p))
Tactic: refine HasEnoughRootsOfUnity.of_card_le ?_
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.Torsion (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : NeZero (p - 1)
⊢ p - 1 ≤ Fintype.card ↥(rootsOfUnity (p - 1) (ZMod p))
have this₁ : Nat.card ↥(rootsOfUnity (p - 1) (ZMod p)) = Nat.card ↥⊤
Tactic: have := Nat.card_congr (MulEquiv.subgroupCongr (ZMod.rootsOfUnity_eq_top (p := p))).toEquiv
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.Torsion (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this_1 : NeZero (p - 1)
this : Nat.card ↥(rootsOfUnity (p - 1) (ZMod p)) = Nat.card ↥⊤
⊢ p - 1 ≤ Fintype.card ↥(rootsOfUnity (p - 1) (ZMod p))
have this₁ : Fintype.card ↥(rootsOfUnity (p - 1) (ZMod p)) = Nat.card ↥⊤
Tactic: rw [Nat.card_eq_fintype_card] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.Torsion (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this_1 : NeZero (p - 1)
this : Fintype.card ↥(rootsOfUnity (p - 1) (ZMod p)) = Nat.card ↥⊤
⊢ p - 1 ≤ Fintype.card ↥(rootsOfUnity (p - 1) (ZMod p))
have rw : p - 1 ≤ Nat.card ↥⊤
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
⊢ IsCyclic (ZMod 4)ˣ
have apply : Nat.card (ZMod 4)ˣ = 2
Tactic: apply isCyclic_of_prime_card (p := 2)
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
⊢ Nat.card (ZMod 4)ˣ = 2
have simp : φ 4 = 2
Tactic: simp only [Nat.card_eq_fintype_card, card_units_eq_totient]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
⊢ ¬IsCyclic (ZMod 8)ˣ
have rw : ¬Monoid.exponent (ZMod 8)ˣ = φ 8
Tactic: rw [IsCyclic.iff_exponent_eq_card, Nat.card_eq_fintype_card, card_units_eq_totient]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (hypothesis)
Goal:
⊢ ¬Monoid.exponent (ZMod 8)ˣ = φ 8
have h : Monoid.exponent (ZMod 8)ˣ ∣ 2
Tactic: have h : Monoid.exponent (ZMod 8)ˣ ∣ 2 := Monoid.exponent_dvd_of_forall_pow_eq_one (by decide)
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
⊢ ∃ (y : R), (1 + u * x) ^ p = 1 + (↑p : R) * u * (x + v * y)
have rw : ∃ (y : R),
  ∑ m ∈ Finset.range (p + 1), (u * x) ^ m * HPow.hPow (α := R) 1 (p - m) * (↑(p.choose m) : R) =
    1 + (↑p : R) * u * (x + v * y)
Tactic: rw [add_comm, add_pow]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
⊢ ∃ (y : R),
    ∑ m ∈ Finset.range (p + 1), (u * x) ^ m * HPow.hPow (α := R) 1 (p - m) * (↑(p.choose m) : R) =
      1 + (↑p : R) * u * (x + v * y)
have rw : ∃ (y : R),
  HPow.hPow (β := ℕ) (u * x) 0 * HPow.hPow (α := R) 1 (p - 0) * (↑(p.choose 0) : R) +
      ∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * HPow.hPow (α := R) 1 (p - x_1) * (↑(p.choose x_1) : R) =
    1 + (↑p : R) * u * (x + v * y)
Tactic: rw [← Finset.add_sum_erase (a := 0) _ _ (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
⊢ ∃ (y : R),
    HPow.hPow (β := ℕ) (u * x) 0 * HPow.hPow (α := R) 1 (p - 0) * (↑(p.choose 0) : R) +
        ∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * HPow.hPow (α := R) 1 (p - x_1) * (↑(p.choose x_1) : R) =
      1 + (↑p : R) * u * (x + v * y)
have simp_rw : ∃ (y : R),
  HAdd.hAdd (α := R) 1 (∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * (↑(p.choose x_1) : R)) =
    1 + (↑p : R) * u * (x + v * y)
Tactic: simp_rw [one_pow, pow_zero, Nat.choose_zero_right, Nat.cast_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
⊢ ∃ (y : R),
    HAdd.hAdd (α := R) 1 (∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * (↑(p.choose x_1) : R)) =
      1 + (↑p : R) * u * (x + v * y)
have rw : ∃ (y : R),
  1 +
      (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
        ∑ x_1 ∈ ((Finset.range (p + 1)).erase 0).erase 1, (u * x) ^ x_1 * (↑(p.choose x_1) : R)) =
    1 + (↑p : R) * u * (x + v * y)
Tactic: rw [← Finset.add_sum_erase (a := 1) _ _ (by simp [hp.pos])]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
⊢ p ∈ ((Finset.range (p + 1)).erase 0).erase 1
have simp : p ≠ 1 ∧ p ≠ 0 ∧ p ∈ Finset.range (p + 1)
Tactic: simp only [Finset.mem_erase]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
⊢ p ≠ 1 ∧ p ≠ 0 ∧ p ∈ Finset.range (p + 1)
have rw : 2 ≤ p ∧ p ∈ Finset.range (p + 1)
Tactic: rw [← and_assoc, and_comm (a := ¬ _), ← Nat.two_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
⊢ ∃ (y : R),
    1 +
        (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
          ∑ x_1 ∈ ((Finset.range (p + 1)).erase 0).erase 1, (u * x) ^ x_1 * (↑(p.choose x_1) : R)) =
      1 + (↑p : R) * u * (x + v * y)
have rw : ∃ (y : R),
  1 +
      (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
        (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
          (u * x) ^ p * (↑(p.choose p) : R))) =
    1 + (↑p : R) * u * (x + v * y)
Tactic: rw [← Finset.sum_erase_add (a := p) _ _ (by -- aesop works but is slow
      simp only [Finset.mem_erase]
      rw [← and_assoc, and_comm (a := ¬ _), ← Nat.two_le_iff]
      simp [hp.two_le])]
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : (↑p : R) * u * v ∣ u ^ p
x : R
⊢ ∃ (y : R),
    1 +
        (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
          (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
            (u * x) ^ p * (↑(p.choose p) : R))) =
      1 + (↑p : R) * u * (x + v * y)
have obtain : ∀ (a : R) (ha : u = v * a),
  ∃ (y : R),
    1 +
        (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
          (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
            (u * x) ^ p * (↑(p.choose p) : R))) =
      1 + (↑p : R) * u * (x + v * y)
Tactic: obtain ⟨a, ha⟩ := hvu
Cleared hypotheses: hvu
-- Lean 4 proof step from Mathlib.RingTheory.ZMod.UnitsCyclic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hpuv : (↑p : R) * u * v ∣ u ^ p
x a : R
ha : u = v * a
⊢ ∃ (y : R),
    1 +
        (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
          (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
            (u * x) ^ p * (↑(p.choose p) : R))) =
      1 + (↑p : R) * u * (x + v * y)
have obtain : ∀ (b : R) (hb : u ^ p = (↑p : R) * u * v * b),
  ∃ (y : R),
    1 +
        (HPow.hPow (β := ℕ) (u * x) 1 * (↑(p.choose 1) : R) +
          (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * (↑(p.choose x_1) : R) +
            (u * x) ^ p * (↑(p.choose p) : R))) =
      1 + (↑p : R) * u * (x + v * y)
Tactic: obtain ⟨b, hb⟩ := hpuv
Cleared hypotheses: hpuv