awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℚ
rw : (↑(a.num * b.num * (↑(a * b).den : ℤ)) : R) = HMul.hMul (α := R) (↑a.num : R) (↑b.num : R) * (↑(a * b).den : R)
⊢ (↑((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ)) : R) = HMul.hMul (α := R) (↑a.num : R) (↑b.num : R) * (↑(a * b).den : R)

Tactic:
rw [Rat.mul_num_den' a b]

Premises used: Rat.mul_num_den'
-- 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.num * b.num * (↑(a * b).den : ℤ)) : R) = HMul.hMul (α := R) (↑a.num : R) (↑b.num : R) * (↑(a * b).den : R)

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))
⊢ Eq.{u_1 + 1} (α := R) ((↑(Rat.num 0) : R) /ₚ (↑(Rat.pnatDen 0) : Rˣ)) 0

Tactic:
simp [divp]

Premises used: divp
-- 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.den : R) + HMul.hMul (α := R) (↑b.num : R) (↑a.den : R)) * (↑(a + b).den : R)
⊢ (↑(a + b).num : R) /ₚ (↑(a + b).pnatDen : Rˣ) =
    HAdd.hAdd (α := R) ((↑a.num : R) /ₚ (↑a.pnatDen : Rˣ)) ((↑b.num : R) /ₚ (↑b.pnatDen : 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]

Premises used: divp_eq_iff_mul_eq, Units.divp_add, _private.0.EqualCharZero.pnatCast_eq_natCast, divp_mul_eq_mul_divp, divp_divp_eq_divp_mul, Rat.coe_pnatDen, Units.val_mul, Units.add_divp
-- 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.den : R) + HMul.hMul (α := R) (↑b.num : R) (↑a.den : 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.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)

Premises used: Int.cast, Rat.num, HMul.hMul, Rat.den, Nat.cast, HAdd.hAdd
-- 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
-- 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 : ℚ
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)
⊢ (↑((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:
rw [Rat.add_num_den' a b]

Premises used: Rat.add_num_den'
-- 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.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:
simp
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 ≠ ⊤
suffices : CharP.{u_1} (R ⧸ I) 0
⊢ CharZero.{u_1} (R ⧸ I)

Tactic:
suffices CharP (R ⧸ I) 0 from CharP.charP_to_charZero _
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 ≠ ⊤
hp : CharP.{u_1} (R ⧸ I) 0
⊢ CharP.{u_1} (R ⧸ I) 0

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

Tactic:
exact hp
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)
⊢ MixedCharZero R p.succ

Tactic:
have h_mixed : MixedCharZero R p.succ := ⟨⟨I, ⟨hI_ne_top, hp⟩⟩⟩
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)
h_mixed : MixedCharZero R p.succ
⊢ CharP.{u_1} (R ⧸ I) 0

Tactic:
absurd h_mixed (h p.succ p.succ_pos)

Premises used: absurd, Nat.succ_pos, Nat.succ
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)
h_mixed : MixedCharZero R p.succ
⊢ CharP.{u_1} (R ⧸ I) 0

Tactic:
exact absurd h_mixed (h p.succ p.succ_pos)

Premises used: absurd, Nat.succ_pos, Nat.succ
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
intro₁ : ∀ (p : ℕ) (hp : CharP.{u_1} (R ⧸ I) (p + 1)), 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)
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 : ℕ), 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)

Premises used: CharP.exists, HasQuotient.Quotient
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
p : ℕ
p_pos : p > 0
by_contra : ∀ (hp_mixedChar : MixedCharZero R p), False
⊢ ¬MixedCharZero R p

Tactic:
by_contra hp_mixedChar
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
rcases : ∀ (I : Ideal R) (hI_ne_top : I ≠ ⊤) (hI_p : CharP.{u_1} (R ⧸ I) p), False
⊢ False

Tactic:
rcases hp_mixedChar.charP_quotient with ⟨I, hI_ne_top, hI_p⟩

Premises used: MixedCharZero.charP_quotient
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ CharP.{u_1} (R ⧸ I) 0

Tactic:
replace hI_zero : CharP (R ⧸ I) 0 := @CharP.ofCharZero _ _ (h I hI_ne_top)
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
hI_zero : CharP.{u_1} (R ⧸ I) 0
⊢ False

