awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp1 : Fact (Nat.Prime p)
hp2 : (↑p : R) ∈ nonunits R
⊢ CharP.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(↑p : R)})) p

Tactic:
have hp0 : (p : R ⧸ (Ideal.span {(p : R)} : Ideal R)) = 0 :=
    map_natCast (Ideal.Quotient.mk (Ideal.span {(p : R)} : Ideal R)) p ▸
      Ideal.Quotient.eq_zero_iff_mem.2 (Ideal.subset_span <| Set.mem_singleton _)
  ringChar.of_eq <|
    Or.resolve_left ((Nat.dvd_prime hp1.1).1 <| ringChar.dvd hp0) fun h1 =>
      hp2 <|
        isUnit_iff_dvd_one.2 <|
          Ideal.mem_span_singleton.1 <|
            Ideal.Quotient.eq_zero_iff_mem.1 <|
              @Subsingleton.elim _ (@CharOne.subsingleton _ _ (ringChar.of_eq h1)) _ _

Premises used: Iff.mpr, ringChar.of_eq, Set.mem_singleton, Ideal.subset_span, ringChar.dvd, Ideal.Quotient.mk, Eq.rec, Or.resolve_left, Nat.dvd_prime, Nat.cast, Ideal.Quotient.eq_zero_iff_mem, map_natCast, Iff.mp, Ideal.span, Ideal.mem_span_singleton, Subsingleton.elim, Singleton.singleton, OfNat.ofNat, DFunLike.coe, isUnit_iff_dvd_one, Fact.out
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : CharP R p
I : Ideal R
h : ∀ (x : ℕ), (↑x : R) ∈ I → Eq.{u_1 + 1} (α := R) (↑x : R) 0
x : ℕ
rw : Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑x : R)) 0 ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (↑x : R ⧸ I) 0 ↔ p ∣ x

Tactic:
rw [← cast_eq_zero_iff R p x, ← map_natCast (Ideal.Quotient.mk I)]

Premises used: Ideal.Quotient.mk, map_natCast, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : CharP R p
I : Ideal R
h : ∀ (x : ℕ), (↑x : R) ∈ I → Eq.{u_1 + 1} (α := R) (↑x : R) 0
x : ℕ
⊢ Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑x : R)) 0 ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0

Tactic:
Ideal.Quotient.eq.trans (?_ : ↑x - 0 ∈ I ↔ _)

Premises used: Submodule.Quotient.mk, Ideal.Quotient.eq, Iff.trans
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : CharP R p
I : Ideal R
h : ∀ (x : ℕ), (↑x : R) ∈ I → Eq.{u_1 + 1} (α := R) (↑x : R) 0
x : ℕ
refine : HSub.hSub (α := R) (↑x : R) 0 ∈ I ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
⊢ Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑x : R)) 0 ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0

Tactic:
refine Ideal.Quotient.eq.trans (?_ : ↑x - 0 ∈ I ↔ _)

Premises used: Ideal.Quotient.eq, Iff.trans
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : CharP R p
I : Ideal R
h : ∀ (x : ℕ), (↑x : R) ∈ I → Eq.{u_1 + 1} (α := R) (↑x : R) 0
x : ℕ
rw : (↑x : R) ∈ I ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
⊢ HSub.hSub (α := R) (↑x : R) 0 ∈ I ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0

Tactic:
rw [sub_zero]

Premises used: sub_zero
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : CharP R p
I : Ideal R
h : ∀ (x : ℕ), (↑x : R) ∈ I → Eq.{u_1 + 1} (α := R) (↑x : R) 0
x : ℕ
⊢ (↑x : R) ∈ I ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0

Tactic:
⟨h x, fun h' => h'.symm ▸ I.zero_mem⟩

Premises used: Eq.rec, Ideal.zero_mem, Iff.intro, Eq.symm
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : CharP R p
I : Ideal R
h : ∀ (x : ℕ), (↑x : R) ∈ I → Eq.{u_1 + 1} (α := R) (↑x : R) 0
x : ℕ
⊢ (↑x : R) ∈ I ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0

