-- Mathlib/Algebra/CharP/CharAndCard.lean
theorem isUnit_iff_not_dvd_char_of_ringChar_ne_zero (R : Type*) [CommRing R] (p : ℕ) [Fact p.Prime]
    (hR : ringChar R ≠ 0) : IsUnit (p : R) ↔ ¬p ∣ ringChar R

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R

Tactic:
have hch := CharP.cast_eq_zero R (ringChar R)

Result:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R

Proof state:
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑p * ↑a = 1
⊢ IsUnit ↑p

Tactic:
exact isUnit_of_mul_eq_one (p : R) a hab

Result:
no goals

Proof state:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
hq : 0 = ↑q
h₄ : ¬ringChar R ∣ q → ¬↑q = 0
⊢ False

Tactic:
exact h₄ h₃ hq.symm

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑(a * ↑p + b * ↑(ringChar R)) = ↑1
⊢ IsUnit ↑p

Tactic:
push_cast at hab

Result:
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑a * ↑p + ↑b * ↑(ringChar R) = 1
⊢ IsUnit ↑p

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
r : ℕ
hr : q = ringChar R * r
⊢ False

Tactic:
rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False

Proof state:
case mp
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ IsUnit ↑p → ¬p ∣ ringChar R

Tactic:
rintro h₁ ⟨q, hq⟩

Result:
case mp.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
⊢ False

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R * 1 = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False

Tactic:
exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
⊢ IsUnit ↑p

Tactic:
rcases (hp.coprime_iff_not_dvd.mpr h).isCoprime with ⟨a, b, hab⟩

Result:
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : a * ↑p + b * ↑(ringChar R) = 1
⊢ IsUnit ↑p

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ IsUnit ↑p → ¬p ∣ ringChar R

case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ ¬p ∣ ringChar R → IsUnit ↑p

Proof state:
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ ¬p ∣ ringChar R → IsUnit ↑p

Tactic:
intro h

Result:
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
⊢ IsUnit ↑p

Proof state:
case mp.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
⊢ False

Tactic:
rcases IsUnit.exists_left_inv h₁ with ⟨a, ha⟩

Result:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
⊢ False

Proof state:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
⊢ False

Tactic:
apply_fun ((↑) : ℕ → R) at hq

Result:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
hq : ↑(ringChar R) = ↑(p * q)
⊢ False

Proof state:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
⊢ False

Tactic:
have h₄ := mt (CharP.intCast_eq_zero_iff R (ringChar R) q).mp

Result:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
⊢ ¬ringChar R ∣ q

Tactic:
rintro ⟨r, hr⟩

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
r : ℕ
hr : q = ringChar R * r
⊢ False

Proof state:
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑a * ↑p + ↑b * ↑(ringChar R) = 1
⊢ IsUnit ↑p

Tactic:
rw [hch, mul_zero, add_zero, mul_comm] at hab

Result:
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑p * ↑a = 1
⊢ IsUnit ↑p

Proof state:
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : a * ↑p + b * ↑(ringChar R) = 1
⊢ IsUnit ↑p

Tactic:
apply_fun ((↑) : ℤ → R) at hab

Result:
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑(a * ↑p + b * ↑(ringChar R)) = ↑1
⊢ IsUnit ↑p