awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)
⊢ 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)
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)
⊢ Eq.{u_1 + 1} (α := R ⧸ M) (↑q : R ⧸ M) 0

Tactic:
simp only [map_natCast, map_zero] at q_zero

Premises used: map_zero, map_natCast
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
apply : r ∣ q
⊢ r ≠ 0

Tactic:
apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)

Premises used: ne_of_gt, ne_zero_of_dvd_ne_zero
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 ∣ q

Tactic:
(CharP.cast_eq_zero_iff (R ⧸ M) r q).mp q_zero

Premises used: HasQuotient.Quotient, Iff.mp, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 ∣ q

Tactic:
exact (CharP.cast_eq_zero_iff (R ⧸ M) r q).mp q_zero

Premises used: HasQuotient.Quotient, Iff.mp, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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

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
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ 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
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
mpr : MixedCharZero R r
⊢ P

Tactic:
apply h r r_prime
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ CharZero R

Tactic:
have : CharZero R := q_mixedChar.toCharZero
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
this : CharZero R
⊢ MixedCharZero R r

Tactic:
⟨⟨M, hM_max.ne_top, ringChar.of_eq rfl⟩⟩

Premises used: ringChar.of_eq, MixedCharZero.mk, And.intro, Exists.intro, Ideal.IsMaximal.ne_top, rfl
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
this : CharZero R
⊢ MixedCharZero R r

Tactic:
exact ⟨⟨M, hM_max.ne_top, ringChar.of_eq rfl⟩⟩
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
mpr : (∃ (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 ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p) ↔ ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p

Tactic:
constructor
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
g : ∃ (I : Ideal R), I ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p
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
⊢ ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p

Tactic:
rcases g with ⟨I, ⟨hI_not_top, _⟩⟩
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
mp : ∀ (M : Ideal R) (hM_max : M.IsMaximal) (hM_ge : I ≤ M), ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p
⊢ ∃ (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⟩⟩

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 ∧ CharP.{u_1} (R ⧸ M) p
⊢ ∃ (I : Ideal R), I.IsMaximal ∧ CharP.{u_1} (R ⧸ I) p

Tactic:
use M
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
h₁ : CharP.{u_1} (R ⧸ M) p
⊢ M.IsMaximal ∧ CharP.{u_1} (R ⧸ M) p

Tactic:
constructor
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ M.IsMaximal

Tactic:
hM_max
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ M.IsMaximal

Tactic:
exact hM_max
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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) r

Tactic:
hr
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
h : p = r
⊢ CharP.{u_1} (R ⧸ M) p

Tactic:
convert! hr
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
rw : Eq.{u_1 + 1} (α := R ⧸ M) (↑p : R ⧸ M) 0
⊢ r ∣ p

Tactic:
rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]

Premises used: HasQuotient.Quotient, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ Eq (α := R ⧸ M) ((Ideal.Quotient.factor hM_ge : (a : R ⧸ I) → R ⧸ M) (↑p : R ⧸ I))
    ((Ideal.Quotient.factor hM_ge : (a : R ⧸ I) → R ⧸ M) 0)

Tactic:
congr_arg (Ideal.Quotient.factor hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)

Premises used: CharP.cast_eq_zero, congr_arg, HasQuotient.Quotient, Ideal.Quotient.factor, DFunLike.coe
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ Eq.{u_1 + 1} (α := R ⧸ M) (↑p : R ⧸ M) 0

Tactic:
convert! congr_arg (Ideal.Quotient.factor hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)

Premises used: CharP.cast_eq_zero, congr_arg, HasQuotient.Quotient, Ideal.Quotient.factor, DFunLike.coe
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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

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)
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
h : r = p
⊢ p = r

Tactic:
symm
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
h : ¬r = 1
⊢ r = p

Tactic:
apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left

Premises used: Nat.Prime.eq_one_or_self_of_dvd, Or.resolve_left
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 = 1

Tactic:
CharP.char_ne_one (R ⧸ M) r

