case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n

case mpr
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n ↔ m = n
constructor
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : ↑m = ↑n
⊢ m = n
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n
intro h
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : coeff (↑m) 0 = coeff (↑n) 0
⊢ m = n
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : ↑m = ↑n
⊢ m = n
apply_fun fun p => p.coeff 0  at h
no goals
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : coeff (↑m) 0 = coeff (↑n) 0
⊢ m = n
simpa using h
case mpr
R✝ : Type u
S : Type v
a b : R✝
n m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑m
case mpr
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n
rintro rfl
no goals
case mpr
R✝ : Type u
S : Type v
a b : R✝
n m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑m
rfl