case a
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
a : ZMod n
⊢ ↑f a = ↑g a
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
⊢ f = g
ext a
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
⊢ ↑f ↑k = ↑g ↑k
case a
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
a : ZMod n
⊢ ↑f a = ↑g a
obtain ⟨k, rfl⟩ := ZMod.int_cast_surjective a
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := comp f (Int.castRingHom (ZMod n))
⊢ ↑f ↑k = ↑g ↑k
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
⊢ ↑f ↑k = ↑g ↑k
let φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := comp f (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := comp g (Int.castRingHom (ZMod n))
⊢ ↑f ↑k = ↑g ↑k
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := comp f (Int.castRingHom (ZMod n))
⊢ ↑f ↑k = ↑g ↑k
let ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := comp f (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := comp g (Int.castRingHom (ZMod n))
⊢ ↑φ k = ↑ψ k
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := comp f (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := comp g (Int.castRingHom (ZMod n))
⊢ ↑f ↑k = ↑g ↑k
show φ k = ψ k
no goals
case a.intro
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := comp f (Int.castRingHom (ZMod n))
ψ : ℤ →+* R := comp g (Int.castRingHom (ZMod n))
⊢ ↑φ k = ↑ψ k
rw [φ.ext_int ψ]