awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
a b : ℚ
⊢ (↑(a + b).num : R) * HMul.hMul (α := R) (↑b.den : R) (↑a.den : R) = (↑((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ)) : R)
have simp_rw : (↑(a + b).num : R) * HMul.hMul (α := R) (↑b.den : R) (↑a.den : R) =
  HMul.hMul (α := R) (↑(a + b).num : R) (↑a.den : R) * (↑b.den : R)
Tactic: simp_rw [Int.cast_mul, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
a b : ℚ
⊢ (↑((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ)) : R) =
    (HMul.hMul (α := R) (↑a.num : R) (↑b.den : R) + HMul.hMul (α := R) (↑b.num : R) (↑a.den : R)) * (↑(a + b).den : R)
have rw : (↑((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ)) : R) =
  (HMul.hMul (α := R) (↑a.num : R) (↑b.den : R) + HMul.hMul (α := R) (↑b.num : R) (↑a.den : R)) * (↑(a + b).den : R)
Tactic: rw [Rat.add_num_den' a b]
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharZero.{u_1} (R ⧸ I)
have suffices : CharP.{u_1} (R ⧸ I) 0
Tactic: suffices CharP (R ⧸ I) 0 from CharP.charP_to_charZero _
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP.{u_1} (R ⧸ I) (p + 1)
⊢ CharP.{u_1} (R ⧸ I) 0
have h_mixed : MixedCharZero R p.succ
Tactic: have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP.{u_1} (R ⧸ I) p
⊢ CharP.{u_1} (R ⧸ I) 0
have intro : ∀ (hp : CharP.{u_1} (R ⧸ I) 0), CharP.{u_1} (R ⧸ I) 0
Tactic: cases p with
    | zero => exact hp
    | succ p =>
      have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
      exact absurd h_mixed (h p.succ p.succ_pos)
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP.{u_1} (R ⧸ I) p
intro : ∀ (hp : CharP.{u_1} (R ⧸ I) 0), CharP.{u_1} (R ⧸ I) 0
⊢ CharP.{u_1} (R ⧸ I) 0
have intro₁ : ∀ (p : ℕ) (hp : CharP.{u_1} (R ⧸ I) (p + 1)), CharP.{u_1} (R ⧸ I) 0
Tactic: cases p with
    | zero => exact hp
    | succ p =>
      have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
      exact absurd h_mixed (h p.succ p.succ_pos)
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
⊢ CharP.{u_1} (R ⧸ I) 0
have x : ∃ (p : ℕ), CharP.{u_1} (R ⧸ I) p
Tactic: cases CharP.exists (R ⧸ I) with
  | intro p hp =>
    cases p with
    | zero => exact hp
    | succ p =>
      have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
      exact absurd h_mixed (h p.succ p.succ_pos)
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
⊢ False
have rcases : ∀ (I : Ideal R) (hI_ne_top : I ≠ ⊤) (hI_p : CharP.{u_1} (R ⧸ I) p), False
Tactic: rcases hp_mixedChar.charP_quotient with ⟨I, hI_ne_top, hI_p⟩
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hI_p : CharP.{u_1} (R ⧸ I) p
⊢ False
have hI_zero : CharP.{u_1} (R ⧸ I) 0
Tactic: replace hI_zero : CharP (R ⧸ I) 0 := @CharP.ofCharZero _ _ (h I hI_ne_top)
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
have mp : Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R) → ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
mp : Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R) → ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
⊢ Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
have mpr : (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)) → Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
h_alg : Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R)
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
have mp : ∀ (h_alg' : Algebra ℚ R) (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
Tactic: haveI h_alg' : Algebra ℚ R := h_alg.some
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
⊢ Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R)
have mpr : Algebra ℚ R
Tactic: apply Nonempty.intro
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
⊢ IsEmpty.{max (u_1 + 1) 1} (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p
have contrapose! : Nonempty.{u_1 + 1} (Algebra ℚ R) ↔ ∀ (p : ℕ) (_ : p > 0), ¬MixedCharZero R p
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
⊢ Nonempty.{u_1 + 1} (Algebra ℚ R) ↔ ∀ (p : ℕ) (_ : p > 0), ¬MixedCharZero R p
have rw : Nonempty.{u_1 + 1} (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
Tactic: rw [← EqualCharZero.iff_not_mixedCharZero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P
have pos : ∀ (h : ∃ p > 0, MixedCharZero R p), P
Tactic: by_cases h : ∃ p > 0, MixedCharZero R p
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
pos : ∀ (h : ∃ p > 0, MixedCharZero R p), P
⊢ P
have neg : ∀ (h : ¬∃ p > 0, MixedCharZero R p), P
Tactic: by_cases h : ∃ p > 0, MixedCharZero R p
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ∃ p > 0, MixedCharZero R p
⊢ P
have pos : ∀ (p : ℕ) (H : p > 0) (hp : MixedCharZero R p), P
Tactic: rcases h with ⟨p, ⟨H, hp⟩⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
H : p > 0
hp : MixedCharZero R p
⊢ P
have pos : ∀ (h_mixed : ∀ p > 0, MixedCharZero R p → P) (p : ℕ) (H : p > 0) (hp : MixedCharZero R p), P
Tactic: rw [← MixedCharZero.reduce_to_p_prime] at h_mixed
Cleared hypotheses: h_mixed, p, H, hp
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ P
have neg : Algebra ℚ R
Tactic: apply h_equal
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ Algebra ℚ R
have h₁ : Nonempty.{u_1 + 1} (Algebra ℚ R)
Tactic: rw [← isEmpty_algebraRat_iff_mixedCharZero, not_isEmpty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
⊢ P
have pos : ∀ (h : p = 0), P
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
pos : ∀ (h : p = 0), P
⊢ P
have neg : ∀ (h : ¬p = 0), P
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
h : p = 0
⊢ P
have p_charP₁ : CharP R 0
Tactic: rw [h] at p_charP
Cleared hypotheses: p_charP, h
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R 0
h : p = 0
⊢ P
have pos : ∀ (h0 : CharZero R), P
Tactic: haveI h0 : CharZero R := CharP.charP_to_charZero R
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P
have x : ∃ (p : ℕ), CharP R p
Tactic: cases CharP.exists R with
  | intro p p_charP =>
    by_cases h : p = 0
    · rw [h] at p_charP
      haveI h0 : CharZero R := CharP.charP_to_charZero R
      exact split_equalCharZero_mixedCharZero R h_equal h_mixed
    · exact h_pos p h p_charP
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P
have refine : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
Tactic: refine split_by_characteristic R ?_ h_equal h_mixed
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
⊢ P
have have : ∀ (p_prime : Nat.Prime p), P
Tactic: have p_prime : Nat.Prime p := or_iff_not_imp_right.mp (CharP.char_is_prime_or_zero R p) p_pos
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P
have refine : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
Tactic: refine split_by_characteristic R ?_ h_equal h_mixed
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
⊢ P
have have : ∀ (p_ppow : IsPrimePow p), P
Tactic: have p_ppow : IsPrimePow (p : ℕ) := or_iff_not_imp_left.mp (charP_zero_or_prime_power R p) p_pos
-- Lean 4 proof step from Mathlib.Algebra.CharP.Pi (goal)
Goal:
ι : Type u
hi : Nonempty ι
R : Type v
inst : Semiring R
p : ℕ
inst_1 : CharP R p
x : ℕ
i : ι
h : Eq.{v + 1} (α := R) (↑x : R) 0
j : ι
rw : Eq.{v + 1} (α := R) (↑x : R) 0
⊢ Eq.{v + 1} (α := R) ((Pi.evalRingHom (fun (x : ι) ↦ R) j : (a : (i : ι) → R) → R) (↑x : ι → R) : R) (0 : R)
have rw₁ : Eq.{v + 1} (α := R) 0 0
Tactic: rw [map_natCast, h]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Pi (goal)
Goal:
ι : Type u
hi : Nonempty ι
R : Type v
inst : Semiring R
p : ℕ
inst_1 : CharP R p
x : ℕ
i : ι
h : Eq (α := ι → R) (↑x : ι → R) 0
⊢ Eq.{v + 1} (α := R) (↑x : R) 0
have rw : Eq.{v + 1} (α := R) ((Pi.evalRingHom (fun (x : ι) ↦ R) i : (a : (i : ι) → R) → R) (↑x : (i : ι) → R) : R) (0 : R)
Tactic: rw [← map_natCast (Pi.evalRingHom (fun _ : ι => R) i) x, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Pi (goal)
Goal:
ι : Type u
hi : Nonempty ι
R : Type v
inst : Semiring R
p : ℕ
inst_1 : CharP R p
x : ℕ
i : ι
h : Eq (α := ι → R) (↑x : ι → R) 0
rw : Eq.{v + 1} (α := R) ((Pi.evalRingHom (fun (x : ι) ↦ R) i : (a : (i : ι) → R) → R) (↑x : (i : ι) → R) : R) (0 : R)
⊢ Eq.{v + 1} (α := R) (↑x : R) 0
have rw₁ : Eq.{v + 1} (α := R) ((Pi.evalRingHom (fun (x : ι) ↦ R) i : (a : (i : ι) → R) → R) 0 : R) (0 : R)
Tactic: rw [← map_natCast (Pi.evalRingHom (fun _ : ι => R) i) x, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Pi (goal)
Goal:
ι : Type u
hi : Nonempty ι
R : Type v
inst : Semiring R
p : ℕ
inst_1 : CharP R p
x : ℕ
i : ι
h : Eq (α := ι → R) (↑x : ι → R) 0
rw : Eq.{v + 1} (α := R) ((Pi.evalRingHom (fun (x : ι) ↦ R) i : (a : (i : ι) → R) → R) (↑x : (i : ι) → R) : R) (0 : R)
rw₁ : Eq.{v + 1} (α := R) ((Pi.evalRingHom (fun (x : ι) ↦ R) i : (a : (i : ι) → R) → R) 0 : R) (0 : R)
⊢ Eq.{v + 1} (α := R) (↑x : R) 0
have rw₂ : Eq.{v + 1} (α := R) 0 0
Tactic: rw [← map_natCast (Pi.evalRingHom (fun _ : ι => R) i) x, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Quotient (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
⊢ Eq (α := Ideal ℤ) (RingHom.ker (F := ℤ →+* R) (algebraMap ℤ R)) (Ideal.span {(↑p : ℤ)})
have h : ∀ (a : ℤ),
  Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* R) (algebraMap ℤ R)) a ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑p : ℤ)}) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.CharP.Quotient (goal)
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.{u_1 + 1} (α := R ⧸ I) (↑x : R ⧸ I) 0 ↔ p ∣ x
have rw : Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑x : R)) 0 ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
Tactic: rw [← cast_eq_zero_iff R p x, ← map_natCast (Ideal.Quotient.mk I)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Quotient (goal)
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
have refine : HSub.hSub (α := R) (↑x : R) 0 ∈ I ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
Tactic: refine Ideal.Quotient.eq.trans (?_ : ↑x - 0 ∈ I ↔ _)
-- Lean 4 proof step from Mathlib.Algebra.CharP.Quotient (goal)
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 : ℕ
⊢ HSub.hSub (α := R) (↑x : R) 0 ∈ I ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
have rw : (↑x : R) ∈ I ↔ Eq.{u_1 + 1} (α := R) (↑x : R) 0
Tactic: rw [sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Quotient (goal)
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
have refine : CharP.{u_1} (R ⧸ I) n → ∀ (x : ℕ) (hx : (↑x : R) ∈ I), Eq.{u_1 + 1} (α := R) (↑x : R) 0
Tactic: refine ⟨fun _ x hx => ?_, CharP.quotient' n I⟩
-- Lean 4 proof step from Mathlib.Algebra.CharP.Quotient (goal)
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) (↑x : R) 0
have rw : Eq.{u_1 + 1} (α := R ⧸ I) (↑x : R ⧸ I) 0
Tactic: rw [CharP.cast_eq_zero_iff R n, ← CharP.cast_eq_zero_iff (R ⧸ I) n _]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : CharP R n
I : Ideal 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))
have 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) ⊥)
Tactic: rw [CharP.quotient_iff, RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (↑(AddSubgroup.index.{u_1} (G := R) (Submodule.toAddSubgroup I)) : R ⧸ I) 0
have 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
Tactic: rw [AddSubgroup.index, Nat.card_eq]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ 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
have 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
Tactic: split_ifs with hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Quotient (goal)
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
⊢ 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
have 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
Tactic: split_ifs with hq
-- Lean 4 proof step from Mathlib.Algebra.CharP.Reduced (goal)
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)
⊢ x = y
have 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
Tactic: rw [← sub_eq_zero] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.CharP.Reduced (hypothesis)
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 = 0
have H₁ : (x - y) ^ p ^ n = 0
Tactic: simp_rw [iterateFrobenius_def, ← sub_pow_expChar_pow] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.CharP.Reduced (goal)
Goal:
R : Type u_1
inst : Finite R
inst_1 : CommRing R
inst_2 : IsReduced R
inst_3 : CharP R 2
a : R
⊢ IsSquare a
have intro : ∀ (val : Fintype R), IsSquare a
Tactic: cases nonempty_fintype R
-- Lean 4 proof step from Mathlib.Algebra.CharP.Reduced (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p k m : ℕ
inst_2 : ExpChar R p
x : R
⊢ x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
have rw : (x ^ m) ^ p ^ k = 1 ↔ x ^ m = 1
Tactic: rw [pow_mul']
-- Lean 4 proof step from Mathlib.Algebra.CharP.Reduced (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p k m : ℕ
inst_2 : ExpChar R p
x : R
⊢ (x ^ m) ^ p ^ k = 1 ↔ x ^ m = 1
have h : Eq (α := R) ((iterateFrobenius R p k : (a : R) → R) 1 : R) (1 : R)
Tactic: convert! ← (iterateFrobenius_inj R p k).eq_iff
-- Lean 4 proof step from Mathlib.Algebra.CharP.Subring (goal)
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
⊢ Eq (α := R) ((S.subtype : (a : ↥S) → R) (↑x : ↥S) : R) (0 : R)
have rw₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [map_natCast, h]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Subring (goal)
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
⊢ Eq (α := R) ((S.subtype : (a : ↥S) → R) (↑x : ↥S) : R) (0 : R)
have rw : Eq (α := R) ((S.subtype : (a : ↥S) → R) 0 : R) (0 : R)
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Subring (goal)
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)
⊢ Eq (α := R) ((S.subtype : (a : ↥S) → R) (↑x : ↥S) : R) (0 : R)
have rw₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Subring (goal)
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
⊢ Eq (α := R) ((S.subtype : (a : ↥S) → R) (↑x : ↥S) : R) (0 : R)
have rw₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [map_natCast, h]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Subring (goal)
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
⊢ Eq (α := R) ((S.subtype : (a : ↥S) → R) (↑x : ↥S) : R) (0 : R)
have rw : Eq (α := R) ((S.subtype : (a : ↥S) → R) 0 : R) (0 : R)
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Subring (goal)
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)
⊢ Eq (α := R) ((S.subtype : (a : ↥S) → R) (↑x : ↥S) : R) (0 : R)
have rw₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
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 : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ 2 ∣ n
have inl : ∀ (hn : Even n), Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ 2 ∣ n
Tactic: obtain hn | hn := Nat.even_or_odd n
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ 2 ∣ n
have inr : ∀ (hn : Odd n), Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ 2 ∣ n
Tactic: obtain hn | hn := Nat.even_or_odd n
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
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 ↔ 2 ∣ n
have inl : Eq.{u_1 + 1} (α := R) (↑n : R) 0
Tactic: simp_rw [hn.two_dvd, iff_true]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Two (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 0 ↔ 2 ∣ n
have inr : ¬Eq.{u_1 + 1} (α := R) (↑n : R) 0
Tactic: simp_rw [hn.not_two_dvd_nat, iff_false]