awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / HPow.hPow (β := ℕ) r ((q.factorization : (a : ℕ) → ℕ) r : ℕ)
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit.{u_1} (M := R) (↑a : R)
rn_cast_zero : Eq.{u_1 + 1} (α := R) (↑(r ^ n) : R) 0
q_eq_rn : q = r ^ n
⊢ IsPrimePow q
have n_pos : n ≠ 0
Tactic: have n_pos : n ≠ 0 := fun n_zero =>
      absurd (by simpa [n_zero] using q_eq_rn) (CharP.char_ne_one R q)
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_zero : r = 0
⊢ IsPrimePow q
have K_char_p_0 : CharP K 0
Tactic: haveI K_char_p_0 := ringChar.of_eq r_zero
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_zero : r = 0
K_char_p_0 : CharP K 0
⊢ IsPrimePow q
have K_char_zero : CharZero K
Tactic: haveI K_char_zero : CharZero K := CharP.charP_to_charZero K
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
⊢ IsPrimePow q
have R_char_zero : CharZero R
Tactic: haveI R_char_zero := RingHom.charZero (IsLocalRing.residue R)
-- Lean 4 proof step from Mathlib.Algebra.CharP.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := (q.factorization : (a : ℕ) → ℕ) r
r_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
R_char_zero : CharZero R
⊢ IsPrimePow q
have q_zero : q = 0
Tactic: have q_zero := CharP.eq R char_R_q (CharP.ofCharZero R)
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
⊢ (∀ p > 0, MixedCharZero R p → P) ↔ ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
have mp : (∀ p > 0, MixedCharZero R p → P) → ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
mp : (∀ p > 0, MixedCharZero R p → P) → ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ (∀ p > 0, MixedCharZero R p → P) ↔ ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
have mpr : (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → ∀ p > 0, MixedCharZero R p → P
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
⊢ P
have mpr : ∀ (I : Ideal R) (hI_ne_top : I ≠ ⊤), CharP.{u_1} (R ⧸ I) q → P
Tactic: rcases q_mixedChar.charP_quotient with ⟨I, hI_ne_top, _⟩
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) q
⊢ P
have mpr : ∀ (M : Ideal R) (hM_max : M.IsMaximal) (h_IM : I ≤ M), P
Tactic: rcases Ideal.exists_le_maximal I hI_ne_top with ⟨M, hM_max, h_IM⟩
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar.{u_1} (R ⧸ M)
⊢ r ≠ 0
have q_zero : Eq (α := R ⧸ M) ((Ideal.Quotient.factor h_IM : (a : R ⧸ I) → R ⧸ M) (↑q : R ⧸ I))
  ((Ideal.Quotient.factor h_IM : (a : R ⧸ I) → R ⧸ M) 0)
Tactic: have q_zero :=
        congr_arg (Ideal.Quotient.factor h_IM) (CharP.cast_eq_zero (R ⧸ I) q)
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar.{u_1} (R ⧸ M)
q_zero :
  Eq (α := R ⧸ M) ((Ideal.Quotient.factor h_IM : (a : R ⧸ I) → R ⧸ M) (↑q : R ⧸ I))
    ((Ideal.Quotient.factor h_IM : (a : R ⧸ I) → R ⧸ M) 0)