Tactic:
exact ⟨h x, fun h' => h'.symm ▸ I.zero_mem⟩
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : CharP R n
I : Ideal R
⊢ CharP.{u_1} (R ⧸ I) n ↔ ∀ (x : ℕ), (↑x : R) ∈ I → Eq.{u_1 + 1} (α := R) (↑x : R) 0

Tactic:
⟨fun _ x hx => ?_, CharP.quotient' n I⟩

Premises used: CharP.quotient', Iff.intro
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : CharP R n
I : Ideal R
refine : CharP.{u_1} (R ⧸ I) n → ∀ (x : ℕ) (hx : (↑x : R) ∈ I), Eq.{u_1 + 1} (α := R) (↑x : R) 0
⊢ CharP.{u_1} (R ⧸ I) n ↔ ∀ (x : ℕ), (↑x : R) ∈ I → Eq.{u_1 + 1} (α := R) (↑x : R) 0

Tactic:
refine ⟨fun _ x hx => ?_, CharP.quotient' n I⟩
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : CharP R n
I : Ideal R
h : CharP.{u_1} (R ⧸ I) n
x : ℕ
hx : (↑x : R) ∈ I
rw : Eq.{u_1 + 1} (α := R ⧸ I) (↑x : R ⧸ I) 0
⊢ Eq.{u_1 + 1} (α := R) (↑x : R) 0

Tactic:
rw [CharP.cast_eq_zero_iff R n, ← CharP.cast_eq_zero_iff (R ⧸ I) n _]

Premises used: HasQuotient.Quotient, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : CharP R n
I : Ideal R
h : CharP.{u_1} (R ⧸ I) n
x : ℕ
hx : (↑x : R) ∈ I
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (↑x : R ⧸ I) 0

Tactic:
(Submodule.Quotient.mk_eq_zero I).mpr hx

Premises used: Iff.mpr, Submodule.Quotient.mk, RingCon.toQuotient, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : CharP R n
I : Ideal R
h : CharP.{u_1} (R ⧸ I) n
x : ℕ
hx : (↑x : R) ∈ I
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (↑x : R ⧸ I) 0

Tactic:
exact (Submodule.Quotient.mk_eq_zero I).mpr hx

Premises used: Iff.mpr, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : CharP R n
I : Ideal R
rw :
  (∀ (x : ℕ), (↑x : R) ∈ I → Eq.{u_1 + 1} (α := R) (↑x : R) 0) ↔
    LE.le (α := Ideal ℕ) (Ideal.comap (F := ℕ →+* R) (Nat.castRingHom R) I)
      (Ideal.comap (F := ℕ →+* R) (Nat.castRingHom R) ⊥)
⊢ CharP.{u_1} (R ⧸ I) n ↔
    LE.le (α := Ideal ℕ) (Ideal.comap (F := ℕ →+* R) (Nat.castRingHom R) I)
      (RingHom.ker (F := ℕ →+* R) (Nat.castRingHom R))

Tactic:
rw [CharP.quotient_iff, RingHom.ker_eq_comap_bot]

Premises used: RingHom.ker_eq_comap_bot, CharP.quotient_iff
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : CharP R n
I : Ideal R
⊢ (∀ (x : ℕ), (↑x : R) ∈ I → Eq.{u_1 + 1} (α := R) (↑x : R) 0) ↔
    LE.le (α := Ideal ℕ) (Ideal.comap (F := ℕ →+* R) (Nat.castRingHom R) I)
      (Ideal.comap (F := ℕ →+* R) (Nat.castRingHom R) ⊥)

