awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p m n : ℕ
inst_1 : ExpChar R p
x : R
simp_rw : x ^ p ^ (m + n) = (x ^ p ^ n) ^ p ^ m
simp_rw₁ : x ^ p ^ (n + m) = (x ^ p ^ n) ^ p ^ m
simp_rw₂ : x ^ (p ^ n * p ^ m) = (x ^ p ^ n) ^ p ^ m
⊢ Eq (α := R) ((iterateFrobenius R p (m + n) : (a : R) → R) x : R)
    ((iterateFrobenius R p m : (a : R) → R) ((iterateFrobenius R p n : (a : R) → R) x : R) : R)

Tactic:
simp_rw [iterateFrobenius_def, add_comm m n, pow_add, pow_mul]

Premises used: pow_add, add_comm, pow_mul, iterateFrobenius_def
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p m n : ℕ
inst_1 : ExpChar R p
⊢ Eq (α := R →+* R) (iterateFrobenius R p (m + n)) (RingHom.comp (iterateFrobenius R p m) (iterateFrobenius R p n))

Tactic:
RingHom.ext (iterateFrobenius_add_apply R p m n)

Premises used: RingHom.ext, iterateFrobenius_add_apply
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p m n : ℕ
inst_1 : ExpChar R p
x : R
simp_rw : (⇑(frobenius R p) : (a : R) → R)^[m * n] x = (⇑(frobenius R p) : (a : R) → R)^[m]^[n] x
⊢ (iterateFrobenius R p (m * n) : (a : R) → R) x = (⇑(iterateFrobenius R p m) : (a : R) → R)^[n] x

Tactic:
simp_rw [coe_iterateFrobenius, Function.iterate_mul]

Premises used: coe_iterateFrobenius, Function.iterate_mul
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
p m n : ℕ
inst_1 : ExpChar R p
⊢ Eq (α := (a : R) → R) (⇑(iterateFrobenius R p (m * n)) : (a : R) → R) (⇑(iterateFrobenius R p m) : (a : R) → R)^[n]

Tactic:
funext (iterateFrobenius_mul_apply R p m n)

Premises used: funext, iterateFrobenius_mul_apply
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →* S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x : R
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((frobenius R p : (a : R) → R) x : R) : S)
    ((frobenius S p : (a : S) → S) ((f : (a : R) → S) x : S) : S)

Tactic:
map_pow f x p

Premises used: map_pow
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
g : R →+* S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x : R
⊢ Eq.{u_2 + 1} (α := S) ((g : (a : R) → S) ((frobenius R p : (a : R) → R) x : R) : S)
    ((frobenius S p : (a : S) → S) ((g : (a : R) → S) x : S) : S)

Tactic:
map_pow g x p

Premises used: map_pow
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →* S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x : R
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((⇑(frobenius R p) : (a : R) → R)^[n] x) : S)
    ((⇑(frobenius S p) : (a : S) → S)^[n] ((f : (a : R) → S) x) : S)

Tactic:
Function.Semiconj.iterate_right (f.map_frobenius p) n x

Premises used: Function.Semiconj.iterate_right, MonoidHom.map_frobenius
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →* S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x : R
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((iterateFrobenius R p n : (a : R) → R) x : R) : S)
    ((iterateFrobenius S p n : (a : S) → S) ((f : (a : R) → S) x : S) : S)

Tactic:
simp [iterateFrobenius_def]

Premises used: iterateFrobenius_def
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
g : R →+* S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x : R
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) ((g : (a : R) → S) ((⇑(frobenius R p) : (a : R) → R)^[n] x) : S)
    ((⇑(frobenius S p) : (a : S) → S)^[n] ((g : (a : R) → S) x) : S)

Tactic:
g.toMonoidHom.map_iterate_frobenius p x n

