-- Mathlib/Algebra/CharP/Algebra.lean
theorem CharP.of_ringHom_of_ne_zero {R A : Type*} [Ring R] [NoZeroDivisors R]
    [NonAssocSemiring A] [Nontrivial A]
    (f : R →+* A) (p : ℕ) (hp : p ≠ 0) [CharP R p] : CharP A p

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this : Nontrivial R
H : Nat.Prime p
⊢ CharP A p

Tactic:
obtain ⟨q, hq⟩ := CharP.exists A

Result:
case intro
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
⊢ CharP A p

Proof state:
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this✝ : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
k : ℕ
e : p = q
this : k = 1
⊢ CharP A p

Tactic:
exact e ▸ hq

Result:
no goals

Proof state:
case intro
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
⊢ CharP A p

Tactic:
obtain ⟨k, e⟩ := dvd_of_ringHom f p q

Result:
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
k : ℕ
e : p = q * k
⊢ CharP A p

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
⊢ CharP A p

Tactic:
have := f.domain_nontrivial

Result:
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this : Nontrivial R
⊢ CharP A p

Proof state:
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this✝ : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
k : ℕ
e : p = q * k
this : k = 1
⊢ CharP A p

Tactic:
rw [this, mul_one] at e

Result:
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this✝ : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
k : ℕ
e : p = q
this : k = 1
⊢ CharP A p

Proof state:
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
k : ℕ
e : p = q * k
⊢ CharP A p

Tactic:
have := Nat.isUnit_iff.mp ((H.2 q k e).resolve_left (Nat.isUnit_iff.not.mpr (char_ne_one A q)))

Result:
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this✝ : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
k : ℕ
e : p = q * k
this : k = 1
⊢ CharP A p

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this : Nontrivial R
⊢ CharP A p

Tactic:
have H := (CharP.char_is_prime_or_zero R p).resolve_right hp

Result:
R : Type u_1
A : Type u_2
inst✝⁴ : Ring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this : Nontrivial R
H : Nat.Prime p
⊢ CharP A p