Premises used: HasQuotient.Quotient, CharP.char_ne_one
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 = 1

Tactic:
exact CharP.char_ne_one (R ⧸ M) r

Premises used: HasQuotient.Quotient, CharP.char_ne_one
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ ∃ (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

Premises used: CharP.exists, HasQuotient.Quotient
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
h : I ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p
⊢ ∃ (I : Ideal R), I ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p

Tactic:
use I
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p

Tactic:
⟨Ideal.IsMaximal.ne_top hI_max, h_charP⟩

Premises used: And.intro, Ideal.IsMaximal.ne_top
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 ≠ ⊤ ∧ CharP.{u_1} (R ⧸ I) p

Tactic:
exact ⟨Ideal.IsMaximal.ne_top hI_max, h_charP⟩
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
cast_injective : Function.Injective.{1, u_1 + 1} (β := R ⧸ I) Nat.cast
⊢ CharZero.{u_1} (R ⧸ I)

Tactic:
constructor
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)
cast_injective : ∀ (hI : a ≠ b), I = ⊤
⊢ a = b

Tactic:
contrapose! hI
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 = ⊤

Tactic:
I.eq_top_of_isUnit_mem ?_ (IsUnit.map (algebraMap ℚ R) (IsUnit.mk0 (a - b : ℚ) ?_))

Premises used: Algebra.algebraMap, Rat, Ideal.eq_top_of_isUnit_mem, HSub.hSub, Nat.cast, IsUnit.mk0, IsUnit.map
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)
cast_injective₁ : HSub.hSub (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ 0
⊢ I = ⊤

Tactic:
refine I.eq_top_of_isUnit_mem ?_ (IsUnit.map (algebraMap ℚ R) (IsUnit.mk0 (a - b : ℚ) ?_))

Premises used: Algebra.algebraMap, Rat, Ideal.eq_top_of_isUnit_mem, HSub.hSub, Nat.cast, IsUnit.mk0, IsUnit.map
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ Membership.mem (α := R) I ((algebraMap ℚ R : (a : ℚ) → R) (HSub.hSub (α := ℚ) (↑a : ℚ) (↑b : ℚ)) : R)

Tactic:
simpa only [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero, map_natCast]

Premises used: map_sub, sub_eq_zero, Ideal.Quotient.eq_zero_iff_mem, map_natCast
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ HSub.hSub (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ 0

Tactic:
simpa only [Ne, sub_eq_zero] using (@Nat.cast_injective ℚ _ _).ne hI

Premises used: sub_eq_zero, Function.Injective.ne, Ne, Nat.cast_injective
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
n : ℕ+
rw : Eq (α := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}) ⊤
⊢ IsUnit.{u_1} (M := R) (↑(↑n : ℕ) : R)

Tactic:
rw [← Ideal.span_singleton_eq_top]

Premises used: Ideal.span_singleton_eq_top
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
n : ℕ+
apply : ¬CharZero.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}))
⊢ Eq (α := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}) ⊤

Tactic:
apply not_imp_comm.mp (h.elim (Ideal.span {↑n}))

Premises used: not_imp_comm, Fact.elim, Iff.mp, Ideal.span, Singleton.singleton
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)}))
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)})
⊢ False

Tactic:
apply h_char_zero.cast_injective.ne n.ne_zero

Premises used: PNat.ne_zero, Function.Injective.ne, CharZero.cast_injective
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)}))
rw : Membership.mem (γ := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}) (↑(↑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)})

Tactic:
rw [← map_natCast (Ideal.Quotient.mk _), Nat.cast_zero, Ideal.Quotient.eq_zero_iff_mem]

Premises used: Ideal.Quotient.mk, Ideal.Quotient.eq_zero_iff_mem, map_natCast, Nat.cast_zero
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)}))
⊢ Membership.mem (γ := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}) (↑(↑n : ℕ) : R)

Tactic:
Ideal.subset_span (Set.mem_singleton _)