Premises used: MonoidHom.map_iterate_frobenius, RingHom.toMonoidHom
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
g : R →+* S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x : R
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) ((g : (a : R) → S) ((iterateFrobenius R p n : (a : R) → R) x : R) : S)
    ((iterateFrobenius S p n : (a : S) → S) ((g : (a : R) → S) x : S) : S)

Tactic:
g.toMonoidHom.map_iterateFrobenius p x n

Premises used: MonoidHom.map_iterateFrobenius, RingHom.toMonoidHom
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
x : R
f : R →* R
p : ℕ
inst_1 : ExpChar R p
n : ℕ
⊢ Eq (α := R) ((⇑f : (a : R) → R)^[n] ((frobenius R p : (a : R) → R) x) : R)
    ((frobenius R p : (a : R) → R) ((⇑f : (a : R) → R)^[n] x) : R)

Tactic:
iterate_map_pow f _ _ _

Premises used: iterate_map_pow
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
x : R
f : R →+* R
p : ℕ
inst_1 : ExpChar R p
n : ℕ
⊢ Eq (α := R) ((⇑f : (a : R) → R)^[n] ((frobenius R p : (a : R) → R) x) : R)
    ((frobenius R p : (a : R) → R) ((⇑f : (a : R) → R)^[n] x) : R)

Tactic:
iterate_map_pow f _ _ _

Premises used: iterate_map_pow
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
g : R →+* S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
⊢ g.comp (frobenius R p) = comp (frobenius S p) g

Tactic:
ext <| map_frobenius g p

Premises used: RingHom.ext, RingHom.map_frobenius
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
g : R →+* S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
n : ℕ
⊢ g.comp (iterateFrobenius R p n) = comp (iterateFrobenius S p n) g

Tactic:
ext fun x ↦ map_iterateFrobenius g p x n

Premises used: RingHom.ext, RingHom.map_iterateFrobenius
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x y : R
inst_4 : Algebra R S
r : R
s : S
simp_rw :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((_root_.frobenius R p : (a : R) → R) r : R) : S)
      ((_root_.frobenius S p : (a : S) → S) s : S) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((_root_.frobenius R p : (a : R) → R) r : R) : S)
      (OneHom.toFun (↑(↑(_root_.frobenius S p) : S →* S) : OneHom S S) s)
⊢ (_root_.frobenius S p : (a : S) → S) (r • s) =
    HSMul.hSMul (α := R) ((_root_.frobenius R p : (a : R) → R) r : R)
      (OneHom.toFun (↑(↑(_root_.frobenius S p) : S →* S) : OneHom S S) s)

Tactic:
simp_rw [Algebra.smul_def, map_mul, ← (algebraMap R S).map_frobenius]

Premises used: Algebra.algebraMap, map_mul, Algebra.smul_def, RingHom.map_frobenius
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x y : R
inst_4 : Algebra R S
r : R
s : S
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((_root_.frobenius R p : (a : R) → R) r : R) : S)
      ((_root_.frobenius S p : (a : S) → S) s : S) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((_root_.frobenius R p : (a : R) → R) r : R) : S)
      (OneHom.toFun (↑(↑(_root_.frobenius S p) : S →* S) : OneHom S S) s)

Tactic:
rfl
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f_1 : R →* S
g : R →+* S
p m n : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x y : R
inst_4 : Algebra R S
f : R
s : S
simp_rw :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (f ^ p ^ n) : S) (s ^ p ^ n) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (f ^ p ^ n) : S)
      (OneHom.toFun (↑(↑(_root_.iterateFrobenius S p n) : S →* S) : OneHom S S) s)
⊢ (_root_.iterateFrobenius S p n : (a : S) → S) (f • s) =
    HSMul.hSMul (α := R) ((_root_.iterateFrobenius R p n : (a : R) → R) f : R)
      (OneHom.toFun (↑(↑(_root_.iterateFrobenius S p n) : S →* S) : OneHom S S) s)