Tactic:
rfl
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
I : Ideal R
inst_1 : CharP.{u_1} (R ⧸ I) p
⊢ Eq (α := R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) (↑p : R)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
rw :
  Eq.{u_1 + 1} (α := R ⧸ I)
    (↑(if x : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I)) then
          Fintype.card.{u_1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I))
        else 0) :
      R ⧸ I)
    0
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (↑(AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) : R ⧸ I) 0

Tactic:
rw [AddSubgroup.index, Nat.card_eq]

Premises used: AddSubgroup.index, Nat.card_eq
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
pos :
  ∀ (hq : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I))),
    Eq.{u_1 + 1} (α := R ⧸ I)
      (↑(Fintype.card.{u_1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I))) : R ⧸ I) 0
neg :
  ∀ (hq : ¬Finite.{u_1 + 1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I))),
    Eq.{u_1 + 1} (α := R ⧸ I) (↑0 : R ⧸ I) 0
⊢ Eq.{u_1 + 1} (α := R ⧸ I)
    (↑(if x : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I)) then
          Fintype.card.{u_1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I))
        else 0) :
      R ⧸ I)
    0

Tactic:
split_ifs with hq
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
hq : ¬Finite.{u_1 + 1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I))
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (↑0 : R ⧸ I) 0

Tactic:
simp
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
hq : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I))
this : Fintype (R ⧸ I) := Fintype.ofFinite (R ⧸ I)
⊢ Eq.{u_1 + 1} (α := R ⧸ I)
    (↑(Fintype.card.{u_1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I))) : R ⧸ I) 0

Tactic:
Nat.cast_card_eq_zero (R ⧸ I)

Premises used: Nat.cast_card_eq_zero, HasQuotient.Quotient, Submodule.quotientRel
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
hq : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I))
this : Fintype (R ⧸ I) := Fintype.ofFinite (R ⧸ I)
⊢ Eq.{u_1 + 1} (α := R ⧸ I)
    (↑(Fintype.card.{u_1} (HasQuotient.Quotient R (B := AddSubgroup R) (Submodule.toAddSubgroup I))) : R ⧸ I) 0

Tactic:
exact Nat.cast_card_eq_zero (R ⧸ I)

Premises used: Nat.cast_card_eq_zero, HasQuotient.Quotient
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p n : ℕ
inst_2 : ExpChar R p
x y : R
H : Eq (α := R) ((iterateFrobenius R p n : (a : R) → R) x : R) ((iterateFrobenius R p n : (a : R) → R) y : R)
rw :
  ∀
    (H :
      HSub.hSub (α := R) (β := R) ((iterateFrobenius R p n : (a : R) → R) x : R)
          ((iterateFrobenius R p n : (a : R) → R) y : R) =
        0),
    x - y = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero] at H ⊢

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p n : ℕ
inst_2 : ExpChar R p
x y : R
H :
  HSub.hSub (α := R) (β := R) ((iterateFrobenius R p n : (a : R) → R) x : R)
      ((iterateFrobenius R p n : (a : R) → R) y : R) =
    0
⊢ (x - y) ^ p ^ n = 0

Tactic:
simp_rw [iterateFrobenius_def, ← sub_pow_expChar_pow] at H

Premises used: iterateFrobenius_def, sub_pow_expChar_pow
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p n : ℕ
inst_2 : ExpChar R p
x y : R
H : (x - y) ^ p ^ n = 0
⊢ x - y = 0

Tactic:
IsReduced.eq_zero _ ⟨_, H⟩

Premises used: Exists.intro, IsReduced.eq_zero
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p n : ℕ
inst_2 : ExpChar R p
x y : R
H : (x - y) ^ p ^ n = 0
⊢ x - y = 0

Tactic:
exact IsReduced.eq_zero _ ⟨_, H⟩

Premises used: Exists.intro, IsReduced.eq_zero
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p : ℕ
inst_2 : ExpChar R p
⊢ Function.Injective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)

Tactic:
iterateFrobenius_one (R := R) p ▸ iterateFrobenius_inj R p 1