Tactic:
absurd (CharP.eq (R ⧸ I) hI_p hI_zero) (ne_of_gt p_pos)

Premises used: ne_of_gt, HasQuotient.Quotient, absurd, CharP.eq
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
hI_zero : CharP.{u_1} (R ⧸ I) 0
⊢ False

Tactic:
exact absurd (CharP.eq (R ⧸ I) hI_p hI_zero) (ne_of_gt p_pos)

Premises used: ne_of_gt, HasQuotient.Quotient, absurd, CharP.eq
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
⊢ (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)) ↔ ∀ p > 0, ¬MixedCharZero R p

Tactic:
⟨to_not_mixedCharZero R, of_not_mixedCharZero R⟩

Premises used: _private.0.EqualCharZero.of_not_mixedCharZero, _private.0.EqualCharZero.to_not_mixedCharZero, Iff.intro
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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)
mpr : (∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)) → Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R)
⊢ Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)

Tactic:
constructor
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
h_alg : Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R)
mp : ∀ (h_alg' : Algebra ℚ R) (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)

Tactic:
haveI h_alg' : Algebra ℚ R := h_alg.some
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
h_alg : Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R)
h_alg' : Algebra ℚ R
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)

Tactic:
apply of_algebraRat

Premises used: _private.0.EqualCharZero.of_algebraRat
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
mpr : Algebra ℚ R
⊢ Nonempty.{max (u_1 + 1) 1} (Algebra ℚ R)

Tactic:
apply Nonempty.intro

Premises used: Nonempty.intro
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
⊢ Algebra ℚ R

Tactic:
exact algebraRat h