Tactic:
simp_rw [iterateFrobenius_def, Algebra.smul_def, mul_pow, ← map_pow]

Premises used: map_pow, iterateFrobenius_def, Algebra.smul_def, mul_pow
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f_1 : R →* S
g : R →+* S
p m n : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x y : R
inst_4 : Algebra R S
f : R
s : S
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (f ^ p ^ n) : S) (s ^ p ^ n) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (f ^ p ^ n) : S)
      (OneHom.toFun (↑(↑(_root_.iterateFrobenius S p n) : S →* S) : OneHom S S) s)

Tactic:
rfl
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
inst_4 : Algebra R S
x : S
⊢ (frobenius R S p : (a : S) → S) x = x ^ p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.CharP.Frobenius
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
inst_4 : Algebra R S
n : ℕ
x : S
⊢ (iterateFrobenius R S p n : (a : S) → S) x = x ^ p ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.CharP.IntermediateField
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
p : ℕ
inst_3 : CharZero F
⊢ CharZero.{u_2} ↥L

Tactic:
charZero_of_injective_algebraMap (algebraMap F _).injective

Premises used: Algebra.algebraMap, RingHom.injective, charZero_of_injective_algebraMap
-- Module: Mathlib.Algebra.CharP.IntermediateField
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
p : ℕ
inst_3 : CharP F p
⊢ CharP.{u_2} (↥L) p

Tactic:
charP_of_injective_algebraMap (algebraMap F _).injective p

Premises used: Algebra.algebraMap, charP_of_injective_algebraMap, RingHom.injective
-- Module: Mathlib.Algebra.CharP.IntermediateField
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
p : ℕ
inst_3 : ExpChar F p
⊢ ExpChar.{u_2} (↥L) p

Tactic:
expChar_of_injective_algebraMap (algebraMap F _).injective p

Premises used: Algebra.algebraMap, RingHom.injective, expChar_of_injective_algebraMap
-- Module: Mathlib.Algebra.CharP.IntermediateField
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
p : ℕ
inst_3 : CharP E p
⊢ CharP.{u_2} (↥L) p

Tactic:
Subfield.charP L.toSubfield p

Premises used: Set.Mem, Subfield.charP, IntermediateField.toSubfield
-- Module: Mathlib.Algebra.CharP.IntermediateField
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
p : ℕ
inst_3 : ExpChar E p
⊢ ExpChar.{u_2} (↥L) p

Tactic:
Subfield.expChar L.toSubfield p

Premises used: Set.Mem, Subfield.expChar, IntermediateField.toSubfield
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Invertible (α := R) 2
a : R
⊢ Even a

Tactic:
.of_isUnit_two (isUnit_of_invertible _) _

Premises used: isUnit_of_invertible, Even.of_isUnit_two
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
inst_1 : Invertible (α := R) 2
a : R
⊢ Odd a

Tactic:
.of_isUnit_two (isUnit_of_invertible _) _

Premises used: isUnit_of_invertible, Odd.of_isUnit_two
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
t : ℕ
inst_1 : Invertible (α := R) (↑t : R)
inst_2 : Nontrivial R
rw : Ne.{u_1 + 1} (α := R) (↑t : R) 0
⊢ ¬ringChar R ∣ t

Tactic:
rw [← ringChar.spec, ← Ne]

Premises used: Ne, ringChar.spec
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
t : ℕ
inst_1 : Invertible (α := R) (↑t : R)
inst_2 : Nontrivial R
⊢ Ne.{u_1 + 1} (α := R) (↑t : R) 0

Tactic:
Invertible.ne_zero (t : R)

Premises used: Invertible.ne_zero, Nat.cast
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
t : ℕ
inst_1 : Invertible (α := R) (↑t : R)
inst_2 : Nontrivial R
⊢ Ne.{u_1 + 1} (α := R) (↑t : R) 0

Tactic:
exact Invertible.ne_zero (t : R)

