case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℤ
⊢ IsInt (↑↑m) m
R : Type u_1
inst✝ : Ring R
n m : ℤ
⊢ IsInt n m → IsInt (↑n) m
rintro ⟨⟨⟩⟩
no goals
case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℤ
⊢ IsInt (↑↑m) m
exact ⟨rfl⟩