Premises used: _private.0.EqualCharZero.algebraRat
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
contrapose! : Nonempty.{u_1 + 1} (Algebra ℚ R) ↔ ∀ (p : ℕ) (_ : p > 0), ¬MixedCharZero R p
⊢ IsEmpty.{max (u_1 + 1) 1} (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p

Tactic:
contrapose!
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
rw : Nonempty.{u_1 + 1} (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)
⊢ Nonempty.{u_1 + 1} (Algebra ℚ R) ↔ ∀ (p : ℕ) (_ : p > 0), ¬MixedCharZero R p

Tactic:
rw [← EqualCharZero.iff_not_mixedCharZero]

Premises used: EqualCharZero.iff_not_mixedCharZero
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
⊢ Nonempty.{u_1 + 1} (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero.{u_1} (R ⧸ I)

Tactic:
apply EqualCharZero.nonempty_algebraRat_iff

Premises used: EqualCharZero.nonempty_algebraRat_iff
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
neg : ∀ (h : ¬∃ p > 0, MixedCharZero R p), P
⊢ P

Tactic:
by_cases h : ∃ p > 0, MixedCharZero R p
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
pos : ∀ (p : ℕ) (H : p > 0) (hp : MixedCharZero R p), P
⊢ P

Tactic:
rcases h with ⟨p, ⟨H, hp⟩⟩
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
pos : ∀ (h_mixed : ∀ p > 0, MixedCharZero R p → P) (p : ℕ) (H : p > 0) (hp : MixedCharZero R p), P
⊢ P

Tactic:
rw [← MixedCharZero.reduce_to_p_prime] at h_mixed

Premises used: MixedCharZero.reduce_to_p_prime
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ p > 0, MixedCharZero R p → P
p : ℕ
H : p > 0
hp : MixedCharZero R p
⊢ P

Tactic:
h_mixed p H hp
-- Module: Mathlib.Algebra.CharP.MixedCharZero
Goal:
R : Type u_1
inst : CommRing R
P : Prop
inst_1 : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ p > 0, MixedCharZero R p → P
p : ℕ
H : p > 0
hp : MixedCharZero R p
⊢ P

Tactic:
exact h_mixed p H hp
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
neg : Algebra ℚ R
⊢ P

Tactic:
apply h_equal
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ Nonempty.{u_1 + 1} (Algebra ℚ R)

Tactic:
rw [← isEmpty_algebraRat_iff_mixedCharZero, not_isEmpty_iff] at h

Premises used: isEmpty_algebraRat_iff_mixedCharZero, not_isEmpty_iff
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 : Nonempty.{u_1 + 1} (Algebra ℚ R)
⊢ Algebra ℚ R

Tactic:
exact h.some

Premises used: Nonempty.some
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
neg : ∀ (h : ¬p = 0), P
⊢ P

Tactic:
by_cases h : p = 0
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
⊢ CharP R 0

Tactic:
rw [h] at p_charP
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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_charP₁ : CharP R 0
⊢ p = 0

Tactic:
rw [h] at p_charP
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
pos : ∀ (h0 : CharZero R), P
⊢ P

Tactic:
haveI h0 : CharZero R := CharP.charP_to_charZero R
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
h0 : CharZero R
⊢ P

Tactic:
split_equalCharZero_mixedCharZero R h_equal h_mixed

Premises used: split_equalCharZero_mixedCharZero
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
h0 : CharZero R
⊢ P

Tactic:
exact split_equalCharZero_mixedCharZero R h_equal h_mixed

Premises used: split_equalCharZero_mixedCharZero
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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

Tactic:
h_pos p h p_charP
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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

Tactic:
exact h_pos p h p_charP
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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 : ℕ), 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

Premises used: CharP.exists
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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

Tactic:
split_by_characteristic R ?_ h_equal h_mixed

Premises used: split_by_characteristic
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
refine : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
⊢ P

Tactic:
refine split_by_characteristic R ?_ h_equal h_mixed

Premises used: split_by_characteristic
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
have : ∀ (p_prime : Nat.Prime p), 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
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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_prime : Nat.Prime p
⊢ P

Tactic:
h_pos p p_prime p_char
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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_prime : Nat.Prime p
⊢ P

Tactic:
exact h_pos p p_prime p_char
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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

Tactic:
split_by_characteristic R ?_ h_equal h_mixed

Premises used: split_by_characteristic
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
refine : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
⊢ P

Tactic:
refine split_by_characteristic R ?_ h_equal h_mixed

Premises used: split_by_characteristic
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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
have : ∀ (p_ppow : IsPrimePow p), P
⊢ P

Tactic:
have p_ppow : IsPrimePow (p : ℕ) := or_iff_not_imp_left.mp (charP_zero_or_prime_power R p) p_pos
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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_ppow : IsPrimePow p
⊢ P

Tactic:
h_pos p p_ppow p_char
-- Module: Mathlib.Algebra.CharP.MixedCharZero
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_ppow : IsPrimePow p
⊢ P

Tactic:
exact h_pos p p_ppow p_char
-- Module: Mathlib.Algebra.CharP.Pi
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
rw₁ rw₂ : Eq.{v + 1} (α := R) 0 0
⊢ Eq.{v + 1} (α := R) ((Pi.evalRingHom (fun (x : ι) ↦ R) j : (a : (i : ι) → R) → R) (↑x : ι → R) : R) (0 : R)

Tactic:
rw [map_natCast, h]

Premises used: map_natCast
-- Module: Mathlib.Algebra.CharP.Pi
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)
rw₂ rw₃ : Eq.{v + 1} (α := R) 0 0
⊢ Eq.{v + 1} (α := R) (↑x : R) 0

Tactic:
rw [← map_natCast (Pi.evalRingHom (fun _ : ι => R) i) x, h, map_zero]

Premises used: map_zero, map_natCast, Pi.evalRingHom
-- Module: Mathlib.Algebra.CharP.Pi
Goal:
ι : Type u
inst : Nonempty ι
R : Type v
inst_1 : CommRing R
p : ℕ
inst_2 : CharP R p
⊢ CharP (ι → R) p

Tactic:
CharP.pi ι R p

Premises used: CharP.pi
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
h :
  ∀ (a : ℤ),
    Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* R) (algebraMap ℤ R)) a ↔
      Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑p : ℤ)}) a
⊢ Eq (α := Ideal ℤ) (RingHom.ker (F := ℤ →+* R) (algebraMap ℤ R)) (Ideal.span {(↑p : ℤ)})

Tactic:
ext a
-- Module: Mathlib.Algebra.CharP.Quotient
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
a : ℤ
⊢ Membership.mem (γ := Ideal ℤ) (RingHom.ker (F := ℤ →+* R) (algebraMap ℤ R)) a ↔
    Membership.mem (γ := Ideal ℤ) (Ideal.span {(↑p : ℤ)}) a

Tactic:
simp [CharP.intCast_eq_zero_iff R p, Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton, CharP.intCast_eq_zero_iff