Premises used: Invertible.ne_zero, Nat.cast
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
this : Eq.{u_1 + 1} (α := R) (↑((↑n : ℤ) * n.gcdA p + (↑p : ℤ) * n.gcdB p) : R) (↑(↑(n.gcd p) : ℤ) : R)
⊢ HMul.hMul (α := R) (↑n : R) (↑(n.gcdA p) : R) = (↑(n.gcd p) : R)

Tactic:
simpa using this
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
suffices : Eq.{u_1 + 1} (α := R) (↑((↑n : ℤ) * n.gcdA p + (↑p : ℤ) * n.gcdB p) : R) (↑(↑(n.gcd p) : ℤ) : R)
⊢ HMul.hMul (α := R) (↑n : R) (↑(n.gcdA p) : R) = (↑(n.gcd p) : R)

Tactic:
suffices ↑(n * n.gcdA p + p * n.gcdB p : ℤ) = ((n.gcd p : ℤ) : R) by simpa using this
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
rw rw₁ : Eq.{u_1 + 1} (α := R) (↑(↑(n.gcd p) : ℤ) : R) (↑(↑(n.gcd p) : ℤ) : R)
⊢ Eq.{u_1 + 1} (α := R) (↑((↑n : ℤ) * n.gcdA p + (↑p : ℤ) * n.gcdB p) : R) (↑(↑(n.gcd p) : ℤ) : R)

Tactic:
rw [← Nat.gcd_eq_gcd_ab]

Premises used: Nat.gcd_eq_gcd_ab
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
⊢ HMul.hMul (α := R) (↑(n.gcdA p) : R) (↑n : R) = (↑(n.gcd p) : R)

Tactic:
Nat.commute_cast _ _ |>.eq.trans <| CharP.intCast_mul_natCast_gcdA_eq_gcd n

Premises used: Nat.commute_cast, CharP.intCast_mul_natCast_gcdA_eq_gcd, Commute.eq, Eq.trans
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
K : Type u_2
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
h : n.Coprime p
rw : Eq.{u_1 + 1} (α := R) (↑(n.gcd p) : R) 1
rw₁ : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ HMul.hMul (α := R) (↑(n.gcdA p) : R) (↑n : R) = 1

Tactic:
rw [CharP.natCast_gcdA_mul_intCast_eq_gcd, h, Nat.cast_one]

Premises used: CharP.natCast_gcdA_mul_intCast_eq_gcd, Nat.cast_one
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
K : Type u_2
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
h : n.Coprime p
rw : Eq.{u_1 + 1} (α := R) (↑(n.gcd p) : R) 1
rw₁ : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ HMul.hMul (α := R) (↑n : R) (↑(n.gcdA p) : R) = 1

Tactic:
rw [CharP.intCast_mul_natCast_gcdA_eq_gcd, h, Nat.cast_one]

Premises used: CharP.intCast_mul_natCast_gcdA_eq_gcd, Nat.cast_one
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
inst_2 : Invertible (α := R) (↑n : R)
h : n.Coprime p
this : Invertible (α := R) (↑n : R) := invertibleOfCoprime h
⊢ Eq.{u_1 + 1} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑n : R) _)
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑n : R) _)

Tactic:
(rfl : ⅟(n : R) = _)

Premises used: rfl
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
inst_2 : Invertible (α := R) (↑n : R)
h : n.Coprime p
this : Invertible (α := R) (↑n : R) := invertibleOfCoprime h
⊢ Eq.{u_1 + 1} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑n : R) _) (↑(n.gcdA p) : R)

Tactic:
convert! (rfl : ⅟(n : R) = _)

Premises used: rfl
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
hp : Nat.Prime p
h : IsUnit.{u_1} (M := R) (↑n : R)
⊢ Nontrivial R