⊢ r ≠ 0
have q_zero₁ : Eq.{u_1 + 1} (α := R ⧸ M) (↑q : R ⧸ M) 0
Tactic: simp only [map_natCast, map_zero] at q_zero
Cleared hypotheses: q_zero
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar.{u_1} (R ⧸ M)
q_zero : Eq.{u_1 + 1} (α := R ⧸ M) (↑q : R ⧸ M) 0
⊢ r ≠ 0
have apply : r ∣ q
Tactic: apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar.{u_1} (R ⧸ M)
⊢ P
have r_pos : r ≠ 0
Tactic: have r_pos : r ≠ 0 := by
      have q_zero :=
        congr_arg (Ideal.Quotient.factor h_IM) (CharP.cast_eq_zero (R ⧸ I) q)
      simp only [map_natCast, map_zero] at q_zero
      apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)
      exact (CharP.cast_eq_zero_iff (R ⧸ M) r q).mp q_zero
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar.{u_1} (R ⧸ M)
r_pos : r ≠ 0
⊢ P
have r_prime : Nat.Prime r
Tactic: have r_prime : Nat.Prime r :=
      or_iff_not_imp_right.1 (CharP.char_is_prime_or_zero (R ⧸ M) r) r_pos
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar.{u_1} (R ⧸ M)
r_pos : r ≠ 0
r_prime : Nat.Prime r
⊢ P
have mpr : MixedCharZero R r
Tactic: apply h r r_prime
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar.{u_1} (R ⧸ M)
r_pos : r ≠ 0
r_prime : Nat.Prime r
⊢ MixedCharZero R r
have this : CharZero R
Tactic: have : CharZero R := q_mixedChar.toCharZero
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ (I : Ideal R), I ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p) ↔ ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p
have mp : (∃ (I : Ideal R), I ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p) → ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
mp : (∃ (I : Ideal R), I ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p) → ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p
⊢ (∃ (I : Ideal R), I ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p) ↔ ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p
have mpr : (∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p) → ∃ (I : Ideal R), I ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
g : ∃ (I : Ideal R), I ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p
⊢ ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p
have mp : ∀ (I : Ideal R) (hI_not_top : I ≠ ⊤), CharP.{u_1} (R ⧸ I) p → ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p
Tactic: rcases g with ⟨I, ⟨hI_not_top, _⟩⟩
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) p
⊢ ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p
have mp : ∀ (M : Ideal R) (hM_max : M.IsMaximal) (hM_ge : I ≤ M), ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p
Tactic: rcases Ideal.exists_le_maximal I hI_not_top with ⟨M, ⟨hM_max, hM_ge⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
⊢ ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p
have h : M.IsMaximal ∧ CharP.{u_1} (R ⧸ M) p
Tactic: use M
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
h : M.IsMaximal
⊢ M.IsMaximal ∧ CharP.{u_1} (R ⧸ M) p
have h₁ : CharP.{u_1} (R ⧸ M) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP.{u_1} (R ⧸ M) r
⊢ CharP.{u_1} (R ⧸ M) p
have h : p = r
Tactic: convert! hr
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP.{u_1} (R ⧸ M) r
⊢ r ∣ p
have rw : Eq.{u_1 + 1} (α := R ⧸ M) (↑p : R ⧸ M) 0
Tactic: rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP.{u_1} (R ⧸ M) r
⊢ p = r
have r_dvd_p : r ∣ p
Tactic: have r_dvd_p : r ∣ p := by
          rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
          convert! congr_arg (Ideal.Quotient.factor hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP.{u_1} (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ p = r
have h : r = p
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP.{u_1} (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ r = p
have h : ¬r = 1
Tactic: apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right : CharP.{u_1} (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
⊢ CharP.{u_1} (R ⧸ M) p
have x : ∃ (p : ℕ), CharP.{u_1} (R ⧸ M) p
Tactic: cases CharP.exists (R ⧸ M) with
      | intro r hr =>
        convert! hr
        have r_dvd_p : r ∣ p := by
          rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
          convert! congr_arg (Ideal.Quotient.factor hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)
        symm
        apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left
        exact CharP.char_ne_one (R ⧸ M) r
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_max : I.IsMaximal
h_charP : CharP.{u_1} (R ⧸ I) p
⊢ ∃ (I : Ideal R), I ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p
have h : I ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p
Tactic: use I
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ CharZero.{u_1} (R ⧸ I)
have cast_injective : Function.Injective.{1, u_1 + 1} (β := R ⧸ I) Nat.cast
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
a b : ℕ
h_ab : Eq.{u_1 + 1} (α := R ⧸ I) (↑a : R ⧸ I) (↑b : R ⧸ I)
⊢ a = b
have cast_injective : ∀ (hI : a ≠ b), I = ⊤
Tactic: contrapose! hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : Eq.{u_1 + 1} (α := R ⧸ I) (↑a : R ⧸ I) (↑b : R ⧸ I)
hI : a ≠ b
⊢ I = ⊤
have cast_injective : Membership.mem (α := R) I ((algebraMap ℚ R : (a : ℚ) → R) (HSub.hSub (α := ℚ) (↑a : ℚ) (↑b : ℚ)) : R)
Tactic: refine I.eq_top_of_isUnit_mem ?_ (IsUnit.map (algebraMap ℚ R) (IsUnit.mk0 (a - b : ℚ) ?_))
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : Eq.{u_1 + 1} (α := R ⧸ I) (↑a : R ⧸ I) (↑b : R ⧸ I)
hI : a ≠ b
cast_injective : Membership.mem (α := R) I ((algebraMap ℚ R : (a : ℚ) → R) (HSub.hSub (α := ℚ) (↑a : ℚ) (↑b : ℚ)) : R)
⊢ I = ⊤
have cast_injective₁ : HSub.hSub (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ 0
Tactic: refine I.eq_top_of_isUnit_mem ?_ (IsUnit.map (algebraMap ℚ R) (IsUnit.mk0 (a - b : ℚ) ?_))
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
n : ℕ+
⊢ IsUnit.{u_1} (M := R) (↑(↑n : ℕ) : R)
have rw : Eq (α := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}) ⊤
Tactic: rw [← Ideal.span_singleton_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
n : ℕ+
⊢ Eq (α := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}) ⊤
have apply : ¬CharZero.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}))
Tactic: apply not_imp_comm.mp (h.elim (Ideal.span {↑n}))
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
n : ℕ+
h_char_zero : CharZero.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}))
⊢ False
have apply : Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}))
  (↑(↑n : ℕ) : R ⧸ Ideal.span {(↑(↑n : ℕ) : R)}) (↑0 : R ⧸ Ideal.span {(↑(↑n : ℕ) : R)})