Premises used: Eq.rec, iterateFrobenius_inj, iterateFrobenius_one, OfNat.ofNat
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : Finite R
inst_1 : CommRing R
inst_2 : IsReduced R
inst_3 : CharP R 2
a : R
intro : ∀ (val : Fintype R), IsSquare a
⊢ IsSquare a

Tactic:
cases nonempty_fintype R

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : Finite R
inst_1 : CommRing R
inst_2 : IsReduced R
inst_3 : CharP R 2
a : R
val : Fintype R
⊢ IsSquare a

Tactic:
Exists.imp (fun b h => pow_two b ▸ Eq.symm h)
      (((Fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a)

Premises used: Iff.mpr, pow_two, Eq.rec, Exists.imp, Fintype.bijective_iff_injective_and_card, Function.Bijective.surjective, And.intro, IsSquare, OfNat.ofNat, Eq.symm, rfl, frobenius_inj
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : Finite R
inst_1 : CommRing R
inst_2 : IsReduced R
inst_3 : CharP R 2
a : R
val : Fintype R
⊢ IsSquare a

Tactic:
exact
    Exists.imp (fun b h => pow_two b ▸ Eq.symm h)
      (((Fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a)

Premises used: Iff.mpr, Exists.imp, Fintype.bijective_iff_injective_and_card, Function.Bijective.surjective, And.intro, OfNat.ofNat, rfl, frobenius_inj
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p k m : ℕ
inst_2 : ExpChar R p
x : R
rw : (x ^ m) ^ p ^ k = 1 ↔ x ^ m = 1
⊢ x ^ (p ^ k * m) = 1 ↔ x ^ m = 1

Tactic:
rw [pow_mul']

Premises used: pow_mul'
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p k m : ℕ
inst_2 : ExpChar R p
x : R
⊢ Eq (α := R) ((iterateFrobenius R p k : (a : R) → R) (x ^ m) : R) ((iterateFrobenius R p k : (a : R) → R) 1 : R) ↔
    x ^ m = 1

Tactic:
(iterateFrobenius_inj R p k).eq_iff

Premises used: Function.Injective.eq_iff, iterateFrobenius_inj
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p k m : ℕ
inst_2 : ExpChar R p
x : R
h : Eq (α := R) ((iterateFrobenius R p k : (a : R) → R) 1 : R) (1 : R)
⊢ (x ^ m) ^ p ^ k = 1 ↔ x ^ m = 1

Tactic:
convert! ← (iterateFrobenius_inj R p k).eq_iff

Premises used: Function.Injective.eq_iff, iterateFrobenius_inj
-- Module: Mathlib.Algebra.CharP.Reduced
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p k m : ℕ
inst_2 : ExpChar R p
x : R
⊢ Eq (α := R) ((iterateFrobenius R p k : (a : R) → R) 1 : R) (1 : R)

Tactic:
apply map_one

Premises used: map_one
-- Module: Mathlib.Algebra.CharP.Subring
Goal:
R : Type u
inst : Semiring R
p : ℕ
inst_1 : CharP R p
S : Subsemiring R
x : ℕ
h : Eq.{u + 1} (α := R) (↑x : R) 0
rw : Eq.{u + 1} (α := R) (↑x : R) 0
rw₁ rw₂ : Eq.{u + 1} (α := R) 0 0
⊢ Eq (α := R) ((S.subtype : (a : ↥S) → R) (↑x : ↥S) : R) (0 : R)

Tactic:
rw [map_natCast, h]

Premises used: map_natCast
-- Module: Mathlib.Algebra.CharP.Subring
Goal:
R : Type u
inst : Semiring R
p : ℕ
inst_1 : CharP R p
S : Subsemiring R
x : ℕ
h : Eq.{u + 1} (α := ↥S) (↑x : ↥S) 0
rw : Eq (α := R) ((S.subtype : (a : ↥S) → R) 0 : R) (0 : R)
rw₁ rw₂ : Eq.{u + 1} (α := R) 0 0
⊢ Eq (α := R) ((S.subtype : (a : ↥S) → R) (↑x : ↥S) : R) (0 : R)

Tactic:
rw [h, map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.CharP.Subring
Goal:
R : Type u
inst : Ring R
p : ℕ
inst_1 : CharP R p
S : Subring R
x : ℕ
h : Eq.{u + 1} (α := R) (↑x : R) 0
rw : Eq.{u + 1} (α := R) (↑x : R) 0
rw₁ rw₂ : Eq.{u + 1} (α := R) 0 0
⊢ Eq (α := R) ((S.subtype : (a : ↥S) → R) (↑x : ↥S) : R) (0 : R)

Tactic:
rw [map_natCast, h]

Premises used: map_natCast
-- Module: Mathlib.Algebra.CharP.Subring
Goal:
R : Type u
inst : Ring R
p : ℕ
inst_1 : CharP R p
S : Subring R
x : ℕ
h : Eq.{u + 1} (α := ↥S) (↑x : ↥S) 0
rw : Eq (α := R) ((S.subtype : (a : ↥S) → R) 0 : R) (0 : R)
rw₁ rw₂ : Eq.{u + 1} (α := R) 0 0
⊢ Eq (α := R) ((S.subtype : (a : ↥S) → R) (↑x : ↥S) : R) (0 : R)

Tactic:
rw [h, map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.CharP.Subring
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : CharP R p
S : Subring R
⊢ CharP.{u} (↥S) p

Tactic:
CharP.subring R p S

Premises used: Set.Mem, CharP.subring
-- Module: Mathlib.Algebra.CharP.Subring
Goal:
R : Type u
inst : Ring R
p : ℕ
⊢ CharP.{u} (↥(Subring.center R)) p ↔ CharP R p

Tactic:
(algebraMap (Subring.center R) R).charP_iff Subtype.val_injective p

Premises used: Algebra.algebraMap, Subtype.val_injective, Subring.center, Membership.mem, Subtype, RingHom.charP_iff
-- Module: Mathlib.Algebra.CharP.Subring
Goal:
R : Type u
inst : Ring R
p : ℕ
⊢ ExpChar.{u} (↥(Subring.center R)) p ↔ ExpChar R p

Tactic:
(algebraMap (Subring.center R) R).expChar_iff Subtype.val_injective p

Premises used: Algebra.algebraMap, Subtype.val_injective, Subring.center, RingHom.expChar_iff, Membership.mem, Subtype
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h₁ : Ne.{u_1 + 1} (α := R) 1 0
h₂ : Eq.{u_1 + 1} (α := R) 2 0
n : ℕ
inl : ∀ (hn : Even n), Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ 2 ∣ n
inr : ∀ (hn : Odd n), Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ 2 ∣ n
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ 2 ∣ n

Tactic:
obtain hn | hn := Nat.even_or_odd n

Premises used: Nat.even_or_odd
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h₁ : Ne.{u_1 + 1} (α := R) 1 0
h₂ : Eq.{u_1 + 1} (α := R) 2 0
n : ℕ
hn : Even n
inl : Eq.{u_1 + 1} (α := R) (↑n : R) 0
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ 2 ∣ n

Tactic:
simp_rw [hn.two_dvd, iff_true]

Premises used: iff_true, Even.two_dvd
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h₁ : Ne.{u_1 + 1} (α := R) 1 0
h₂ : Eq.{u_1 + 1} (α := R) 2 0
n : ℕ
hn : Even n
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0

Tactic:
natCast_eq_zero_of_even_of_two_eq_zero hn h₂

Premises used: natCast_eq_zero_of_even_of_two_eq_zero
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h₁ : Ne.{u_1 + 1} (α := R) 1 0
h₂ : Eq.{u_1 + 1} (α := R) 2 0
n : ℕ
hn : Even n
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0

Tactic:
exact natCast_eq_zero_of_even_of_two_eq_zero hn h₂

Premises used: natCast_eq_zero_of_even_of_two_eq_zero
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h₁ : Ne.{u_1 + 1} (α := R) 1 0
h₂ : Eq.{u_1 + 1} (α := R) 2 0
n : ℕ
hn : Odd n
inr : ¬Eq.{u_1 + 1} (α := R) (↑n : R) 0
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ 2 ∣ n

Tactic:
simp_rw [hn.not_two_dvd_nat, iff_false]

Premises used: iff_false, Odd.not_two_dvd_nat
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h₁ : Ne.{u_1 + 1} (α := R) 1 0
h₂ : Eq.{u_1 + 1} (α := R) 2 0
n : ℕ
hn : Odd n
inr inr₁ inr₂ inr₃ : ¬Eq.{u_1 + 1} (α := R) 1 0
⊢ ¬Eq.{u_1 + 1} (α := R) (↑n : R) 0

Tactic:
rwa [natCast_eq_one_of_odd_of_two_eq_zero hn h₂]

Premises used: natCast_eq_one_of_odd_of_two_eq_zero
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
rw : Eq.{u_1 + 1} (α := R) (↑2 : R) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) 2 0

Tactic:
rw [← Nat.cast_two, CharP.cast_eq_zero]

Premises used: CharP.cast_eq_zero, Nat.cast_two
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
n : ℕ
zero : Eq.{u_1 + 1} (α := R) (↑0 : R) (if Even (α := ℕ) 0 then 0 else 1)
succ :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R) (↑n : R) (if Even n then 0 else 1) →
      Eq.{u_1 + 1} (α := R) (↑(n + 1) : R) (if Even (n + 1) then 0 else 1)
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) (if Even n then 0 else 1)

Tactic:
induction n
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
⊢ Eq.{u_1 + 1} (α := R) (↑0 : R) (if Even (α := ℕ) 0 then 0 else 1)

Tactic:
aesop (add simp [one_add_one_eq_two])

Premises used: one_add_one_eq_two
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑n : R) (if Even n then 0 else 1)
⊢ Eq.{u_1 + 1} (α := R) (↑(n + 1) : R) (if Even (n + 1) then 0 else 1)

Tactic:
aesop (add simp [one_add_one_eq_two])

Premises used: one_add_one_eq_two
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
hp : ∃ (a : ℕ), Even a
hn : ∃ (a : ℕ), ¬Even a
⊢ Eq (α := Set R) (Set.range Nat.cast) {0, 1}

Tactic:
rw [funext natCast_eq_ite, Set.range_ite_const]

Premises used: funext, CharTwo.natCast_eq_ite, Set.range_ite_const
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
h : Even (α := ℕ) 0
⊢ ∃ (a : ℕ), Even a

Tactic:
use 0
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
⊢ Even (α := ℕ) 0

Tactic:
simp
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
h : ¬Even (α := ℕ) 1
⊢ ∃ (a : ℕ), ¬Even a

Tactic:
use 1
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
⊢ ¬Even (α := ℕ) 1

Tactic:
simp
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0 ∨ Eq.{u_1 + 1} (α := R) (↑n : R) 1

Tactic:
range_natCast.le (Set.mem_range_self _)

Premises used: Set.mem_range_self, Set.insert, Set.Mem, setOf, CharTwo.range_natCast, Eq.le, Set.singleton
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) (↑(n % 2) : R)

Tactic:
simp [natCast_eq_ite, Nat.even_iff]

Premises used: CharTwo.natCast_eq_ite, Nat.even_iff
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharP R 2
n : ℕ
inst_2 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) (OfNat.ofNat n) (↑(HMod.hMod (α := ℕ) (OfNat.ofNat n) 2) : R)

Tactic:
natCast_eq_mod n

Premises used: CharTwo.natCast_eq_mod
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
ι : Type u_2
inst : AddMonoidWithOne R
inst_1 : CharP R 2
⊢ Eq.{u_1 + 1} (α := R) 37 1

Tactic:
simp
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
x : R
rw : 2 * x = 0
rw₁ : 0 * x = 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ x + x = 0

Tactic:
rw [← two_mul x, two_eq_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, CharTwo.two_eq_zero, two_mul
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
x : R
rw : x + x = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HSMul.hSMul (α := ℕ) 2 x = 0

Tactic:
rw [two_nsmul, add_self_eq_zero]

Premises used: CharTwo.add_self_eq_zero, two_nsmul
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
a b : R
rw : a + a + b = b
rw₁ : 0 + b = b
rw₂ rw₃ : b = b
⊢ a + (a + b) = b

Tactic:
rw [← add_assoc, add_self_eq_zero, zero_add]

Premises used: add_assoc, CharTwo.add_self_eq_zero, zero_add
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Semiring R
inst_1 : CharP R 2
a b : R
rw : a + (b + b) = a
rw₁ : a + 0 = a
rw₂ rw₃ : a = a
⊢ a + b + b = a

Tactic:
rw [add_assoc, add_self_eq_zero, add_zero]

Premises used: add_assoc, CharTwo.add_self_eq_zero, add_zero
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
x : R
rw : x + x = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ -x = x

Tactic:
rw [neg_eq_iff_add_eq_zero, add_self_eq_zero]

Premises used: neg_eq_iff_add_eq_zero, CharTwo.add_self_eq_zero
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
⊢ Eq.{u_1 + 1} (α := R → R) Neg.neg id

Tactic:
funext neg_eq

Premises used: CharTwo.neg_eq, funext
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
x y : R
rw : x + -y = x + y
rw₁ rw₂ : x + y = x + y
⊢ x - y = x + y

Tactic:
rw [sub_eq_add_neg, neg_eq]

Premises used: CharTwo.neg_eq, sub_eq_add_neg
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
a b c : R
rw : a + b = c ↔ a - b = c
rw₁ rw₂ : a + b = c ↔ a + b = c
⊢ a + b = c ↔ a = c + b

Tactic:
rw [← sub_eq_iff_eq_add, sub_eq_add]

Premises used: sub_eq_iff_eq_add, CharTwo.sub_eq_add
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
a b c : R
rw : a = b + c ↔ a = b - c
rw₁ rw₂ : a = b + c ↔ a = b + c
⊢ a = b + c ↔ a + c = b

Tactic:
rw [← eq_sub_iff_add_eq, sub_eq_add]

Premises used: eq_sub_iff_add_eq, CharTwo.sub_eq_add
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
x : R
rw : x + x = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HSMul.hSMul (α := ℤ) 2 x = 0

Tactic:
rw [two_zsmul, add_self_eq_zero]

Premises used: CharTwo.add_self_eq_zero, two_zsmul
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
a b : R
rw : a - b = 0 ↔ a = b
rw₁ : a = 0 + b ↔ a = b
rw₂ rw₃ : a = b ↔ a = b
⊢ a + b = 0 ↔ a = b

Tactic:
rw [← CharTwo.sub_eq_add, sub_eq_iff_eq_add, zero_add]

Premises used: zero_add, sub_eq_iff_eq_add, CharTwo.sub_eq_add
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
n : ℤ
inl : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑(↑n : ℤ) : R) (if Even (α := ℤ) (↑n : ℤ) then 0 else 1)
inr : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (↑(-(↑n : ℤ)) : R) (if Even (α := ℤ) (-(↑n : ℤ)) then 0 else 1)
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) (if Even n then 0 else 1)

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

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Algebra.CharP.Two
Goal:
R : Type u_1
inst : Ring R
inst_1 : CharP R 2
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑(↑n : ℤ) : R) (if Even (α := ℤ) (↑n : ℤ) then 0 else 1)

Tactic:
simpa using natCast_eq_ite n

Premises used: CharTwo.natCast_eq_ite