Tactic:
have := CharP.nontrivial_of_char_ne_one (R := R) hp.ne_one
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
hp : Nat.Prime p
h : IsUnit.{u_1} (M := R) (↑n : R)
this : Nontrivial R
rw : ¬Eq.{u_1 + 1} (α := R) (↑n : R) 0
⊢ ¬p ∣ n

Tactic:
rw [← CharP.cast_eq_zero_iff (R := R)]

Premises used: CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
hp : Nat.Prime p
h : IsUnit.{u_1} (M := R) (↑n : R)
this : Nontrivial R
⊢ ¬Eq.{u_1 + 1} (α := R) (↑n : R) 0

Tactic:
h.ne_zero

Premises used: IsUnit.ne_zero
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
hp : Nat.Prime p
h : IsUnit.{u_1} (M := R) (↑n : R)
this : Nontrivial R
⊢ ¬Eq.{u_1 + 1} (α := R) (↑n : R) 0

Tactic:
exact h.ne_zero

Premises used: IsUnit.ne_zero
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
inst_2 : n.AtLeastTwo
hp : Nat.Prime p
⊢ IsUnit.{u_1} (M := R) (OfNat.ofNat n) ↔ ¬p ∣ OfNat.ofNat n

Tactic:
CharP.isUnit_natCast_iff hp

Premises used: CharP.isUnit_natCast_iff
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
z : ℤ
hp : Nat.Prime p
inl : ∀ (n : ℕ), IsUnit.{u_1} (M := R) (↑(↑n : ℤ) : R) ↔ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑n : ℤ)
inr : ∀ (n : ℕ), IsUnit.{u_1} (M := R) (↑(-(↑n : ℤ)) : R) ↔ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (-(↑n : ℤ))
⊢ IsUnit.{u_1} (M := R) (↑z : R) ↔ ¬(↑p : ℤ) ∣ z

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
hp : Nat.Prime p
n : ℕ
⊢ IsUnit.{u_1} (M := R) (↑(↑n : ℤ) : R) ↔ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑n : ℤ)

Tactic:
simp [CharP.isUnit_natCast_iff hp, Int.ofNat_dvd]

Premises used: Int.ofNat_dvd, CharP.isUnit_natCast_iff
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
hp : Nat.Prime p
n : ℕ
⊢ IsUnit.{u_1} (M := R) (↑(-(↑n : ℤ)) : R) ↔ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (-(↑n : ℤ))

Tactic:
simp [CharP.isUnit_natCast_iff hp, Int.dvd_neg, Int.ofNat_dvd]

Premises used: Int.ofNat_dvd, Int.dvd_neg, CharP.isUnit_natCast_iff
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
K : Type u_2
inst : DivisionSemiring K
inst_1 : CharZero K
⊢ Ne (α := ℕ) 2 0

Tactic:
decide
-- Module: Mathlib.Algebra.CharP.Invertible
Goal:
R : Type u_1
K : Type u_2
inst : DivisionSemiring K
inst_1 : CharZero K
⊢ Ne (α := ℕ) 3 0

Tactic:
decide
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
rw :
  Eq.{u_1 + 1} (α := R) (∑ m ∈ range (p ^ n + 1), x ^ m * y ^ (p ^ n - m) * (↑((p ^ n).choose m) : R))
    (∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R))
rw₁ :
  Eq.{u_1 + 1} (α := R) (∑ m ∈ Ico 0 (p ^ n + 1), x ^ m * y ^ (p ^ n - m) * (↑((p ^ n).choose m) : R))
    (∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R))
rw₂ rw₃ :
  Eq.{u_1 + 1} (α := R) (∑ m ∈ Icc 0 (p ^ n), x ^ m * y ^ (p ^ n - m) * (↑((p ^ n).choose m) : R))
    (∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R))
⊢ (x + y) ^ p ^ n = ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R)

Tactic:
rw [h.add_pow, ← Nat.Ico_zero_eq_range, Ico_add_one_right_eq_Icc]