Premises used: Set.mem_singleton, Ideal.subset_span, Set.Mem
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)}))
⊢ Membership.mem (γ := Ideal R) (Ideal.span {(↑(↑n : ℕ) : R)}) (↑(↑n : ℕ) : R)

Tactic:
exact Ideal.subset_span (Set.mem_singleton _)

Premises used: Set.mem_singleton, Ideal.subset_span
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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ˣ) : R) (↑1 : R)
⊢ Eq.{u_1 + 1} (α := Rˣ) (↑1 : Rˣ) 1

Tactic:
apply Units.ext

Premises used: Units.ext
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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ˣ) : R) 1
⊢ Eq.{u_1 + 1} (α := R) (↑(↑1 : Rˣ) : R) (↑1 : R)

Tactic:
rw [Units.val_one]

Premises used: Units.val_one
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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) (↑(IsUnit.unit (a := (↑(↑1 : ℕ) : R)) ⋯) : R) 1
⊢ Eq.{u_1 + 1} (α := R) (↑(↑1 : Rˣ) : R) 1

Tactic:
change ((PNat.isUnit_natCast (R := R) 1).unit : R) = 1

Premises used: Units.val, _private.0.EqualCharZero.PNat.isUnit_natCast, IsUnit.unit, OfNat.ofNat
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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) (↑(IsUnit.unit (a := (↑(↑1 : ℕ) : R)) ⋯) : R) 1

Tactic:
rw [IsUnit.unit_spec (PNat.isUnit_natCast 1)]

Premises used: _private.0.EqualCharZero.PNat.isUnit_natCast, OfNat.ofNat, IsUnit.unit_spec
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
huv₁ huv₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (↑(↑1 : ℕ) : R) 1

Tactic:
rw [PNat.one_coe, Nat.cast_one]

Premises used: PNat.one_coe, Nat.cast_one
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I))
n : ℕ+
change : Eq.{u_1 + 1} (α := R) (↑(IsUnit.unit ⋯) : R) (↑(↑n : ℕ) : R)
⊢ Eq.{u_1 + 1} (α := R) (↑(↑n : Rˣ) : R) (↑(↑n : ℕ) : R)

Tactic:
change ((PNat.isUnit_natCast (R := R) n).unit : R) = ↑n

Premises used: Units.val, _private.0.EqualCharZero.PNat.isUnit_natCast, IsUnit.unit
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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) (↑(IsUnit.unit ⋯) : R) (↑(↑n : ℕ) : R)

Tactic:
simp only [IsUnit.unit_spec]

Premises used: IsUnit.unit_spec
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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))
⊢ Eq.{u_1 + 1} (α := R) ((↑(Rat.num 1) : R) /ₚ (↑(Rat.pnatDen 1) : Rˣ)) 1

Tactic:
simp
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 : ℚ
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)
⊢ (↑(a * b).num : R) /ₚ (↑(a * b).pnatDen : Rˣ) =
    HMul.hMul (α := R) ((↑a.num : R) /ₚ (↑a.pnatDen : Rˣ)) ((↑b.num : R) /ₚ (↑b.pnatDen : 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]

Premises used: divp_eq_iff_mul_eq, divp_assoc, _private.0.EqualCharZero.pnatCast_eq_natCast, divp_mul_eq_mul_divp, divp_divp_eq_divp_mul, Rat.coe_pnatDen, Units.val_mul
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)
trans₁ :
  (↑((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ)) : R) = HMul.hMul (α := R) (↑a.num : R) (↑b.num : R) * (↑(a * 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)

Tactic:
trans (↑((a * b).num * a.den * b.den) : R)

Premises used: Int.cast, Rat.num, HMul.hMul, Rat.den, Nat.cast
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 : ℚ
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)
⊢ (↑(a * b).num : R) * HMul.hMul (α := R) (↑b.den : R) (↑a.den : R) = (↑((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ)) : R)

Tactic:
simp_rw [Int.cast_mul, Int.cast_natCast]

Premises used: Int.cast_natCast, Int.cast_mul
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 * b).num : R) (↑a.den : R) * (↑b.den : R)

Tactic:
ring