Tactic: apply h_char_zero.cast_injective.ne n.ne_zero
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
n : ℕ+
h_char_zero : CharZero.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}))
⊢ Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}))
    (↑(↑n : ℕ) : R ⧸ Ideal.span {(↑(↑n : ℕ) : R)}) (↑0 : R ⧸ Ideal.span {(↑(↑n : ℕ) : R)})
have rw : Membership.mem (γ := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}) (↑(↑n : ℕ) : R)
Tactic: rw [← map_natCast (Ideal.Quotient.mk _), Nat.cast_zero, Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
⊢ Eq.{u_1 + 1} (α := Rˣ) (↑1 : Rˣ) 1
have huv : Eq.{u_1 + 1} (α := R) (↑(↑1 : Rˣ) : R) (↑1 : R)
Tactic: apply Units.ext
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
⊢ Eq.{u_1 + 1} (α := R) (↑(↑1 : Rˣ) : R) (↑1 : R)
have huv : Eq.{u_1 + 1} (α := R) (↑(↑1 : Rˣ) : R) 1
Tactic: rw [Units.val_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
⊢ Eq.{u_1 + 1} (α := R) (↑(↑1 : Rˣ) : R) 1
have huv : Eq.{u_1 + 1} (α := R) (↑(IsUnit.unit (a := (↑(↑1 : ℕ) : R)) sorry) : R) 1
Tactic: change ((PNat.isUnit_natCast (R := R) 1).unit : R) = 1
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
⊢ Eq.{u_1 + 1} (α := R) (↑(IsUnit.unit (a := (↑(↑1 : ℕ) : R)) ⋯) : R) 1
have huv : Eq.{u_1 + 1} (α := R) (↑(↑1 : ℕ) : R) 1
Tactic: rw [IsUnit.unit_spec (PNat.isUnit_natCast 1)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
⊢ Eq.{u_1 + 1} (α := R) (↑(↑1 : ℕ) : R) 1
have huv : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
Tactic: rw [PNat.one_coe, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
huv : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
⊢ Eq.{u_1 + 1} (α := R) (↑(↑1 : ℕ) : R) 1
have huv₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [PNat.one_coe, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.MixedCharZero (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
n : ℕ+
⊢ Eq.{u_1 + 1} (α := R) (↑(↑n : Rˣ) : R) (↑(↑n : ℕ) : R)
have change : Eq.{u_1 + 1} (α := R) (↑(IsUnit.unit sorry) : R) (↑(↑n : ℕ) : R)
Tactic: change ((PNat.isUnit_natCast (R := R) n).unit : R) = ↑n
-- 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) /ₚ (↑(a * b).pnatDen : Rˣ) =
    HMul.hMul (α := R) ((↑a.num : R) /ₚ (↑a.pnatDen : Rˣ)) ((↑b.num : R) /ₚ (↑b.pnatDen : Rˣ))
have simp : (↑(a * b).num : R) * HMul.hMul (α := R) (↑b.den : R) (↑a.den : R) =
  HMul.hMul (α := R) (↑a.num : R) (↑b.num : R) * (↑(a * b).den : R)
Tactic: simp only [← divp_assoc, divp_mul_eq_mul_divp, divp_divp_eq_divp_mul, divp_eq_iff_mul_eq,
        pnatCast_eq_natCast, Rat.coe_pnatDen, Units.val_mul]
-- 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) =
    HMul.hMul (α := R) (↑a.num : R) (↑b.num : R) * (↑(a * b).den : R)
have trans : (↑(a * b).num : R) * HMul.hMul (α := R) (↑b.den : R) (↑a.den : R) = (↑((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ)) : R)
Tactic: trans (↑((a * b).num * a.den * b.den) : R)
-- 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 : ℚ
trans :
  (↑(a * b).num : R) * HMul.hMul (α := R) (↑b.den : R) (↑a.den : R) = (↑((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ)) : R)
⊢ (↑(a * b).num : R) * HMul.hMul (α := R) (↑b.den : R) (↑a.den : R) =
    HMul.hMul (α := R) (↑a.num : R) (↑b.num : R) * (↑(a * b).den : R)
have trans₁ : (↑((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ)) : R) = HMul.hMul (α := R) (↑a.num : R) (↑b.num : R) * (↑(a * b).den : R)
Tactic: trans (↑((a * b).num * a.den * b.den) : R)
-- 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.num : R) * (↑(a * b).den : R)
have rw : (↑(a.num * b.num * (↑(a * b).den : ℤ)) : R) = HMul.hMul (α := R) (↑a.num : R) (↑b.num : R) * (↑(a * b).den : R)
Tactic: rw [Rat.mul_num_den' a b]
-- 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) /ₚ (↑(a + b).pnatDen : Rˣ) =
    HAdd.hAdd (α := R) ((↑a.num : R) /ₚ (↑a.pnatDen : Rˣ)) ((↑b.num : R) /ₚ (↑b.pnatDen : Rˣ))
have simp : (↑(a + b).num : R) * HMul.hMul (α := R) (↑b.den : R) (↑a.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: simp only [Units.add_divp, pnatCast_eq_natCast, Rat.coe_pnatDen, divp_mul_eq_mul_divp,
        Units.divp_add, divp_divp_eq_divp_mul, divp_eq_iff_mul_eq, Units.val_mul]
-- 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) =
    (HMul.hMul (α := R) (↑a.num : R) (↑b.den : R) + HMul.hMul (α := R) (↑b.num : R) (↑a.den : R)) * (↑(a + b).den : R)
have trans : (↑(a + b).num : R) * HMul.hMul (α := R) (↑b.den : R) (↑a.den : R) = (↑((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ)) : R)
Tactic: trans (↑((a + b).num * a.den * b.den) : R)
-- 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 : ℚ
trans :
  (↑(a + b).num : R) * HMul.hMul (α := R) (↑b.den : R) (↑a.den : R) = (↑((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ)) : R)
⊢ (↑(a + b).num : R) * HMul.hMul (α := R) (↑b.den : R) (↑a.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 trans₁ : (↑((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)
Tactic: trans (↑((a + b).num * a.den * b.den) : R)