Premises used: Commute.add_pow, Finset.Ico_add_one_right_eq_Icc, Nat.Ico_zero_eq_range
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
simp_rw :
  ∑ x_1 ∈ cons (p ^ n) (cons 0 (Ioo 0 (p ^ n)) ⋯) ⋯, x ^ x_1 * y ^ (p ^ n - x_1) * (↑((p ^ n).choose x_1) : R) =
    x ^ p ^ n + y ^ p ^ n + ∑ x_1 ∈ Ioo 0 (p ^ n), x ^ x_1 * y ^ (p ^ n - x_1) * (↑((p ^ n).choose x_1) : R)
⊢ ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R)

Tactic:
simp_rw [Icc_eq_cons_Ico zero_le, Ico_eq_cons_Ioo (pow_pos hp.pos _)]

Premises used: zero_le, pow_pos, Nat.Prime.pos, Finset.Icc_eq_cons_Ico, Finset.Ico_eq_cons_Ioo
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ x_1 ∈ cons (p ^ n) (cons 0 (Ioo 0 (p ^ n)) ⋯) ⋯, x ^ x_1 * y ^ (p ^ n - x_1) * (↑((p ^ n).choose x_1) : R) =
    x ^ p ^ n + y ^ p ^ n + ∑ x_1 ∈ Ioo 0 (p ^ n), x ^ x_1 * y ^ (p ^ n - x_1) * (↑((p ^ n).choose x_1) : R)

Tactic:
simp [-cons_eq_insert, add_assoc]

Premises used: add_assoc, Finset.cons_eq_insert
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
simp_rw :
  x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    x ^ p ^ n + y ^ p ^ n + ∑ i ∈ Ioo 0 (p ^ n), (↑p : R) * (x ^ i * y ^ (p ^ n - i) * (↑((p ^ n).choose i / p) : R))
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    x ^ p ^ n + y ^ p ^ n +
      HMul.hMul (α := R) (↑p : R) (∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R))

Tactic:
simp_rw [mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
h₁ :
  ∀ (k : ℕ) (hk : k ∈ Ioo 0 (p ^ n)),
    x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
      (↑p : R) * (x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R))
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    x ^ p ^ n + y ^ p ^ n + ∑ i ∈ Ioo 0 (p ^ n), (↑p : R) * (x ^ i * y ^ (p ^ n - i) * (↑((p ^ n).choose i / p) : R))

Tactic:
congr! 2 with k hk
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk : k ∈ Ioo 0 (p ^ n)
⊢ 0 < k

Tactic:
obtain ⟨hk₀, hk⟩ := mem_Ioo.1 hk

Premises used: Finset.mem_Ioo, Iff.mp
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
⊢ k < p ^ n

Tactic:
obtain ⟨hk₀, hk⟩ := mem_Ioo.1 hk

Premises used: Finset.mem_Ioo, Iff.mp
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk_1 : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
h₁ :
  x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    x ^ k * y ^ (p ^ n - k) * HMul.hMul (α := R) (↑((p ^ n).choose k / p) : R) (↑p : R)
⊢ x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    (↑p : R) * (x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R))

Tactic:
rw [Nat.cast_comm, mul_assoc (_ * _)]

Premises used: Nat.cast_comm, HMul.hMul, mul_assoc
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk_1 : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
h₁ : x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) = x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p * p) : R)
⊢ x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    x ^ k * y ^ (p ^ n - k) * HMul.hMul (α := R) (↑((p ^ n).choose k / p) : R) (↑p : R)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk_1 : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
rw : k ≠ 0
rw₁ : k ≠ p ^ n
⊢ x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) = x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p * p) : R)

Tactic:
rw [Nat.div_mul_cancel (hp.dvd_choose_pow _ _)]

Premises used: Nat.div_mul_cancel, Nat.Prime.dvd_choose_pow
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk_1 : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ 0

Tactic:
lia
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk_1 : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ p ^ n

Tactic:
lia